I was playing a bit with Ocaml type system the other day...
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