Re: [Caml-list] Naming polymorphic variant types -- additional questions

[Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>]

From: "Nick Alexander" <nalexander@amavi.com>
> When I was trying this, I accidently tried:
> type outer = [< 'A | 'B]
> and was duly rewarded with
> Unbound type parameter [..]

OK, [< t] and [> t] types contain an hidden type variable.
If you really want to define a polymorphic type, you must write

   type 'a outer = 'a constraint 'a = [< `A | `B]

Looks a bit confusing? This just means that ('a outer) can unify with
anything included in [< `A | `B]

> I am also a neophyte polymorphic variants user.  It seems very intuitive
> to me that [`A] is a subtype of [`A | `B].  Jacques informs me that
> unification rejects the subtyping in favour of equality.  So, what is the
> situation where [`A] is _not_ a subtype of [`A | `B]?  Ie, what common
> construct, design pattern, or idiom reflects this?

[`A] _is_ a subtype of [`A | `B]. The point is just that in ocaml
subtyping is not implicit, like it is in most OO languages.
     fun (x : [`A]) -> (x :> [`A|`B]) ,
where :> denotes an explicit coercion, is typable, showing the
subtyping relation.

In ocaml, the implicit subsumption relation is instanciation rather
than subtyping. While subtyping makes function arguments
contravariant, with instanciation everything is "covariant", which has
some advantages, but clearly doesn't mix well with subtyping.

Polymorphic variants are based on instanciation: a polymorphic variant
type can be seen as a constraint on the values that may go through
this type. Unification refines it.
Another small point is that in ML quantification only occurs at
toplevel. This means that [< `A | `B] itself is not a closed type, and
that you cannot close it easily.  As a result, you cannot compare it
to [`A], other than say they are unifiable. On the other hand, if you
have a function whose type is All('a). ([< `A | `B] as 'a) -> t  (this
is the meaning of "val f : [< `A | `B] -> t") and another function
whose type is [`A] -> t (here there is nothing to quantify), then you
can see that the first one will accept more inputs, and as a result is
more general then the second one.

Not very clear, but this is the rough idea.

Jacques Garrigue
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners