This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

[Caml-list] Y combinator and type-checking
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2004-07-02 (17:36) From: Martin Berger Subject: [Caml-list] Y combinator and type-checking
```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 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

```