[Caml-list] GADTs + Phantom types

["David Allsopp" <dra-news@metastack.com>]

The premise here is that I've been trying to use polymorphic variants as
phantom types to create subsets of a GADT for certain function calls. It's
working fine - in fact, it's really quite elegant being able to have a GADT
listing a whole load of properties and being able to tag each one as
read-only, write-only or read+write and then have the type checker able to
report whether the wrong constructor is passed to a [get] or [set] function.

The snag is that I've hit a problem when composing these functions - say
trying to call a function that accepts all the constructors using a
parameter which is restricted to a subset of them.

I've tried to play with a few simplified versions to understand the problem
and perhaps be able to explain it in a small example. My first attempt
(without GADTs) looks like this. I define an abstract type T.t allowing me
to tag integer values:

module T :
  sig
    type +'a t
    val create : int -> 'a t
    val get : 'a t -> int
  end =
  struct
    type 'a t = int
    let create x = x
    let get x = x
  end

I then define a function f1:

let f1 : [ `After | `Before ] T.t -> unit =
  fun value -> Printf.printf "Value given: %d\n" (T.get value)

and can pass values to it:

let (dummy : [> `After ] T.t) = T.create 42
in
  f1 dummy

Furthermore, because of the variance annotation, I can define a function f2:

let f2 : [ `After ] T.t -> unit =
  f1 (param : [ `After ] T.t :> [> `After ] T.t)

which allows me to have f2 accepting [ `After ] T.t only but still using f1
(which accepts [ `After ] T.t, [ `Before ] T.t and [ `After | `Before ] T.t
values) as a utility function.

So then I tried applying this to my original problem with GADTs:

type (_, _) t = A : (bool, [< `Before | `After ]) t
              | B : (int, [> `After ]) t
              | C : (string, [> `Before ]) t

let f1 : type s . (s, [ `After | `Before ]) t -> s -> unit = fun attr value
->
  match attr with
    A -> Printf.printf "Bool given: %b\n" value
  | B -> Printf.printf "Int given: %d\n" value
  | C -> Printf.printf "String given: %S\n" value

let f2 : type s . (s, [ `Before ]) t -> s -> unit = fun attr value ->
  f1 attr value

As this code stands, I get a typing error in [f2] because [attr] does not
allow the constructor [ `After ] so it's not a valid parameter for [f1].

So, having scratched my head for a bit as to why (s, [ `Before ]) t was not
a subtype of (s, [ `After | `Before ]) t I remembered variance annotations
and tried changing [t] to be:

type (_, +_) t = ...

But the type checker said "In this GADT definition, the variance of some
parameter cannot be checked".

At which point, rather out my depth, I felt thoroughly morose and deflated
and decided it was time to ask the lovely type experts on this list whether
I'm just being stupid or whether what I'm trying to do is in fact
impossible.

I'd tried not using polymorphic variants as the phantom type, but the
problem is that unlike the classic "readonly/readwrite" example, these
things may readonly, writeonly or readwrite and I couldn't see how you could
code that requirement without using polymorphic variants. I also came across
this thread https://sympa.inria.fr/sympa/arc/caml-list/2012-02/msg00059.html
from last year which means I think I understand why I'm getting that
variance error message - what I couldn't tell is whether the proposed
changes would make the above type work or not. 


David