Re: [Caml-list] let rec and polymorphic functions

[Jeremy Yallop <jeremy.yallop@ed.ac.uk>]

David Allsopp wrote:
> That does explain it - which I didn't know. Consider this which is also
> broken (and simpler because it has nothing to do with the ad-hoc
> polymorphism of printf)
> 
> let rec id x = x
> and _ = id 0
> in
>   id (); (* *** *)
>   id 1;;
> 
> Gives a type error for *** because id is already inferred as int -> int
> because of the monomorphic nature of the recursive definition. 

Right.  In particular, it gives a type error because `id' is used at the 
type int -> int within its own definition (the rhs of every binding in 
the group), so that's the type that it's given for the rest of the 
program (the part following "in").

> This is
> over-guarded but I never got an answer on a previous post as to why. The
> equivalent SML does type polymorphically:
> 
> let fun id x = x
> val _ = id 0
> in
>   id ();
>   id 1
> end;

This isn't really "the equivalent SML", since the definition of `id x' 
and the application `id 0' aren't in the same recursive group.  The 
equivalent in SML would be something like

    let val rec id = fn x => x
            and _  = id 0
        in
           id ();
           id 1
    end

although this actual program isn't valid; SML only allows syntactic 
function expressions on the rhs of `let rec'.  If you throw in a "fn" to 
avoid the restriction you'll find that SML behaves essentially the same 
as OCaml:

     let val rec id = fn x => x
             and x = fn _ => id 0
         in
           id ();
           id 1
     end



OCaml seems a little inconsistent here, actually.  The application `id 
0' is only valid as the rhs of let rec because the compiler can 
determine that there's no actual recursion involved.  There doesn't seem 
to be a reason not to apply a similar analysis to type checking, 
allowing more polymorphism for functions in the same recursive group 
that aren't actually part of a cycle.

Jeremy.