Unexpected '_a problem
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20060802 (07:00) 
From:  Alain Frisch <Alain.Frisch@i...> 
Subject:  Re: [Camllist] Unexpected '_a problem 
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.kyotou.ac.jp/~garrigue/papers/morepolylong.pdf ), page 15: dangerous type variables (which are not generalized when the righthand side of the letbinding 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 toplevel 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 typescheme 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