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

[Jon Harrop <jon@ffconsultancy.com>]

On Wednesday 27 June 2007 11:24:53 David Allsopp wrote:
> The type-checker doesn't see that surely? Surely on that expression it sees
> out : string -> int -> unit?? Note that changing the sequence to
>
> out "%b" true;
> out "%d" 0;
>
> and removing the out "TEST" still causes problems - although O'Caml manages
> to infer the [format4] first argument for [out], it fixes the first
> parameter of the [format4] as being [bool -> unit] and so prevents [out]
> from being used with anything other than a single "%b" argument and hence
> gives a type error on the next application.

Yes. This is the polymorphic recursion part of your problem. You cannot 
call "f" polymorphically from inside the "let" binding.

Look at this:

# let rec f x = Printf.printf x and g() = f "%d" 3;;
val f : (int -> unit, out_channel, unit) format -> int -> unit = <fun>
val g : unit -> unit = <fun>

Note how "f" has been made specific to the type "int" because of its call 
inside "g".

If you separate the calls (which you can do in this special case) you recover 
the polymorphic "f":

# let rec f x = Printf.printf x;;
val f : ('a, out_channel, unit) format -> 'a = <fun>
# let g() = f "%d" 3;;
val g : unit -> unit = <fun>

The critical difference is whether or not the call to "f" appears inside its 
definition, and that includes inside the body of "g" when "g" is defined at 
the same time as "f" using "let rec". If you want more details, read papers 
about the implementation of non-generalized type variables in the 
Hindley-Milner type system.

I'll try to ossify this by example. You can do:

# let f _ = () in f 0; f "foo";;
- : unit = ()

but not:

# let rec f _ = () and g = f 0; f "foo";;
This expression has type string but is here used with type int

> > Also, recursive calls ossify the function to a monomorphic type, so you
> > cannot do polymorphic recursion in OCaml. There are workaround using
> > recursive modules or objects but I don't think this is what you want
> > here.
>
> 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;;

Exactly, yes.

> Gives a type error for *** because id is already inferred as int -> int
> because of the monomorphic nature of the recursive definition. 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;

No, that is equivalent to the OCaml that does work:

# let f _ = () in f 0; f "foo";;
- : unit = ()

> Incidentally, it's lucky that this is polymorphic in SML because all
> function definitions are recursive IIRC.
>
> But no-one posted an explanation as to why there's this difference in the
> let construct between the two flavours of ML :(

SML does not support polymorphic recursion either:

$ sml
Standard ML of New Jersey v110.62 [built: Thu Feb 22 13:17:37 2007]
- fun f x = f 1; f 1.0; ()
val f = fn : int -> 'a
stdIn:1.16-1.21 Error: operator and operand don't agree [tycon mismatch]
  operator domain: int
  operand:         real
  in expression:
    f 1.0

The reason is basically that both OCaml and Standard ML were designed around 
the Hindley-Milner type system, which made the deliberate design decision to 
push the limits of a decideable type system as far as possible. So they were 
designed to infer as much as possible whilst ensuring that type annotations 
are never required. Polymorphic recursion oversteps this boundary.

The designers of Haskell decided to ditch decideability in favour of (much) 
more power in the type system. So Haskell sometimes requires you to write 
explicit type annotations. Indeed, Haskell programmers almost always write 
type annotations, which is one of the reasons why idiomatic Haskell is 
comparatively verbose.

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