Browse thread
RE: [Caml-list] Why type infenere enter infinte loop here?
- Kevin S. Millikin
[
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: | -- (:) |
| From: | Kevin S. Millikin <kmillikin@a...> |
| Subject: | RE: [Caml-list] Why type infenere enter infinte loop here? |
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