Type system infering 'a and '_a

Type system infering 'a and '_a

[Tom]

[-- 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 --]

Re: [Caml-list] Type system infering 'a and '_a

[Jacques Garrigue]

From: Tom <tom.primozic@gmail.com>

> 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

Re: [Caml-list] Type system infering 'a and '_a

[skaller]

On Thu, 2006-09-14 at 09:24 +0900, Jacques Garrigue wrote:
> From: Tom <tom.primozic@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