Re: [Caml-list] phantom types and identity function

[Gabriel Scherer <gabriel.scherer@gmail.com>]

On Wed, Nov 28, 2012 at 4:42 AM, Ivan Gotovchits <ivg@ieee.org> wrote:
> And now I'm confused much more =). Please, could you explain the
> relevance between subtyping and type restriction?

I was reacting mostly to Jacques' remark that "you cannot even use
subtyping for that".

The relation between subtyping and "constraint" is as explained in the
manual excerpt I quoted. The following is valid:
  type 'a t = {x : 'a} ;;
  let f x = (x : [ `A ] t :> [ `A | `B ] t);;

but the following is not:
  type 'a t = {x : 'a} constraint 'a = [< `A | `B ];;
  let f x = (x : [ `A ] t :> [ `A | `B ] t);;
    Error: Type [ `A ] t is not a subtype of [ `A | `B ] t
    The first variant type does not allow tag(s) `B

The reason for this behavior is that in the first case, t was inferred
covariant, while the presence of a constraint disables variance
inference (in the manual: "otherwise (ie. [...] for non-free
parameters) the variance must be given explicitly)"). You can make the
constrained version work with an explicit variance annotation:
  type +'a t = {x : 'a} constraint 'a = [< `A | `B ];;
  let f x = (x : [ `A ] t :> [ `A | `B ] t);;

Finally, while in this example 'a occurs positively in ('a t), in your
example 'a did not occur at all. In this case it is correct to coerce
from (foo t) to (bar t), whatever the type expression (foo) and (bar)
are -- they don't need to be in a subtyping relation. The following
works:
 type 'a t = { x : int };;
 let f x = (x : [ `A ] t :> [ `B ] t);;

I'm calling this form of variance "irrelevant" to highlight that the
parameter can simply be ignored when checking for subtyping (some
people call it "nonvariant", but it's kind of awkward if you already
use "invariant" for the opposite notion of appearing both in positive
and negative position).
The OCaml type checker can use some restricted form of it (eg. the
previous example), but you cannot abstract over it: there is no
variance annotation to express that.

Jacques' workaround replaces the definition of a new constrained type
with a constrained type synonym, that is not checked using variance
but direct expansion. But that works because you know what the
definition  expands to. In general there may be situation when you
want to say "type 'a t, where 'a is not used" but not expose a
(potentially abstract) non-parametrized type u such that "type 'a t =
u".


While we're at it: are you sure you need to play with phantom
polymorphic variant types now that we have GADTs? I have used phantom
types in the past, but my personal use cases would be profitably
rewritten using GADTs. They tend to produce hairy error messages, but
phantom polymorphic variants are not better in this regard.