"ocaml_beginners"::[] ocaml type checker

Hey,

if I write:

let tw f x = f(f(x));;

tw tw tw tw tw tw;;

it typechecks almost instantly (I'm using the interactive toplevel
interpreter here). But when I then write:

tw tw tw tw tw tw tw;;

it takes forever to type-check. I mean literally forever - it runs out
of memory! Now I've just written my own very simple type-checker in
Prolog, and that only takes a few seconds to typecheck the same
expression. Why does ocaml's type checker find this sooooo hard?

Cheers,
John

Messages in this topic (1) Reply (via web post) | Start a new topic

.

I can't answer your question, but note that this has something to do
with the value restriction: the type of (tw tw tw tw tw tw) is
monomorphic [1] and eta-expanding your examples makes the problem
disappear.

# let tw f x = f (f x);;
val tw : ('a -> 'a) -> 'a -> 'a = <fun>;
# tw tw tw tw tw tw ;;
- : ('_a -> '_a) -> '_a -> '_a = <fun>;
# tw tw tw tw tw tw tw ;;
Stack overflow during evaluation (looping recursion?).
# let g x = tw tw tw tw tw tw tw x ;;
val g : ('a -> 'a) -> 'a -> 'a = <fun>;
# let g x = tw tw tw tw tw tw tw tw tw tw tw tw tw tw x ;;
val g : ('a -> 'a) -> 'a -> 'a = <fun>;

Best regards,
Chris

[1] http://caml.inria.fr/pub/old_caml_site/FAQ/FAQ_EXPERT-eng.html#variables_de_types_faibles

On Sat, Mar 29, 2008 at 3:43 PM, john_wicko < jpw48%40cam.ac.uk">jpw48cam.ac.uk> wrote:
&gt; Hey,
>;
> if I write:
&gt;
> let tw f x = f(f(x));;
>
&gt; tw tw tw tw tw tw;;
>;
> it typechecks almost instantly (I'm using the interactive toplevel
> interpreter here). But when I then write:
&gt;
> tw tw tw tw tw tw tw;;
>;
> it takes forever to type-check. I mean literally forever - it runs out
> of memory! Now I've just written my own very simple type-checker in
> Prolog, and that only takes a few seconds to typecheck the same
>; expression. Why does ocaml's type checker find this sooooo hard?
&gt;
> Cheers,
> John
>;
>
> ------------------------------------
&gt;
> Archives up to December 31, 2007 are also downloadable at http://www.connettivo.net/cntprojects/ocaml_beginners/
> The archives of the very official ocaml list (the seniors' one) can be found at http://caml.inria.fr
> Attachments are banned and you're asked to be polite, avoid flames etc.Yahoo! Groups Links
&gt;
>
>
>;

Messages in this topic (2) Reply (via web post) | Start a new topic

.

On Saturday 29 March 2008 21:26:59 Christopher L Conway wrote:
&gt; I can't answer your question, but note that this has something to do
> with the value restriction: the type of (tw tw tw tw tw tw) is
> monomorphic [1] and eta-expanding your examples makes the problem
> disappear.
>
&gt; # let tw f x = f (f x);;
>; val tw : ('a -> 'a) -> 'a -> 'a = <fun>;
> # tw tw tw tw tw tw ;;
> - : ('_a -> '_a) -> '_a -> '_a = <fun>;
> # tw tw tw tw tw tw tw ;;
> Stack overflow during evaluation (looping recursion?).
> # let g x = tw tw tw tw tw tw tw x ;;
> val g : ('a -> 'a) -> 'a -> 'a = <fun>;
> # let g x = tw tw tw tw tw tw tw tw tw tw tw tw tw tw x ;;
> val g : ('a -> 'a) -> 'a -> 'a = <fun>;

Curiously, this is also specific to the top-level. Even the compilers compiled
to bytecode handle it. The value restriction affects the way code is JIT
compiled, which would explain that aspect of this.

--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/products/?e

Messages in this topic (3) Reply (via web post) | Start a new topic

.