Sunday, April 10, 2005

 

On second thought..

Well, I was doing pretty well with the lambda-calculus-in-ocaml thing until I tried to define XOR for Church booleans. I defined it as:
λa.λb.a (not b) b

I worked this out on paper and it seems to be correct. It fails when I define it in OCAML as:
let xorx = fun a b -> a (notx b) b;;

When I say it fails, I mean that I get a type error when I try something like this:
(xorx fls tru) "true" "false"
(or if I just call my print_cbool function). It works if I define xorx as:
let xorx = fun a b -> a (notx b) (b tru fls);;
Since b is supposed to be a boolean, (b tru fls) should be redundant.

A patient gentleman on the #ocaml channel tried to explain to me why OCAML wasn't good for doing Church booleans, but when I started hearing terms like "predicative polymorphism" and "prenex normal form" I realized that I wasn't going to understand the explanation. I hope I will understand some of these terms better by the time I finish Types and Programming Languages.

Comments:
If you try

let tru = fun (a: 'a) (b: 'a) -> a;;
let fls = fun (a: 'a) (b: 'a) -> b;;
let notx = fun (a: 'a->'a->'a) -> a fls tru;;
let xorx = fun (a: 'a) (b: 'a) -> a (notx b) b;;

you get a more readable error.

OCaml is typed so you need to find types for the untyped lambda terms. You may say a boolean has type 'a -> 'a -> 'a, i.e. it is something that takes two things of whichever type and return one of them. But the problem is that one of those two things can be a boolean, so you need to somehow convince the type system that:

'a = 'a -> 'a -> 'a

... and that certainly looks odd to OCaml. In this case you need to convince it that the argument of notx and its result have the same type. One tool you could use is this function:

let u = fun (x: 'a) -> (fun (a: 'a) (b: 'a) -> x);;

It has the type 'a->('a->'a->'a). I think you can't get something with the type ('a->'a->'a)->'a. Anyway the definition of notx changes to:

let notx = fun (a: 'a->'a->'a) -> u (a fls tru);;

And now you can define:

let xorx = fun (a: 'a) (b: 'a) -> (u a) (notx b) b;;

But its type already got obscenely big. In a typed environment one would expect xor to have the type:

bool->bool->bool

But since in lambda calculus we have

bool = bool->bool->bool

In order to define it in a typed environment we need a couple of expansions that replace the lhs with the rhs of the equality above.

Now the definition looks more uniform: it uses a general tool (the function u) and all boolean types are expanded the same number of times. In other words the result of xorx has the same type as the arguments, which certainly makes it easier to reason about.

You still can print it of course. You can print

'a->'a->'a

But now we need a function to print:

('a->'a->'a)->('a->'a->'a)->('a->'a->'a)

One (ugly) way to write it is:

let pp = fun x -> x (fun _ _ -> "true") (fun _ _ -> "false") "" "";;

Depending on how many operations we do, the booleans have an "order" because of the types. That order is the number of expansions we need to do to get their type. Note that we need some care to organize the booleans in such layers, i.e. to dissallow types like:

('a->'a->'a)->'a->('a->'a->'a)

with "partial expansions". We must introduce "u" operations so that the number of operations that act on a boolean in an expression is the same for all booleans in that expression.

For each such order we need a specialized print to "see the boolean".

I hope you can make some sense out of this unorganized comment.
 
Post a Comment

<< Home

This page is powered by Blogger. Isn't yours?