[Caml-list] Y combinator and type-checking

[Caml-list] Y combinator and type-checking

[Martin Berger]

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

Re: [Caml-list] Y combinator and type-checking

[Brian Hurt]

On Fri, 2 Jul 2004, Martin Berger wrote:

> 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 );;

This is where your mistake is.  Don't duplicate the type of f.  Instead, 
you should have done:

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

And now it works:
$ ocaml
        Objective Caml version 3.07
 
# let rec y (f : ('a -> 'b) -> 'a -> 'b) : 'a -> 'b = f (fun x -> (y f) 
x);;
val y : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>
#

-- 
"Usenet is like a herd of performing elephants with diarrhea -- massive,
difficult to redirect, awe-inspiring, entertaining, and a source of
mind-boggling amounts of excrement when you least expect it."
                                - Gene Spafford 
Brian

-------------------
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

[Caml-list] Why type infenere enter infinte loop here?

[Andy Yang]

Hi, all

I am relatively new in Ocaml. Perhaps this problem is
trivial. With the following interactive process, ocaml
cannot give out f2's type. Could you tell me why it
cannot?
                                                      
                         
# let rec y f = f (fun x ->(y f) x);;
val y : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>
# let g h x = h x;;
val g : ('a -> 'b) -> 'a -> 'b = <fun>
# let f1 = y g;;
val f1 : '_a -> 'b = <fun>
# let k x = x * x + 1;;
val k : int -> int = <fun>
# let f2 = f1 k;;

Thanks a lot!

Andy


		
__________________________________
Do you Yahoo!?
Yahoo! Mail - 50x more storage than other providers!
http://promotions.yahoo.com/new_mail

-------------------
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

RE: [Caml-list] Why type infenere enter infinte loop here?

[Kevin S. Millikin]

On Tuesday, July 06, 2004 5:25 PM, Andy Yang [SMTP:yyu08@yahoo.com] wrote:
> Hi, all
>
> I am relatively new in Ocaml. Perhaps this problem is
> trivial. With the following interactive process, ocaml
> cannot give out f2's type. Could you tell me why it
> cannot?
>
>
> # let rec y f = f (fun x ->(y f) x);;
> val y : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>
> # let g h x = h x;;
> val g : ('a -> 'b) -> 'a -> 'b = <fun>
> # let f1 = y g;;
> val f1 : '_a -> 'b = <fun>
> # let k x = x * x + 1;;
> val k : int -> int = <fun>
> # let f2 = f1 k;;
>

For the same reason that it does not print the type of

# while true do () done;;

y is a fixpoint combinator.  g is the application combinator (Curry's B 
combinator).  f1 is the fixpoint of application, which does not 
terminating.  Your definition of f1 is the same as

# let f1 = y (fun h x -> h x);;

which is the same as

# let rec f1 = fun x -> f1 x;;

An application of f1 will not terminate.  The typechecker is perfectly h  
appy to determine that your f2 has type 'a -> 'b, but it won't print that 
type until it finishes computing the value.

-- Kevin

-------------------
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