Re: [Caml-list] Re: Empty polymorphic variant type

[Christophe TROESTLER <Christophe.Troestler+ocaml@umh.ac.be>]

On Wed, 6 Feb 2008 12:24:21 +0000, Till Varoquaux wrote:
> 
> On Feb 6, 2008 12:16 PM, Till Varoquaux <till.varoquaux@gmail.com> wrote:
> > Polymorohic variants are great to encode permissions as phantom types.
> > This usage is hindered by the apparent impossibility to declare the
> > empty polymorphic type.
> >
> > To illustrate this use case I'll take a bogus example: suppose one is
> > handling accounts, you might want to be able to add a permission on
> > private information (NIN, passwords etc..). So you could be handling
> > accounts where you'd have read permission, write permission both or
> > none. By using a polymorphic variant type:
> >
> > type 'a account constraint 'a = [< `Read | `Write ];;
> >
> Small addendum:
> 
> type 'a account constraint 'a = [< `Permission |`Read | `Write > `Permission ];;
> 
> would work but it seems clunky and convoluted.

The empty polymorphic type may be declared with the camlp5 revised
syntax but does not behave as a universal polymorphic variant
subtype :

  $ cat a.ml
  type account 'a = 'b constraint 'a = [ < `Read | `Write ];
  type t = account [= ];
  
  $ ocamlc -pp camlp5r a.ml
  File "a.ml", line 2, characters 17-21:
  This type [  ] should be an instance of type [< `Read | `Write ]
  These two variant types have no intersection

IMHO I guess your best solution for readability (at least in the code
you write, not always for the generated types) ATM is to define type
aliases:

  type 'a account constraint 'a = [< `None |`Read | `Write > `None ]
  type none = [ `None ]
  type read = [ `None | `Read ]
  type write = [ `None | `Write ]

Then you can have :

  val x : [> read] account
  val y : [> write] account
  # [x; y; z];;
  - : [ `None | `Read | `Write ] account list = [<abstr>; <abstr>; <abstr>]
  # let f (x : [< read ] account) = ...
  # let g (x : [ read | write ] account) = ...

My 0.02€,
ChriS