Type system infering 'a and '_a

[Tom <tom.primozic@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 1594 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 2053 bytes --]