Re: [Caml-list] Phantom types and read-only variables

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: Markus Mottl <markus.mottl@gmail.com>

> Hm, it seems to me that the compiler could do a better job here.
> 
> Instead of writing:
> 
>   type 'a t = { mutable value: int }
> 
> write:
> 
>   type v = { mutable value: int }
>   type 'a t = v
> 
> This should make the code compile.

Indeed, by doing that you make t extensible to a type that drops the
type parameter, meaning that type inference will never try to unify
the parameter.

A more direct way would be to define

  type 'a t = int ref

Alternatively, you could just slightly change the definition of
freeze, to allow dropping the parameter

  # type 'a t = { mutable value: int } ;;
  # let freeze ({value=_} as v) = v ;;
  val freeze : 'a t -> 'b t = <fun>

> I think the compiler should be able to infer automatically that 'a isn't
> used on the right hand side of the record definition (i.e. that it is
> just a phantom type) without using the hint of a separate monomorphic
> record definition.  I guess this feature should be trivial to add.
> Maybe in the next release? :-)

Actually, this is a bit problematic.
Types defined as abbreviations are automatically expanded during
unification, so that unused parameters disappear.
But datatypes cannot be expanded, so their parameters are going to be
unified. Avoiding it would mean checking whether the parameters appear
in the real definition during unification. This is possible, but would
change the semantics of unification, something you want to be careful
about.

Actually ocaml 3.09 will go in the somehow opposite direction:
allowing private types to behave as phantom types. Currently private
types have their variance automatically inferred from their
definition, meaning you can use the above subtyping trick even after
the type is made private, but considering the fact they are
semi-abstract, it seems more natural to require their variance to be
explicitly given, allowing one to disallow such subtyping.

Jacques Garrigue