The Universe conspired to bring me precompiled binaries for Idris

Installing it with cabal on Windows proved impossible. A SuSe VM on VirtualBox couldn’t cut it either. Actually installing MinGW, which was the recommended way on WIndows, didn’t give me Idris, either. But still, I wanted it. And, sure enough, as Paulo Coelho predicted, the Universe conspired to help me get it, and one can now download precompiled binaries for Windows!

Now that I had a real dependently-typed programming language, with realistic-looking tutorials and documentation, I thought it was a great excuse to implement type-safe dimensional calculations in it. The resulting code is so terse, compared to the Scala example, it almost feels like cheating. In the beginning, is the dependent type itself.

data DimVal : Int -> Int -> Int -> Int -> Type where
    DV :  (m:Int) -> (k:Int) -> (s:Int) -> (a:Int) -> (v:Float) -> DimVal m k s a

Please compare it with the Scala (and C++) equivalent. The similarities are obvious but this version completely blends the two levels together. DimVal is a type constructor indexed by four integers and DV is its sole constructor.

Calculating with these types needs the usual arithmetic operations. Unfortunately, trying to overload the operators did not work for me, as they were imported already by the Num class in the Prelude.

||| The Num class defines basic numerical arithmetic.
class Num a where
(+) : a -> a -> a
(-) : a -> a -> a
(*) : a -> a -> a
||| Absolute value
abs : a -> a
||| Conversion from Integer.
fromInteger : Integer -> a

DimVal cannot be made an instance of Num, because types need to be closed under all three operations, and this cannot be the case, since the point is to represent each dimension vector by a different type. So I faked four appropriate operators.

infixr 10 /+/
(/+/) : DimVal m k s a -> DimVal m k s a -> DimVal m k s a
(DV m k s a v1) /+/ (DV m k s a v2) = DV m k s a (v1+v2)

infixr 10 /-/
(/-/) : DimVal m k s a -> DimVal m k s a -> DimVal m k s a
(DV m k s a v1) /-/ (DV m k s a v2) = DV m k s a (v1-v2)

infixr 20 /*/
(/*/) : DimVal m1 k1 s1 a1 -> DimVal m2 k2 s2 a2 -> DimVal (m1+m2) (k1+k2) (s1+s2) (a1+a2)
(DV m1 k1 s1 a1 v1) /*/ (DV m2 k2 s2 a2 v2) = DV (m1+m2) (k1+k2) (s1+s2) (a1+a2) (v1*v2)

infixr 20 ///
(///) : DimVal m1 k1 s1 a1 -> DimVal m2 k2 s2 a2 -> DimVal (m1-m2) (k1-k2) (s1-s2) (a1-a2)
(DV m1 k1 s1 a1 v1) /// (DV m2 k2 s2 a2 v2) = DV (m1-m2) (k1-k2) (s1-s2) (a1-a2) (v1/v2)

Next up, printing dimensioned values. For this, I used an intermediate Dimension type.

data Dimension : Type where
    Dim : (m:Int) -> (k:Int) -> (s:Int) -> (a:Int) -> Dimension    

unitToStr : Dimension -> String
unitToStr (Dim m k s a) =
    case (m, k, s, a) of
        (0,0,1,1) => "C"
        (1,1,-2,0) => "N"
        (0,0,-1,0) => "Hz"
        (-1,1,-2,0) => "Pa"
        (2,1,-3,-2) => "ohm"
        (2,1,-3,-1) => "V"
        (-2,-1,3,2) => "S"
        (2,1,-3,0) => "W"
        (2,1,-2,0) => "J"
        (-2,-1,4,2) => "F"
        (2,1,-2,-2) => "H"
        (2,1,-2,-1) => "Wb"
        (0,1,-2,-1) => "T"
        _ => (if m /= 0 then "m" ++ (if m /= 1 then (show m) else "") else "") ++
            (if (m /= 0) && (k /= 0) then "." else "") ++
            (if k /= 0 then "Kg" ++ (if k /= 1 then (show k) else "") else "") ++
            (if (abs(m) + abs(k)) /= 0 && s /= 0 then "." else "") ++
            (if s /= 0 then "s" ++ (if s /= 1 then (show s) else "") else "") ++
            (if (abs(m) + abs(k) + abs(s)) /= 0 && a /= 0 then "." else "") ++
            (if a /= 0 then "A" ++ (if a /= 1 then (show a) else "") else "")
            
toStr : DimVal m k s a -> String
toStr (DV m k s a v) = (show v) ++ " " ++ (unitToStr (Dim m k s a))
    
instance Show (DimVal m k s a) where
    show dv = toStr dv

The Num class was out of the question, but Eq and Ord are readily instantiable.

dimValEq : DimVal m k s a -> DimVal m k s a -> Bool
dimValEq (DV m k s a v1) (DV m k s a v2) = (v1==v2)
    
dimValComp : DimVal m k s a -> DimVal m k s a -> Ordering
dimValComp (DV m k s a v1) (DV m k s a v2) = compare v1 v2

instance Eq (DimVal m k s a) where
    dv1 == dv2 = dimValEq dv1 dv2

instance Ord (DimVal m k s a) where
    compare dv1 dv2 = dimValComp dv1 dv2

Idris has syntax support for creating DSLs so, a native Idris speaker would probably go on to create a better DSL for creating values, arithmetic etc. I’ll just show how type-safe calculations can naturally be encoded in plain Idris. I did not go into the trouble of defining all named physical types but I guess you see how this can be done without any problem.

Mass : Type
Mass = DimVal 1 0 0 0

mass : Float -> Mass
mass = DV 1 0 0 0

main : IO ()
main = 
    let x = DV 1 1 (-2) 0 14.5 in
    let y = DV 1 1 (-2) 0 15.5 in
    let z = DV 2 2 0 0 15.5 in
    let xpy = x /+/ y in
    let xmy = x /-/ y in
    let xtz = x /*/ z in
    let xdz = x /// z in
    let m : Mass = mass 12.6 in
        do
            putStrLn (show m)
            putStrLn (show x)
            putStrLn (show y)
            putStrLn (show z)
            putStrLn (show (x == x))
            putStrLn (show (x == y))
--            putStrLn ((show (y == z))) -- Doesn't even compile!
            putStrLn (show (x < y))
--            putStrLn ((show (z < y))) -- Doesn't even compile!
            putStrLn (show xtz)
            putStrLn (show xdz)

It does feel like cheating, doesn’t it? Calculating with physical types is actually done at two levels: the values themselves are operated upon as if they were dimensionless, while the dimensions are vectors representing exponents and are operated upon using exponent arithmetic. Idris handles both levels in the same way, very naturally. It is said that all high-level languages are equivalent in the computations they can express, but their compilers are certainly not equivalent.

My Frugal Summer of Code, part 2

Here I am, continuing my foray into the realm of array programming, that started in my previous post. Let me start with a disclaimer: I do not claim that what you read here is good, idiomatic J.This is not a J tutorial. I mean it as an exposé of the notions of array programming and how they can enhance the worldview of the traditional programmer. I’d love it if it could also be a bridge between mainstream FP and Array Programming, but I’m afraid I’m not sufficiently proficient in either to do it.

Remember the last five lines of code? I’m going to dissect them now for your benefit.

NB. Locations (mask bits) where digits have lines 
digitmasks =. '         ' ~:"(1) (,"2 digits)

Laid out, this means: concatenate all lines in each digit (keeping them in three lines serves only for displaying them). This is done by , (called append), applied to cells of digits of rank 2 (the "2 modifier, called an conjunction in J). Then, compare lines (cells of rank 1, the "1 thing) of that, using the “not equals” comparator (the ~:) to a literal with 9 spaces.

This gives you a bit (an 1) whenever there’s anything than a space. I can do that because the digits, as defined, when they share a graphic element, it’s always the same in the same location. So I’m getting rid of some excessive information to make my life easier. So, digitmasks is the following.

0 1 0 1 0 1 1 1 1
0 0 0 0 0 1 0 0 1
0 1 0 0 1 1 1 1 0
0 1 0 0 1 1 0 1 1
0 0 0 1 1 1 0 0 1
0 1 0 1 1 0 0 1 1
0 1 0 1 1 0 1 1 1
0 1 0 0 0 1 0 0 1
0 1 0 1 1 1 1 1 1
0 1 0 1 1 1 0 1 1
NB. Locations where digits share mask bits
maskcompmatrix =. (-"1/~ digitmasks) ="0 ] 0

Moving on, first, I make a table where, I subtract each line (i.e. digit bitmask) from each other. The -"1/~ digitmasks thing is shorthand for digitmasks -"1/ digitmasks, i.e. tabulate (the / adverb – another kind of higher-level construct, like conjunctions – for a dyadic operation) the operation “subtract each line” (the -"1). Afterwards, the whole thing is compared, bit by bit (the ="0) to zero. The result is a 10 x 10 x 9 bitmask array. Are you getting the hang of it?

NB. Count of similar mask bits between digits
diffmatrix =. +/"1 maskcompmatrix

Further, I sum: insert, using the / adverb, the operation “plus” (the + verb) at the level of each line (the "1 conjunction) on maskcompmatrix. This gives a 10 x 10 array of the number of same bits in each bitmask (digit).

9 5 6 6 5 6 7 6 8 7
5 9 4 6 7 4 3 8 4 5
6 4 9 7 4 5 6 5 7 6
6 6 7 9 6 7 6 7 7 8
5 7 4 6 9 6 5 6 6 7
6 4 5 7 6 9 8 5 7 8
7 3 6 6 5 8 9 4 8 7
6 8 5 7 6 5 4 9 5 6
8 4 7 7 6 7 8 5 9 8
7 5 6 8 7 8 7 6 8 9

Now comes the easy part.

NB. Outside the diagonal: Digits that share 8 out of 9 mask bits
offbyone =. diffmatrix ="(0) 8

I make a 10 x 10 array of selectors (bits) when digits share 8 out of 9 bits.

offbyones =. (monad : '< y # i. 10')"1 offbyone

Then, I make a vector (list, in J) of which digits share 8 bits for each digit.

┌─┬─┬┬─┬┬───┬───┬─┬─────┬─────┐
│8│7││9││6 9│5 8│1│0 6 9│3 5 8│
└─┴─┴┴─┴┴───┴───┴─┴─────┴─────┘

I wanted to spare you (and me!) the trouble of bringing up “boxing” but, since the shape is irregular, it was really the easiest solution. Boxing (conveniently displayed with actual boxes) creates an atomic value of anything you put into it.

And, in reality, I found out that it makes calculations simpler if the digits themselves are included, so I really need the following.

NB. Digits that share 8 or 9 (i.e. themselves) mask bits
sameandoffbyone =. diffmatrix >:"(0) 8

sameandoffbyones =. (monad : '< y # i. 10')"1 sameandoffbyone
┌───┬───┬─┬───┬─┬─────┬─────┬───┬───────┬───────┐
│0 8│1 7│2│3 9│4│5 6 9│5 6 8│1 7│0 6 8 9│3 5 8 9│
└───┴───┴─┴───┴─┴─────┴─────┴───┴───────┴───────┘

This was sort of easy, wasn’t it? I’m afraid the rest will be a little more complicated. I’ll throw it all in one glob, and focus on the big picture first. The operation I’m trying to achieve, is fix broken account numbers by trying similar digits, where similar is defined by off-by-one bit.

NB. fold operation to produce the combinations
foldop =. dyad : ',/ <"1 (>y) ,"1/ (,. >x)'
identity =. <''

NB. Use if checksum is <> 0: try combinations with digits off by one mask bit and see which (if any) produce checksum of 0
alternatives =. monad define
 alt =. >"0 foldop/ identity ,~ |. y { sameandoffbyones
 ((checksum"1 = 0:) alt) # alt
)

There’s a fold taking place, which is a common thing in FP. The first complication is that, in J, for reasons of uniformity with its right-to-left evaluation order, when you fold a list (remember, a list is a vector of something) you also do it right-to-left. That’s why I reverse (the |. thing) the result of indexing (the {) sameandoffbyones by the account digits (y stands for the argument in a monadic verb). Then I append the identity element, which is a boxed empty list. Folding takes place, and I’ll explain the operation folded next but, for now, let’s stick to what the fold produces, which is a list of boxed candidate account numbers, which are unboxed (the >"0) and then checked with checksum (the checksum"1 = 0: is actually a composite verb!) and only those with zero checksum are kept (operation copy, the #).

Example usage:

alternatives 2 4 4 4 1 2 5 6 7
2 4 4 4 1 2 5 6 1
2 4 4 4 1 2 9 8 7
2 4 4 4 7 2 6 6 1

However, don’t try it on 7 2 3 4 5 6 7 8 9. It produces 109 possible alternatives! In retrospect, this error correction policy is not very robust or, rather, the checksum used in not suitable to how digits can be misread.

Let’s go back to the folded operation now. I won’t go into it symbol-by-symbol but here’s an English description. One operand holds a list of boxes with partial account numbers, and the result is also a list of boxes with longer partial account numbers, formed by appending the initial partial account numbers with all alternatives for the current digit, held by the other operand as a boxed list.

Have I picked your curiosity until now? Have I succeeded in presenting J as more than a curiosity itself? There is real power in its notions and it goes beyond its conciseness. Imagine all these operations using standard Scala, for example. “It’s easy if you try.” I think it is a useful thing to add to standard FP, which lacks the language to talk about arrays at the level that array programming languages do. I have not even found a data type to represent arbitrary-ranked arrays, let alone how to represent ranked operations and implicit loops and stuff. But I think it can be done, and I’m setting it as a wanna-do-it for the future.

My Frugal Summer of Code

The title being a wordplay on “Google Summer of Code” does not mean that it is not entirely true, as there is hardly any time during vacationing with two little children to write much code. And I admit that most of what you’ll see in this post was written pre- and post-vacations. But I did read a lot of stuff on array programming, APL, J, papers on array functional programming. I thought really hard (but vacation-grade hard) about how some of these things can be grafted on a more conventional functional language. And I did make an honest effort to find a Java or Scala library for dense multidimensional arrays that could provide a basic substrate for such an effort. If the job, Flying Donut or life, in general, let me, you’ll hear more in another post.

The current post, however, will use J to tackle a code kata I found, which I thought would be ideal for some array-fu.

Assume you have the three lines that constitute an account number. The first thing you should do is separate the nine “digits”. Conveniently, the same functionality can be used to generate some data useful in the sequel, so let’s start by separating the ten digits 0 – 9.

alldigits =. ] ;._2 (0 : 0)
 _     _  _     _  _  _  _  _
| |  | _| _||_||_ |_   ||_||_|
|_|  ||_  _|  | _||_|  ||_| _|
)

NB. Break in 3x3 cells
chop =. monad : ',/ (3 3 ,: 3 3) ];._3 y'

digits =. chop alldigits

I know, most of it looks like a cartoon character swearing. What you see in the above is a handy way of writing multi-line data and a handy higher-level operation to apply an operation to subarrays of an operand. Let’s chop a sample account number.

NB. A number with no wrong digits
num =. ] ;._2 (0 : 0)
    _  _     _  _  _  _  _ 
  | _| _||_||_ |_   ||_||_|
  ||_  _|  | _||_|  ||_| _|
)
 
nums =. chop num
<"_1 nums

The resulting “digits” are “boxed” so that they are also displayed as boxed.

┌───┬───┬───┬───┬───┬───┬───┬───┬───┐
│   │ _ │ _ │   │ _ │ _ │ _ │ _ │ _ │
│  |│ _|│ _|│|_|│|_ │|_ │  |│|_|│|_|│
│  |│|_ │ _|│  |│ _|│|_|│  |│|_|│ _|│
└───┴───┴───┴───┴───┴───┴───┴───┴───┘

And the magic continues. Let’s write lots of nested loops to recognize the corresponding digits.

NB. Results in character list
digitize =. digits&i.

Ok, I was kidding. Here’s what digitize nums gives you: the vector 1 2 3 4 5 6 7 8 9. Transforming it to a human readable string is equally ridiculously simple.

NB. Takes digitized list, results in character list 
show =. {&'0123456789?'

Non recognized digits result in a past-the-end index, hence the ‘?’ after the last valid digit.

NB. A number with one wrong digit
wrongnum =. ] ;._2 (0 : 0)
_   _  _     _  _  _  _  _ 
  | _| _||_||_ |_   ||_||_|
  ||_  _|  | _||_|  ||_| _|
)  
wrongnums =. chop wrongnum
show digitize wrongnums

The output is ?23456789.

Surely calculating the checksum should be a little more difficult.

NB. (to be used only on correctly parsed numbers)
checksum =. monad : '11 | (1+i. 9) (+/ . *) |. y'

Well, it is a little more difficult, truth be told. But I have to go to bed, so I’ll break off at this point, but only after I compute some data for the next step, which is to try digits to similar ones in order to produce candidate account numbers to recover from checksum errors.

NB. Locations (mask bits) where digits have lines 
digitmasks =. '         ' ~:"(1) (,"2 digits)

NB. Locations where digits share mask bits
maskcompmatrix =. (-"1/~ digitmasks) ="0 ] 0

NB. Count of similar mask bits between digits
diffmatrix =. +/"1 maskcompmatrix

NB. Outside the diagonal: Digits that share 8 out of 9 mask bits
offbyone =. diffmatrix ="(0) 8

offbyones =. (monad : '< y # i. 10')"1 offbyone

I guess this suddenly strikes you as too much code, doesn’t it? Five whole lines! It’s only one line shorter than the code to define a property in Java, for crying out loud!

I’ll get into the details next time!

TO BE CONTINUED