I believe
http://arxiv.org/abs/cs.PL/0403034
is relevant, claiming that phantom types can encode any first-order 
subtyping hierarchy.

If I recall correctly, you force the client to provide "witnesses" 
(i.e., coercions), which to answer a later question in the thread, is 
how you can support things like passing a "read_write" file handle to 
read.  That is, you have a functions like:

val up_to_read : read_write file -> read file
val up_to_write : read_write file -> write file

These are the identity function and we can expect cross-module inlining 
to remove them.

--Dan

Geoffrey Alan Washburn wrote:
> Dan Grossman wrote:
> 
>> It enforces that you don't confuse your reads and writes, but *not* 
>> that you don't use a file after you close it.  A monadic approach 
>> (where each operation would return a "new" file) or linearity appears 
>> necessary for the latter.
> 
> 
>     Okay, good point.  However, that raises the interesting question of 
> whether there is a nice positive specification of the class of 
> "protocols" that are expressible in the presence of effects, rather than 
> a negative characterization -- all those that can be broken by aliasing, 
> nontermination, etc.
> 
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs