I totally agree -- effects limit the class of protocols you can enforce, 
but I believe (please correct me if I've missed a dirty trick) the 
"simple stuff" still works fine.  For example:

type read;
type write;
type 'a file;
val open_r : string -> read file;
val open_w : string -> write file;
val write : write file -> char -> unit;
val read : read file -> char;
val close : 'a file -> unit;

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.

--Dan

Geoffrey Alan Washburn wrote:
> Dan Grossman wrote:
> 
>> Phantom types are a programming idiom that can often pull off this 
>> sort of thing.
> 
> 
>     Maybe I'm just not smart enough, but I can't seem to think of a way 
> to do this in an effectful language without getting bitten by aliasing.  
> In a purely functional setting, a monadic approach seems plausible, but 
> if you can create a "ref" anywhere, as in OCaml, it seems 
> straightforward to subvert any uses of phantom types for implementing 
> protocols.  I suppose one could look at it from the angle that phantom 
> types make it harder for cooperative users to make mistakes, but I can't 
> see how they can prevent the need for runtime checks.
> 
> _______________________________________________
> 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