The following message is a courtesy copy of an article
that has been posted to comp.lang.functional as well.

Shaddin Doghmi <shaddin@mitre.org> writes:

> What is the difference between double corcion and single coersion? what 
> can double coercion do that single coercion cant?

Lots of things :-)
In a single coercion, the expected type is directly built from the
target type in a predefined way. The algorithm attempts to be clever,
but if the target type is recursive, or already has a polymorphic
structure, there is no unique most general expected type. Moreover,
there are extra restrictions to avoid a blow-up in type inference
time, namely left hand sides of arrows are not available for subtyping
(but other contravariant types are...)

Here are typical examples involving polymorphic variants

fun x -> (x :> [`Nil | `Cons of 'a * 'b] as 'b)
- : [< `Cons of 'b * ([ `Cons of 'a | `Nil ] as 'c) as 'a | `Nil ] -> 'c
Note that the expected type has only been partially open.

fun x ->
  (x : [< `Nil | `Cons of 'a * 'b] as 'b :> [`Nil | `Cons of 'a * 'c] as 'c)
With a double coercion we can get recursion on the expected side.

fun x ->
  (x : [< `Nil | `Cons of 'a * 'b] as 'b :> [> `Nil | `Cons of 'a * 'c] as 'c)
This wouldn't work with a single coercion, as the target is polymorphic.

If there is no recursion, you can get this last effect through dispatch:
function `None | `Some _ as x -> x
- : [< `None | `Some of 'a ] -> [> `None | `Some of 'a ]

> Also, there doesnt seem to be any good detailed references for 
> polymorphic variants. Both the ocaml manual and the oreilly book dont 
> mention lots of details. Anybody know of any good references?

See my publications for examples and theory with polymorphic variants.
In particular the paper on code reuse is a good introduction, and the
syntax is (almost) the current one.

http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/

There is a very small bit on coercions in "Programming with ..."
(which uses an older syntax, by the way).
Basically they work just like for object types, which get a reasonably
detailed account in the reference manual. The main differences are
that (1)there is no concept of class type with variants, so you always
need double coercions to introduce recursion, and (2)with polymorphic
variants a closed type vt has both a polymorphic subtype [< vt] and a
polymorphic supertype [> vt], while an object type has only a subtype
#vt.

P.S. I forward to the caml-list to be in the logs...

---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>

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