[Camllist] Y combinator and typechecking
 Martin Berger
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20040702 (17:36) 
From:  Martin Berger <martinb@d...> 
Subject:  [Camllist] Y combinator and typechecking 
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 thumbsup, but the inferred and annotated types differ. why? I hope this is not a wellknown beginners issue! martin  To unsubscribe, mail camllistrequest@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/camlbugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners