## Friday, November 09, 2007

### Some lambda calculus examples

#### Syntax

In a previous blog entry I described a simple evaluator and type checker for the lambda cube, i.e., various forms of lambda calculus.

Here I'm going to show some examples of code in pure typed λ-calculus. All the examples are typable in Fω; the full lambda cube is not necessary.

Before doing any examples we'd better have some syntax that is not too painful, because writing λ-expression in raw Haskell is tedious. The syntax for variables, * kind, and application is easy, I'll just use Haskell syntax. For λ-expressions the Haskell syntax doesn't allow explicit type annotations, but various Haskell compiler implement that extension, so I'll just pick that. So a λ will be written, "\ (var::type) -> expr". And as in Haskell I'll allow multiple variables between the "\" and "->"; it's just a shorthand for multiple lambdas.

So what about the dependent function type? The syntax (x:t)→u suggests (x::t)->u, so I'll use that. And when the variable doesn't occur we'll write t->u as usual. For type variables Haskell (well, not Haskell 98, but extensions) uses forall (a::*) . t, so I'll allow that too.

An example, the identity function:

```\ (a::*) (x::a) -> x
```
with type
```forall (a::*) . a->a
```
And using it
```id Int 5
```
Writing a pretty printer and parser for this is pretty straight forward so I'll skip that and just point you to the code. BTW, instead of using Parsec for the parser like everyone else I used ReadP. The ReadP library is very nice, partly because the alternative operator is actually commutative (unlike Parsec). But the error messages suck.

#### Enter let

Now if we want to use, say, the identity function more than once we need to name it. There is a mechanism for that, namely λ. But it looks awkward. Look:
```(\ (id :: forall (a::*) . a->a) -> ... id ... id ... id ...) (\ (a::*) (x::a) -> x)
```
What makes it awkward is that the name, id, is far away from the body, \ (a::*) (x::a) -> x. From Haskell we are more used the let and where expressions. So let's add that let. Instead of what we have above we'll write
```let id :: forall (a::*) . a->a = \ (a::*) (x::a) -> x
in  ... id ... id ... id ...
```
The let construct could be just be syntactic suger for a lambda and an application, but I've decided to add it as a constructor to the expression type instead.
```    | Let Sym Type Expr Expr
```
Adding a new constructor means that we have to modify all the functions operating on Expr, and it's extra much work because Let is a variable binding construct. For substitution we just cheat a little and use the expansion into an application and λ
```    sub (Let i t e b) = let App (Lam i' t' b') e' = sub (App (Lam i t b) e)
in  Let i' t' e' b'
```
And for normal form we use the same trick.
```    spine (Let i t e b) as = spine (App (Lam i t b) e) as
```
And for now, let's extend the type checker in the same way.

To make definitions a little less verbose I'll allow multiple bindings. E.g.

```let x :: Int = g a; y :: Int = f x in h x y
```
It's just multiple nested Lets in the obvious way. Another shorthand. I'll allow the identity function to be written
```let id (a::*) (x::a) :: a = x
in ...
```
The translation is pretty easy
```let f (x1::t1) ... (xn::tn) :: t = b in e
```
is
```let f :: forall (x1::t1) ... (xn::tn) . t = \ (x1::t1) ... (xn::tn) -> b in e
```
And finally, to make it even more like Haskell, I'll allow the type signature to be on a line of its own, omitting types on the bound variables.
```let id :: forall (a::*) . a -> a;
id a x = x;
in  ...
```
It's pretty easy to translate to the bare expression type. Why all these little syntactic extras? Well, remember Mary Poppins "A spoonful of sugar makes the medicine go down." Phew! Enough syntax, on to the examples.

#### Bool

We could start by throwing in all kinds of primitive types into our little language, but who knows what might happen then. All the nice properties that have been shown about the language might not hold anymore. So instead we'll code all the types we need with what we already have.

The Bool type has two values: False and True. So we need to find a type that has exactly two different values. Fortunately that's easy: a->a->a (I'll be a bit sloppy and leave off top level quantifier sometimes, just like Haskell; That should be forall (a::*) . a->a->a).

Why does that have two possible values? Well, we have a function type that must return an a for any possible a that it's given, so it can't conjure up the return value out of thin air. It has to return one of it's arguments. And there are two arguments to choose from, so there are two different values in that type. Here's Bool, False, True:

```Bool :: *;
Bool = forall (a::*) . a->a->a;

False :: Bool;
False = \ (a::*) (x::a) (y::a) -> x;

True  :: Bool;
True = \ (a::*) (x::a) (y::a) -> y;
```
If the definition for Bool was written in Haskell it would be
```type Bool = forall a . a->a->a

false :: Bool
false = \ x y -> x

true :: Bool
true = \ x y -> y
```
It would be easy to add more sugar and allow type which just means you're defining something of type *. And you could also make an omitted type in a forall mean type *. But I've not added these little extras.

Defining the if function is trivial; it's just a matter of permuting the arguments a little, because the boolean values come with the "if" built in.

```if :: forall (a::*) . Bool -> a -> a -> a;
if a b t f = b a t f;
```
Note how the type signature is exactly the same as you'd find in Haskell. A difference is that we have explicit type abstraction and type application. For instance, if takes a first argument that is the type of the branches. So when using if we must pass in a type.

Given this we can try to type check some simple code:

```let Bool :: *;
Bool = forall (a::*) . a->a->a;
False :: Bool;
False = \ (a::*) (x::a) (y::a) -> x;
in  False
```
Here is what happens:
```*CubeExpr> typeCheck \$ read "let Bool :: *; Bool = forall (a::*) . a->a->a; False :: Bool;False = \\ (a::*) (x::a) (y::a) -> x; in False"
*** Exception: Type error:
Bad function argument type:
Function: \ (False :: Bool) -> False
argument: \ (a :: *) (x :: a) (y :: a) -> x
expected type: Bool
got type: forall (a :: *) . a->a->a
```
What is it whining about? Expected Bool, got forall (a :: *) . a->a->a. But it says right there in the code that Bool is exactly that. What's going on?
Well, the type checker knows the type of everything, but not the value of anything. So the type checker knows that type of Bool is *, but it doesn't know what it is equal to.

The problem is that when we have a let binding we know the value of the defined variable and to be able to do dependent type checking the type checker needs to know it too. We need to change the type checking of let. Here's a simple solution:

```tCheck r (Let s t a e) = do
tCheck r t
ta <- tCheck r a
when (not (betaEq ta t)) \$ throwError \$ "Bad let def\n" ++ show (ta, t)
te <- tCheck r (subst s a e)
tCheck r (Pi s t te)
return te
```
Note how we substitute the value of the definition (a) in the body before type checking it. This is a sledge hammer approach. A better one would be to change the environment in the type checker to carry values when they are known. These values could then be used when computing the normal form of an expression. But let's keep it simple for now.

Let's try again:

```*CubeExpr> typeCheck' \$ read "let Bool :: *; Bool = forall (a::*) . a->a->a; False :: Bool;False = \\ (a::*) (x::a) (y::a) -> x; in False"
forall (a :: *) . a->a->a
```
That worked!

#### A simple top level

To make experimentation easier I've added a simple top level where you can evaluate expression, make definitions, load files, etc. The files are just a bunch of definitions the way they would go inside a let.

Sample session:

```Welcome to the Cube.
Use :help to get help.
Cube> \ (a::*) (x::a) -> x
\ (a :: *) (x :: a) -> x
::
forall (a :: *) . a->a
Cube>
```
When evaluating an expression it will first print the value, then ::, and finally the type.
Let's try some more. Here's the file bool.cube.
```-- The Bool type.

Bool :: *;
Bool = forall (boolT::*) . boolT->boolT->boolT;

False :: Bool;
False = \ (boolT::*) (false::boolT) (true::boolT) -> false;

True  :: Bool;
True = \ (boolT::*) (false::boolT) (true::boolT) -> true;

if :: forall (a::*) . Bool -> a -> a -> a;
if a b t f = b a f t;

not :: Bool -> Bool;
not b = if Bool b False True;

and :: Bool -> Bool -> Bool;
and x y = if Bool x y False;

or :: Bool -> Bool -> Bool;
or x y = if Bool x True y;
```
Note how I've named some of the type variables with more suggestive names. More about that in a moment.
```Cube> :load bool.cube
Cube> True
\ (boolT :: *) (false :: boolT) (true :: boolT) -> true
::
forall (boolT :: *) . boolT->boolT->boolT
Cube> and True False
\ (boolT :: *) (false :: boolT) (true :: boolT) -> false
::
forall (boolT :: *) . boolT->boolT->boolT
```
By staring carefully at these you can convince yourself that it's right. What's making it a little hard to read are all those leading lambdas (and the corresponding function types). But there's an option to suppress the printing of them.
```Cube> :skip
Cube> True
true
::
boolT
Cube> and True False
false
::
boolT
```
Look, it got deceptively readable.

#### Characters

So we can define booleans. What about something like characters? You can define those too. What is the ASCII type? It's a type with 128 different values. We saw how we can make a type with two values (Bool); we can do the same for 128. Since that takes a lot of room, I'll do it for just four values.
```Char :: *;
Char = forall (charT::*) . charT->charT->charT->charT->charT;

'a' :: Char;
'a' = \ (charT::*) (_'a'::charT) (_'b'::charT) (_'c'::charT) (_'d'::charT) -> _'a';
'b' :: Char;
'b' = \ (charT::*) (_'a'::charT) (_'b'::charT) (_'c'::charT) (_'d'::charT) -> _'b';
'c' :: Char;
'c' = \ (charT::*) (_'a'::charT) (_'b'::charT) (_'c'::charT) (_'d'::charT) -> _'c';
'd' :: Char;
'd' = \ (charT::*) (_'a'::charT) (_'b'::charT) (_'c'::charT) (_'d'::charT) -> _'d';

eqChar :: Char -> Char -> Bool;
eqChar x y = x Bool (y Bool True False False False)
(y Bool False True False False)
(y Bool False False True False)
(y Bool False False False True);
```
Since single quotes are allowed in identifiers in my little language the 'a' is just an identifier as usual. Some sample use:
```Cube> :load char.cube
Cube> 'a'
_'a'
::
charT
Cube> eqChar 'a' 'a'
true
::
boolT
Cube> eqChar 'a' 'b'
false
::
boolT
```

A different way to use characters is just to assume that there is some character type and that is has some values. How can we do that? By using a lambda expression.

```\ (Char :: *) -> \ ('a' :: Char) ('b' :: Char) ... -> ...
```
One final little syntactic sugar is to allow lambda expressions to be written with let. So
```let x :: T;
in  e
```
is the same as
```\ (x :: T) -> e
```
So for Char we can write
```Char :: *;
'a' :: Char;
'b' :: Char;
'c' :: Char;
'd' :: Char;
eqChar :: Char -> Char -> Bool;
```
This is a very handy notation during program development, btw. Inside i let you can first just write the type of something and then use it freely. This something will then be lambda abstracted until such a time that you provide the definition.

Let's try the "fake" characters.

```Cube> :load extchar.cube
Cube> 'a'
'a'
::
Char
Cube> :skip
Cube> 'a'
\ (Char :: *) ('a' :: Char) ('b' :: Char) ('c' :: Char) ('d' :: Char)
(eqChar :: Char->Char->forall (boolT :: *) . boolT->boolT->boolT)
-> 'a'
::
forall (Char :: *) .
Char->Char->Char->Char->
(Char->Char->forall (boolT :: *) . boolT->boolT->boolT)->
Char
Cube> :skip
Cube> eqChar 'a' 'b'
eqChar 'a' 'b'
::
forall (boolT :: *) . boolT->boolT->boolT
```
Now eqChar no longer gets evaluated, naturally, because it has no definition; it's λ bound.

Now we know how the Char type could be implemented (or supplied from the outside). It would then be all right to add it as a primitive (with the same behavior), because it will not ruin any properties. (Speaking of ruining properties, the seq function in Haskell is an example of a function that cannot be defined in the λ-calculus. And sure enough, adding it to Haskell ruined the validity of η-reduction.)

It's not difficult to extend the Expr type with some Prim constructor for primitive functions, and adding some special cases in the syntax and type checking for them. But since this is not intended to be a usable language I'll resist the temptation (for now).

#### Pairs

OK, booleans and characters were pretty easy. Let's do pairs next. The Pair type is parameterized over two types; the type of the first and the second component. As with booleans the representation of pairs come with the case analysis "build in". (Case analysis on pairs is flip uncurry in Haskell.) If we can correctly implement building pairs, fst, and snd we are done.
```Pair :: * -> * -> *;
Pair a b = forall (pairT::*) . (a->b->pairT) -> pairT;

PairC :: forall (a::*) (b::*) . a -> b -> Pair a b;
PairC a b x y = \ (pairT::*) (pair :: a->b->pairT) -> pair x y;

fst :: forall (a::*) (b::*) . Pair a b -> a;
fst a b p = p a (\ (x::a) (y::b) -> x);

snd :: forall (a::*) (b::*) . Pair a b -> b;
snd a b p = p b (\ (x::a) (y::b) -> y);
```
So the type is called Pair and the constructor PairC. Since they live in the same name space we can't use Haskell's convention of giving them the same name (which is (,) in Haskell.).

Again, in Haskell the first definition would be

```type Pair a b = forall pairT . (a->b->pairT) -> pairT
```
Staring at these definitions makes it obvious(?) that they work. But we can test it too.
```Cube> :let S :: *; s :: S; T :: *; t :: T
Cube> :load pair.cube
Cube> :let p :: Pair S T; p = PairC S T s t
Cube> p
pair s t
::
pairT
Cube> fst S T p
s
::
S
Cube> snd S T p
t
::
T
```
The :let command is used to make bindings without having to load them from a file. The first :let just introduces some values to play with.

Again, the big difference compared to Haskell is that all types are explicit. (But users of templates in C++ or generics in Java/C# might appeciate it?)

#### Maybe

We can follow the same pattern and define Haskell's Maybe type. In fact any non-recursive Haskell data type has a mechanical translation and easy into lambda calculus. We've seen boolean, characters, and pairs above.
```Maybe :: * -> *;
Maybe a = forall (maybeT::*) . maybeT->(a->maybeT)->maybeT;

Nothing :: forall (a::*) . Maybe a;
Nothing a = \ (maybeT::*) (nothing::maybeT) (just::a->maybeT) -> nothing;

Just :: forall (a::*) . a -> Maybe a;
Just a x = \ (maybeT::*) (nothing::maybeT) (just::a->maybeT) -> just x;

maybe :: forall (a::*) (r::*) . r -> (a->r) -> Maybe a -> r;
maybe a r nothing just s = s r nothing just;
```

#### Natural numbers

Let's carry on with some natural numbers. Natural numbers are trickier because it's a recursive type. In Haskell:
```data Nat = Zero | Succ Nat
```
Let's try the cube version:
```Cube> :load nat.cube
Cube> 2
succ (succ zero)
::
natT
Cube> add 2 3
succ (succ (succ (succ (succ zero))))
::
natT
```
What does the definitions for natural numbers look like?
```Nat :: *;
Nat = forall (natT::*) . natT -> (natT->natT) -> natT;

0 :: Nat;
0 = \ (natT::*) (zero::natT) (succ::natT->natT) -> zero;

Succ :: Nat -> Nat;
Succ n = \ (natT::*) (zero::natT) (succ::natT->natT) -> succ (n natT zero succ);

natprim :: forall (r::*) . (r->r) -> r -> Nat -> r;
natprim r succ zero n = n r zero succ;

add :: Nat -> Nat -> Nat;
add x y = x Nat y Succ;

mul :: Nat -> Nat -> Nat;
mul x y = x Nat 0 (add y);

power :: Nat -> Nat -> Nat;
power x y = y Nat (Succ 0) (mul x);

isZero :: Nat -> Bool;
isZero n = n Bool True (\ a::Bool -> False);

1 :: Nat;
1 = Succ 0;
2 :: Nat;
2 = Succ 1;
3 :: Nat;
3 = Succ 2;
```
The natprim function corresponds to foldr for list and is our means of recursion. This type for natural numbers come with primitive recursion built in, just as the non-recursive data types earlier came with case analysis built in.

I'll skip defining subtraction&co, they are possible, but a little tedious (and very inefficient).

#### Lists

Lists are like a hybrid of natural numbers and the Maybe type. They follow the same pattern as before.
```List :: * -> *;
List e = forall (listT::*) . listT -> (e->listT->listT) -> listT;

Nil :: forall (e::*) . List e;
Nil e = \ (listT::*) (nil::listT) (cons::e->listT->listT) -> nil;

Cons :: forall (e::*) . e -> List e -> List e;
Cons e x xs = \ (listT::*) (nil::listT) (cons::e->listT->listT) -> cons x (xs listT nil cons);
```
And some sample functions.
```foldr :: forall (a::*) (b::*) . (a->b->b) -> b -> List a -> b;
foldr a b f z xs = xs b z f;

map :: forall (a::*) (b::*) . (a->b) -> List a -> List b;
map a b f xs = foldr a (List b) (\ (x::a) (r::List b) -> Cons b (f x) r) (Nil b) xs;

append :: forall (a::*) . List a -> List a -> List a;
append a xs ys = foldr a (List a) (Cons a) ys xs;

foldl :: forall (a::*) (b::*) . (b->a->b) -> b -> List a -> b;
foldl a b f z xs = foldr a (b->b) (\ (x::a) (g::b->b) (v::b) -> g (f v x)) (\ (x::b) -> x) xs z;

reverse :: forall (a::*) . List a -> List a;
reverse a xs = foldl a (List a) (\ (r :: List a) (x :: a) -> Cons a x r) (Nil a) xs;
```
And a test:
```Welcome to the Cube.
Use :help to get help.
Cube> :load bool.cube
Cube> :load nat.cube
Cube> :load list.cube
Cube> :load pair.cube
Cube> :load listmisc.cube
Cube> :load extchar.cube
Cube> :skip
Cube> replicate Char 3 'b'
cons 'b' (cons 'b' (cons 'b' nil))
::
listT
Cube> :quit
```
And with that, I'll quit too for now.

Labels: ,

## Tuesday, November 06, 2007

### Benchmarking ray tracing, Haskell vs. OCaml

On his web site about OCaml Jon Harrop has a benchmark for a simple ray tracing program written in a number of languages. When I saw it I wondered why Haskell was doing so badly, especially since this benchmark was taken as some kind of proof that Haskell performs poorly in "real life". So I have rerun the benchmarks. I've also rewritten the Haskell versions of the programs. The Haskell versions on Jon's web site were OK, but they were too far from the OCaml versions for my taste. I prefer to keep the programs very similar in a situation like this. My rewrite of the benchmarks from OCaml to Haskell was done with a minimum of intelligence. Here are the only things I did that needed creative thought:
1. Use the type Vector to represent vectors instead of a tuple. This allows the components to be strict.
2. Use the type Scene instead of a tuple to represent a scene. The tuple used in the OCaml code uses the dubious feature of equi-recursive types (even Xavier thinks it's strange enough to have a flag to enable it).
3. Rewrite the loop that computes a pixel's value using an accumulating updatable variable into a list comprehension that sums the list.
4. Finally, the compiler flags needed a bit of tweaking to get good performance, even though "-O3 -funbox-strict-fields -fexcess-precision -optc-ffast-math" were pretty obvious.
In addition to this I made the code look a little more Haskellish, e.g., using overloading to allow + and - on vectors. This is really just minor syntactic changes, but makes the code more readable.

To make the program size comparison fair I removed some dead code from the OCaml code.

I then reran the benchmarks using Haskell, OCaml, and C++.

The benchmarks are five programs that starts from very simple ray tracing and specializing the program more and more to speed it up.

The numbers are in the tables below. The time is execution time in second, the characters are non-white characters in the file, and the lines are the number of lines in the file. To ease comparison I also include the relative numbers compared to OCaml (smaller numbers are better).

Interestingly, and unlike Jon's benchmark, the Haskell code is always smaller than the OCaml code. Furthermore, the Haskell code ranges from much faster to slightly faster than the OCaml code. Again, this is very unlike Jon's benchmark. I find the unoptimized version of the benchmark especially interesting since Haskell is 5 times(!) faster than OCaml. I've not investigated why, but I suspect laziness.

#### Results

The programs, ray1-ray5, are variations on the ray tracer as given on Jon's web site. I've used the same size metrics as Jon does.
• Haskell: My Haskell code compiled with ghc 6.8.1
• Haskell old: Jon's Haskell code, compiled with ghc 6.8.1
• Haskell old 6.6: Jon's Haskell code, compiled with ghc 6.1.1
• OCaml: Jon's OCaml code
• C++: Jon's C++ code
• Time: execution time is second
• Char: number of non-white chracters in the program
• Lines: number of lines in the program
• Rel T: execution time relative to OCaml
• Rel C: non-white characters relative to OCaml
• Rel L: lines relative to OCaml
• Mem: Maximum resident memory
 ray1 Time Chars Lines Rel T Rel C Rel L Mem Haskell 15.3 1275 51 0.202 0.990 1.020 5M Haskell, old 15.8 1946 88 0.208 1.511 1.760 9M Haskell, old 6.6 28.1 1946 88 0.370 1.511 1.760 9M OCaml 75.9 1288 50 1.000 1.000 1.000 18M C++ 8.1 2633 122 0.106 2.044 2.440 8M

 ray2 Time Chars Lines Rel T Rel C Rel L Mem Haskell 11.5 1457 50 0.206 0.912 0.943 12M Haskell, old 12.0 2173 99 0.215 1.360 1.868 35M Haskell, old 6.6 21.1 2173 99 0.379 1.360 1.868 35M OCaml 55.8 1598 53 1.000 1.000 1.000 15M C++ 6.1 3032 115 0.108 1.897 2.170 8M

 ray3 Time Chars Lines Rel T Rel C Rel L Mem Haskell 9.7 1794 62 0.970 0.919 0.939 12M Haskell, old 11.1 2312 103 1.112 1.184 1.561 35M Haskell, old 6.6 19.7 2312 103 1.984 1.184 1.561 35M OCaml 10.0 1953 66 1.000 1.000 1.000 15M C++ 5.4 3306 143 0.545 1.693 2.167 8M

 ray4 Time Chars Lines Rel T Rel C Rel L Mem Haskell 8.5 1772 66 0.985 0.867 0.957 12M Haskell, old 11.7 2387 110 1.360 1.168 1.594 36M Haskell, old 6.6 19.2 2387 110 2.235 1.168 1.594 35M OCaml 8.6 2043 69 1.000 1.000 1.000 11M C++ 5.0 3348 149 0.584 1.639 2.159 8M

 ray5 Time Chars Lines Rel T Rel C Rel L Haskell 7.0 2246 95 0.999 0.878 0.950 OCaml 7.0 2559 100 1.000 1.000 1.000 C++ 4.7 3579 142 0.674 1.399 1.420

The source code is available in a Darcs repository.

#### Software and hardware details

Hardware: MacBook, Intel Core Duo 2GHz, 2MB L2 Cache, 1GB 667MHz DRAM

Software:

• Haskell compiler: ghc-6.8.1
• OCaml compiler: 3.10.0
• g++: gcc version 4.0.1 (Apple Computer, Inc. build 5367)
Compilation commands:
• ghc: -O3 -fvia-C -funbox-strict-fields -optc-O3 -fexcess-precision -optc-ffast-math -funfolding-keeness-factor=10
• OCaml: -rectypes -inline 100 -ffast-math -ccopt -O3
• g++: -O3 -ffast-math
Target architecture is x86 (even though the processor is x86_64 capable).

#### Some observations

Haskell should really have the definitions of infinity and epsilon_float in a library. They are quite useful. Also, having them in a library would have made the Haskell code somewhat shorter and faster.

Converting these programs from OCaml to Haskell was very mechanical; it could almost be done with just sed.

I'm glad version 5 of the benchmark didn't show much improvement, because it's a really ugly rewrite. :)

Note that the code is all Haskell98, no strange extensions (even though -funbox-strict-fields deviates subtly from H98).

#### Conclusion

Benchmarking is tricky. I'm not sure why my and Jon's numbers are so different. Different hardware, slightly different programs, different software.

Haskell is doing just fine against OCaml on this benchmark; the Haskell programs are always smaller and faster.

Edit: Updated tables with more numbers.

PS: Phil Armstrong wrote the Haskell code on Jon's web site and I took some code from his original.

Labels: ,