This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

Re: [Caml-list] let rec and polymorphic functions
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2007-06-27 (13:18) From: Jon Harrop Subject: Re: [Caml-list] let rec and polymorphic functions
```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

```