[Caml-list] GADTs + Phantom types

[Caml-list] GADTs + Phantom types

[David Allsopp]

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 

Re: [Caml-list] GADTs + Phantom types

[Gabriel Scherer]

In fact, you can write a coercion function by hand (because in fact it
is sound to declare the parameter covariant in your type-declaration,
but the type-checker doesn't see that):

# let coerce : type a . (a, [ `Before ]) t -> (a, [ `Before | `After
]) t = function A -> A | C -> C;;
val coerce : ('a, [ `Before ]) t -> ('a, [ `After | `Before ]) t = <fun>

I personally try to avoid using polymorphic variants as phantom types
when I use GADTs. The two features are subtle enough in isolation to
become a potential nightmare when put together. Given that GADTs allow
a cleaner approach than phantom types, I would encourage you to try
GADT-using, polymorphic-variant-free approaches.

(Of course that doesn't negate the usefulness of polymorphic variants
when actually used as values, instead of weird type-level stuff only.)

type tag_b = TagB
type tag_a = TagA
type tag_c = TagC

type (_, _) t =
  | A : (bool, tag_a) t
  | B : (int, tag_b) t
  | C : (string, tag_c) t

type _ before =
  | BA : tag_a before
  | BC : tag_c before

type _ after =
  | AA : tag_a after
  | AB : tag_b after

let f1 : type s tag . (s, tag) t * s -> unit  = function
  | A, b -> if b then ()
  | B, i -> if i = 0 then ()
  | C, s -> if s = "" then ()

let f2 : type s tag . tag before * (s, tag) t * s -> string = function
  | BA, A, b -> string_of_bool b
  | BC, C, s -> s


On Wed, Jul 3, 2013 at 3:59 PM, David Allsopp <dra-news@metastack.com> wrote:
> 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
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

RE: [Caml-list] GADTs + Phantom types

[David Allsopp]

Thanks for looking at this...

Gabriel Scherer wrote:
> In fact, you can write a coercion function by hand (because in fact it is
> sound to declare the parameter covariant in your type-declaration, but the
> type-checker doesn't see that):
> 
> # let coerce : type a . (a, [ `Before ]) t -> (a, [ `Before | `After
> ]) t = function A -> A | C -> C;;
> val coerce : ('a, [ `Before ]) t -> ('a, [ `After | `Before ]) t = <fun>

The problem with that in my actual use case the type is buried inside a list - so that effectively requires the list to be copied just to coerce each value to the other type. There are also a large number of constructors and other options in addition to `Before and `After! It's a lot of code just for a type coercion...

When you say that the type checker can't see that the covariant declaration is sound, is it one of those instances from your previous thread where you'd reckoned that the type-checker *could* be altered to see it, but the current implementation doesn't or is it not possible in general for it to detect that kind of declaration?

> I personally try to avoid using polymorphic variants as phantom types when
> I use GADTs. The two features are subtle enough in isolation to become a
> potential nightmare when put together.

Actually, I think that's the best lesson here, thanks! :o) While the initial functions are straightforward, it seems complexity is always lurking around the corner as soon as you try to combine them.

> Given that GADTs allow a cleaner
> approach than phantom types, I would encourage you to try GADT-using,
> polymorphic-variant-free approaches.
> 
> (Of course that doesn't negate the usefulness of polymorphic variants when
> actually used as values, instead of weird type-level stuff only.)
> 
> type tag_b = TagB
> type tag_a = TagA
> type tag_c = TagC
> 
> type (_, _) t =
>   | A : (bool, tag_a) t
>   | B : (int, tag_b) t
>   | C : (string, tag_c) t
> 
> type _ before =
>   | BA : tag_a before
>   | BC : tag_c before
> 
> type _ after =
>   | AA : tag_a after
>   | AB : tag_b after
> 
> let f1 : type s tag . (s, tag) t * s -> unit  = function
>   | A, b -> if b then ()
>   | B, i -> if i = 0 then ()
>   | C, s -> if s = "" then ()
> 
> let f2 : type s tag . tag before * (s, tag) t * s -> string = function
>   | BA, A, b -> string_of_bool b
>   | BC, C, s -> s

I don't follow here the equivalence to my original example - this requires that BA or BC in the call which kind of negates the point that all of the checking is embedded in the type system. However, what it did show me was that I was missing an obvious trick to allow for tagging both `Before and `After which is to have the tags:

type 'a connect
type before = A
type after = B

and then the GADT can be written:

type (_, _) t = A : (bool, _ connect) t
              | B : (int, after connect) t
              | C : (string, before connect) t

and then with a few more type variables in [f1] and [f2] you can have:

let f1 : type s a . (s, a connect) 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 connect) t -> s -> unit = fun attr value ->
  f1 attr value


David

Re: [Caml-list] GADTs + Phantom types

[Jacques Garrigue]

On 2013/07/04, at 2:11, David Allsopp <dra-news@metastack.com> wrote:
> type (_, _) t = A : (bool, [< `Before | `After ]) t
>              | B : (int, [> `After ]) t
>              | C : (string, [> `Before ]) t
> 
> Gabriel Scherer wrote:
>> In fact, you can write a coercion function by hand (because in fact it is
>> sound to declare the parameter covariant in your type-declaration, but the
>> type-checker doesn't see that):
>> 
>> # let coerce : type a . (a, [ `Before ]) t -> (a, [ `Before | `After
>> ]) t = function A -> A | C -> C;;
>> val coerce : ('a, [ `Before ]) t -> ('a, [ `After | `Before ]) t = <fun>
> 
> When you say that the type checker can't see that the covariant declaration is sound, is it one of those instances from your previous thread where you'd reckoned that the type-checker *could* be altered to see it, but the current implementation doesn't or is it not possible in general for it to detect that kind of declaration?

Actually, this coercion shows something else: that your phantom parameter doesn't work like a phantom parameter anymore. Now it is a constraint associated with the constructor, and you can change the parameter by copying the constructor. This may be what you want (it guarantees some invariant), or this may be not (all the properties must be expressed by the constraint, otherwise they will be lost on copying).

As for the soundness, this only comes from the fact the constructors have no value arguments, so anything would be sound anyway. And if you allow marking the second parameter as covariant, you would actually get a behavior different from what to expect: pattern matching (a,b) t against A would only tell you that b must be a supertype of [< `Before | `After], whose meaning is not very clear to me.

Last, as Gabriel mentioned, GADTs and polymorphic variants do not play very well together.
In particular, incremental refinement is not guaranteed to work as expected.

But, if what you want is a combination of GADT and phantom types, you can still do it by exporting t as private:

module T : sig
  type (_, +_) t = private
    | A : (bool, _) t
    | B : (int, _) t
    | C : (string, _) t
  val a : (bool, [< `Before | `After]) t
  val b : (int, [> `After]) t
  val c : (string, [> `Before]) t
end = struct
  type (_, +_) t =
    | A : (bool, _) t
    | B : (int, _) t
    | C : (string, _) t
  let a = A
  let b = B
  let c = C
end

open T
let f x = (x : (_, [`After]) t :> (_, [>`After]) t)

let f1 : type s . (s, _) 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

This way you get GADT refinement for the first parameter, and subtyping for the second one.

Jacques Garrigue

Re: [Caml-list] GADTs + Phantom types

[oleg]

First of all, I'd like to re-iterate that there are no phantom types
in the declaration below:

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


By definition, a type (variable) is phantom if it appears on the
left-hand side of the declaration but not on the right-hand side. For
example, in

        type 'a foo = I of int | B of bool
'a is phantom because it does not appear on the right-hand side.

Your original GADT (_,_) t can be [not quite, see below]
rewritten as a regular ADT of the form

type ('a,'b) t =
   | A of ('a,bool) eq   * ('b,[< `Before | `After ]) eq
   | B of ('a,int) eq    * ('b,[> `After ]) eq
   | C of ('a,string) eq * ('b,[> `Before]) eq

All type parameters on the left-hand side appear on the right-hand
side. There are no phantom types therefore.

I have used
type (_,_) eq = Refl : ('a,'a) eq
;;

which is the equality GADT. In fact, any GADT can be re-written as a regular
ADT and the eq GADT. One may say that the eq GADT is the only necessary
GADT; all others are syntactic sugar. Well, the sugar is very useful
because it greatly helps in the exhaustiveness check, eliminating false
negatives. 

If you actually try passing the rewritten definition of t to OCaml,
you see a type error about some extra parameter c. That was the row
variable that was lurking in the type [> `After ]. That's the source
of many troubles; that's why Jacques used the 'private' type.

Here is one solution that works for a shallow lattice, like the
lattice of simple permissions: No permission, only Read, only Write,
or anything goes. That is, Bottom, Top, and one layer in between.

Or in our example, only Before, only After, or either way.

type after
type before
;;

type (_, _) t = A : (bool, 'a) t
              | B : (int, after) t
              | C : (string, before) t
;;

(* Function f1 doesn't care about before or after, that's why
it is polymorphic in the second type parameter of attr. Polymorphism
means TOP *)

let f1 : type s any . (s, any) 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
;;

(* Function f2 cares: only before. Therefore, attr cannot have the
case B *)

let f2 : type s . (s, before) t -> s -> unit = fun attr value ->
  f1 attr value
;;

f2 A;; (* - : bool -> unit = <fun> *)
f2 B;; (* type error, as expected *)
f2 C;; (* - : string -> unit = <fun> *)


That code type checks.

What about the general case? Let's consider permissions again:
        None, only Read, only Write, only Delete, ReadWrite (but not
delete), and Everything.

We should recall from Math the correspondence between lattices and
partial orders and the power-set partial order.  Given three elements
read, write, delete, we can build 8 subsets, which can be ordered by
inclusion. Here is the implementation of the idea.

type read
type write
type delete
;;

type (_, _) p = A   : (bool,   (_ * _ * _)) p
              | R   : (int,    (read * _ * _)) p
              | W   : (string, (_ * write * _)) p
              | D   : (string, (_ * _ * delete)) p
              | RW  : (string, (read * write * _)) p
              | RWD : (bool,   (read * write * delete)) p
;;

let f1 : type s .  (s, unit * write * 'a) p -> unit = function
        | A -> ()
        (* | R -> () cannot be read *)
        | W -> ()
        | D -> ()
;;

f1 R;; (* type error *)
f1 D;; (* () *)