'_a

[Mike Hamburg <hamburg@fas.harvard.edu>]

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).

The cause of the problem is that programs may create a closure with a 
mutable variable of type 'a, which if we were to let 'a generalize 
could be replaced with a subtype 'b of 'a, and then used as another 
subtype 'c of 'a, which would be unsafe.

As a fix, I propose the following: the type system should keep track of 
where a mutable or immutable reference to a polymorphic variable with 
type parameter 'a is created on the stack.  Call these places [m'a] and 
[i'a].  For example, ref should have type 'a -> [m'a] 'a, and ref [] 
should have type [m'a] 'a (which is equivalent to the current '_a).  I 
don't propose that the printing should show this complexity, just as it 
hides whatever heuristic O'Caml is using now, except in the case where 
there is a mutable reference at top level, in which case it should 
convert 'a to '_a.

Of course, module interfaces shouldn't have to show when they keep 
references to things, so we probably can't do much about applying 
List.map to the identity without modifying List (for instance, what if 
List.map decided to memoize the function fed into it using a hash 
table?).

Is this a reasonable idea?  If so, can someone give me a pointer on how 
to go about implementing it (or proving that it is type-safe with 
appropriate unification rules?)?

Mike