Re: [Caml-list] Unexpected '_a problem

[Alain Frisch <Alain.Frisch@inria.fr>]

Remi Vanicat wrote:
> But for a reson I don't
> fully understood, one cannot do:
> 
> # let f () (_ : 'a -> unit) = ();;
> val f : unit -> ('a -> unit) -> unit = <fun>
> # f ();;
> - : ('_a -> unit) -> unit = <fun>


See the paper _Relaxing the value restriction_ by Jacques Garrigue (
http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/morepoly-long.pdf
), page 15: dangerous type variables (which are not generalized when the
right-hand side of the let-binding is not a value) are not only those is
contravariant position - this would be enough to ensure type soundness -
but also those which appear in a contravariant branch (e.g. anywhere on
the left of an arrow) - this is necessary to ensure that the type system
has principal types.

Let me reformulate the example given in the paper. Consider the
top-level binding:

let f = print_newline (); fun x -> raise Exit

Semantically, it would be sound to give g a polymorphic type:
\forall 'a,'b. 'a -> 'b. However, the relaxed value restriction does not
try to be that clever; it decides which variables to generalize only by
looking at the type of the bound expression (when it is not a
syntactical value). Here are two possible types for the expression:

'a -> 'b
('c -> 'd) -> 'b

Generalizing all variables in covariant positions would give these two
type schemes:

\forall 'b.    'a -> 'b           ('a monomorphic)
\forall 'b,'c. ('c -> 'd) -> 'b   ('d monomorphic)

The only type-scheme which is more general than these two
would be \forall 'a,'b. 'a -> 'b, but this one is not ok (a
contravariant variable has been generalized).

To retrieve principality, the type system has been designed so that
the variable 'c above would not be generalized (it is on the left of an
arrow), which makes the type scheme \forall 'b. ('c -> 'd) -> 'b
less general than \forall 'b. ('a -> 'b) (which is the principal type
scheme inferred by OCaml).


-- Alain