RE: [Caml-list] GADTs + Phantom types

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

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