Re: [Caml-list] GADTs + Phantom types

[Gabriel Scherer <gabriel.scherer@gmail.com>]

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