Can type variables be used when writing a type signature for a polymorphic variant type?

Question

I would like to constrain a type variable to allow only polymorphic variant types, such that I could use the variable to construct other polymorphic variant types in a signature:

type 'a t
val f : 'a t -> [`Tag | 'a] t

Is there a way to accomplish this in OCaml? Perhaps using classes/objects instead? A naive attempt failed to compile:

type 'a t = { dummy: int } constraint 'a = [>]

let f : 'a t -> ['a | `Tag] t = fun _ -> { dummy = 0 }
                 ^^

The type [> ] does not expand to a polymorphic variant type

Reason for the question:

I want to use the type signature to reflect capabilities of a t statically, to enforce that a t without a given capability can never be used inappropriately.

val do_something_cool : [<`Super_power] t -> unit
val do_something_else : [<`Super_power|`Extra_super_power] t -> unit
val enhance : 'a t -> ['a | `Super_power] t
val plain_t : [`Empty] t

let () = plain_t |> do_something_cool (* fails *)
let () = plain_t |> enhance |> do_something_cool (* succeeds *)
let () = plain_t |> enhance |> do_something_else (* succeeds *)

Obviously there are other ways to achieve this compile-time safety. For example, enhance could just return a [`Super_power] t that could be used in place of plain_t where required. However, I'm really curious whether the first way could succeed. I am writing a DSL which would be a lot more concise if all the capabilities of t could be reflected in its type.

octachron octachron · Accepted Answer · 2019-03-09T19:50:15

The short answer is no: it is only possible to inline type declarations, not type variables. In other words, this is fine:

type on = [`On]
type off = [`Off]
type any = [ on | off ]
let f: [< any ] -> _ = fun _ -> ()

but not this

let merge: 'a -> 'b -> [ 'a | 'b ] = ...

However, if you only have a closed set of independent capabilities, it might work to switch to an object phantom type where each capacity correspond to a field and each field can be either on or off. For instance,

type +'a t constraint 'a = < super: [< any ]; extra: [< any ]>

Then consumer functions that only require a conjunction of capabilities are relatively easy to write:

val do_something_cool : < super:on; ..>  t -> unit
val do_something_extra : < extra:on; ..> t -> unit
val do_something_super_but_not_extra: <super:on; extra:off; .. > t -> unit

but switching a capability on or off is more complex and fixes the set of capabilities:

val enhance : < super: _; extra: 'es > t -> < super: on; extra:'es > t

Beyond those limitations, everything works as expected. For instance, if I have a variable x

 val x: <super: off; extra:on > t

This works:

 let () = do_something_extra x

whereas

 let () = do_something_cool x

fails and finally

 let () =
   let x = enhance x in
   do_something_cool x; do_something_extra x

works fine too.

The main issue is thus writing the enable function. One trick that may help is to write helper type to manipulate more easily a subset of capabilities. For instance, if I have a complex type:

type 'a s
  constraint 'a = < a: [< any]; b:[< any]; c: [< any ]; d: [< any] >

I can use the following type:

type ('a, 'others) a = < a:'a; b:'b; c:'c; d: 'd>
  constraint 'others = 'b * 'c * 'd

to select the capability a, and thus write

val enable_a: (_,'rest) a s -> (on, 'rest) a s

without having to explicit the three type variables hidden in 'rest.

Can type variables be used when writing a type signature for a polymorphic variant type?

1 Answers