Re: [Caml-list] GADTs + Phantom types

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

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