Re: [Caml-list] '_a

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: Mike Hamburg <hamburg@fas.harvard.edu>
Subject: [Caml-list] '_a
Date: Wed, 26 Jan 2005 19:19:16 -0500

> The appearance of '_a in places where it shouldn't appear causes some 
> annoyance, and a good deal of confusion among beginners to O'Caml.  In 
> particular, List.map (fun x -> x) "ought to" have type 'a list -> 'a 
> list, whereas it instead has type '_a list -> '_a list.
> 
> Some types are treated specially for creation of '_a, such as refs and 
> arrays.  For instance, if you have the following two declarations:
> 
> # let a = let f x () = [x] in f [];;
> val a : unit -> 'a list list = <fun>
> # let b = let f x () = [|x|] in f [];;
> val b : unit -> '_a list array = <fun>
> 
> Although I haven't read the code for O'Caml, I deduce from this that 
> there is deep magic in place to determine when to turn 'a into '_a, and 
> in many cases, the heuristic is wrong (in the conservative direction: 
> in this case, 'a should not be turned into '_a until b is applied).

There is no deep magic, no heuristics. There is just a type system
which guarantees type soundness (i.e. "well typed programs cannot
produce runtime type errors").

If you want the type system and all the historical details, read my
paper "Relaxing the value restriction" at
  http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/

In a nutshell, ocaml uses an improvement of the value restriction.
With the value restriction, only definitions which are syntactical
values (i.e. that do not call functions, etc when defined) are allowed
to contain polymorphic type variables.
This is improved by allowing covariant type variables to be
generalized in all cases. Your first example is ok, because list is a
covariant type, but your second fails, because array is not (you may
assign to an array, and you would have to look at the code to see that
each call to b creates a different array)

Of course, one could think of many clever tricks by looking
at what the code actually does. The above paper describes some of the
"crazy" things Xavier Leroy and others tried in the past, which
actually subsume your ideas, before they all decided this was too
complicated. The main reason is that, if something is going to break
at module boundaries, then it is not really useful.

Good reading,

Jacques Garrigue