[Caml-list] Type system infering 'a and '_a
Tom
type 'a t1 = Empty1 | Full1 of 'a
# let a1 = Empty1;;
val a1 : 'a t1 = Empty1
Smart.
type 'a t2 = Empty2 of 'a option ref | Full2 of 'a
# let a2 = Empty2 (ref None);;
val a2 : '_a t2 = Empty2 {contents = None}
The type system won't infer a2 as being polymorphic, as it is mutable.
Smart.
type 'a t3 = Empty3 of string | Full3 of 'a
# let a3 = Empty3 "foo";;
val a3 : 'a t3 = Empty3 "foo"
Even thou a3 is mutable, mutating it can't bind 'a, so a3 is polymorphic.
Smart.
type ('a, 'b) t4 = Empty4 of 'a option ref | Full4 of 'a * 'b
# let a4 = Empty4 (ref None);;
val a4 : ('_a, 'b) t4 = Empty4 {contents = None}
As only 'a is "contained" in a mutable type, a4 is polymorphic only in 'b.
Smart
But now...
type ('a, 'b) t5 =
Empty_a5 of 'a option ref
| Empty_b5 of 'b option ref
| Full5 of 'a * 'b
# let a5 = Empty_a5 (ref None);;
val a5 : ('_a, '_b) t5 = Empty_a5 {contents = None}
Stupid. Value a5 should be polymorphic in 'b!
(And, with a bit of hacking:
type 'a t1 = Empty1 | Full1 of 'a
# let b1 = Full1 (Obj.magic 0);;
val b1 : 'a t1 = Full1 <poly>
Smart.
type ('a, 'b) t4 = Empty4 of 'a option ref | Full4 of 'a * 'b
# let b4 = Full4 (Obj.magic 0, Obj.magic 0);;
val b4 : ('_a, 'b) t4 = Full4 (<poly>, <poly>)
Stupid.
)
So we see that "mutability" of each type variable is defined for the whole
type, not for the individual value constructors only. Is there a theoretical
reason (of course, one reason is probably an easier implementation)?
- Tom
Jacques Garrigue
> But now...
>
> type ('a, 'b) t5 =
> Empty_a5 of 'a option ref
> | Empty_b5 of 'b option ref
> | Full5 of 'a * 'b
>
> # let a5 = Empty_a5 (ref None);;
> val a5 : ('_a, '_b) t5 = Empty_a5 {contents = None}
>
> Stupid. Value a5 should be polymorphic in 'b!
The main role of a type system is not to be smart, just to be correct :-)
So the above sentence should use "could", not "should".
Let's just explain why you get this result.
The decision on how to generalize is made at the level of the let.
If the right hand side contains mutable values creations and/or
function applications, the generalization is made in "safe" mode,
generalizing only covariant type variables in the result type.
This "safe" generalization is done without looking at the definition
itself, so it doesn't know what caused the switch to safe mode.
One can always imagine more clever approaches, like memorizing
variables that cannot be generalized just where the mutable value is
created, rather than decide on a whole-expression basis. In some cases
this would give better types. But this also adds complexity to the
type-checker, which still should be able to generalize this variable
if it is covariant in the final type. And complexity can be the enemy
of correctness, so this is not done currently.
Do you have a concrete example where the above polymorphism is required,
and there is no workaround?
In general there is an (easy) workaround: separate definition of
mutable parts from immutable ones.
# let r = ref None;;
val r : '_a option ref = {contents = None}
# let a5' = Empty_a5 r;;
val a5' : ('_a, 'b) t5 = Empty_a5 {contents = None}
Jacques Garrigue
_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
skaller
> From: Tom <tom.pr...@gmail.com>
> The main role of a type system is not to be smart, just to be correct :-)
Bull! Ordinary variants are correct. Polymorphic variants are SMART :)
Second order polymorphism for class and record fields .. that's
pretty smart too. Particularly the fact it works with the usual
type inference with only minor hiccups (occasionally you need
some coercions).
--
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net