[Caml-list] Y combinator and type-checking

[Martin Berger <martinb@dcs.qmul.ac.uk>]

i just noticed something confusing: consider an implementation of the
Y combinator (for a CBV language):

     let rec y f = f (fun x -> (y f) x );;

let's see what ocaml says about this definition.

     # let rec y f = f (fun x -> (y f) x );;
     val y : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>

now i annotate the definition above with the types just
inferred:

     let rec y  ( f : ( 'a -> 'b ) -> 'a -> 'b )
            : ( ( 'a -> 'b ) -> 'a -> 'b ) -> 'a -> 'b
       = f (fun x -> (y f) x );;

suddenly, ocaml complains:

     #let rec y  ( f : ( 'a -> 'b ) -> 'a -> 'b )
              : ( ( 'a -> 'b ) -> 'a -> 'b ) -> 'a -> 'b
         = f (fun x -> (y f) x );;

     This expression has type 'a -> 'b -> 'c but is here used with
     type (('a -> 'b -> 'c) -> 'a -> 'b -> 'c) -> 'a -> 'b -> 'c


why would annotating a program with seemingly correct types render
a program untypable? this is my main question.

here's a related observation: if we run the last program under "ocaml
-rectypes" instead of just "ocaml" we get

     # let rec y  ( f : ( 'a -> 'b ) -> 'a -> 'b )
              : ( ( 'a -> 'b ) -> 'a -> 'b ) -> 'a -> 'b
         = f (fun x -> (y f) x );;
     val y :
     (((('a -> ('a -> 'b as 'b)) -> 'a -> 'b as 'a) -> 'b) -> 'a
     -> 'b) -> 'a -> 'b = <fun>

so now the typechecker gives a thumbs-up, but the inferred and annotated
types differ. why?

I hope this is not a well-known beginners issue!

martin

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners