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

["Kevin S. Millikin" <kmillikin@atcorp.com>]

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