Re: [Caml-list] Type inference question

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

From: Mark Shinwell <Mark.Shinwell@cl.cam.ac.uk>

> However, in the Marshal example above, we have
> 
> 	Marshal.from_channel stdin []
> 
> in the first part of the "let".  In the SML terminology, this is not a
> "nonexpansive expression"[*] (unlike "fun x -> x").  Therefore, I would
> have thought that the appearance of such an expression here would
> prohibit generalisation (in order to prevent possible unsoundness in the
> presence of mutable state).  This is presumably not the case in OCaml:
> can someone explain why?

Because ocaml now uses an improvement of the so-called "value restriction".
Rather than refusing to generalize any variable in expansive
expressions, it generalizes covariant ones, as they cannot be
used in an unsound way.
(See "Relaxing the value restriction" at
 http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/)

What we see here is a consequence of that for functions which
are known as typing holes: any function that returns a totally
unconstrained result (as input_value or Obj.magic) allows this result
to be generalized. Actually, for Obj.magic this is a good thing: you
sometimes want the result to be polymorphic (this is not a real
function anyway). For input_value this is subject for discussion, but
anyway this function is a glaring hole in the type system... maybe we
should have a way to explicitly require its result to be annotated
with a ground type!

Jacques Garrigue