Empty polymorphic variant type

Empty polymorphic variant type

[Till Varoquaux]

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

to could express as closed type 3 of 4 possible case, the one where
you have neither read nor write access cannot be expressed.

One could use objects as phantom types:

type 'a account constraint 'a = <..>;;

but this solution is just not as elegant. Any other ideas?

Till
-- 
http://till-varoquaux.blogspot.com/

Re: Empty polymorphic variant type

[Till Varoquaux]

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 ];;
>
> to could express as closed type 3 of 4 possible case, the one where
> you have neither read nor write access cannot be expressed.
>
> One could use objects as phantom types:
>
> type 'a account constraint 'a = <..>;;
>
> but this solution is just not as elegant. Any other ideas?
>
> Till

Small addendum:

type 'a account constraint 'a = [< `Permission |`Read | `Write > `Permission ];;

would work but it seems clunky and convoluted.

Till
> --
> http://till-varoquaux.blogspot.com/
>



-- 
http://till-varoquaux.blogspot.com/

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

[Bünzli Daniel]

Le 6 févr. 08 à 13:24, Till Varoquaux a écrit :

> would work but it seems clunky and convoluted.

Still clunky but what about

type permission_kind = [ `Read | `Write ]
type 'a account contraint 'a = [< `None | `Some of [<  
permission_kind]];;

Best,

Daniel

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

[Till Varoquaux]

It looks a little nicer but breaks the subtyping: [`None] is not a
subtype of [>`Some [>`Readable]] so you now have to write the
type readonly as: [< `None | `Some of [`Read] ] t if you want it to
unify with [`None].

I'm not sure this is a huge benefit

Till


On Feb 6, 2008 12:33 PM, Bünzli Daniel <daniel.buenzli@erratique.ch> wrote:
>
> Le 6 févr. 08 à 13:24, Till Varoquaux a écrit :
>
> > would work but it seems clunky and convoluted.
>
> Still clunky but what about
>
> type permission_kind = [ `Read | `Write ]
> type 'a account contraint 'a = [< `None | `Some of [<
> permission_kind]];;
>
> Best,
>
> Daniel
>
>



-- 
http://till-varoquaux.blogspot.com/

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

[Christophe TROESTLER]

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