Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs

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

On 2013/07/01, at 23:47, Alain Frisch <alain@frisch.fr> wrote:

> A GADT was recently introduced to replace this with a more direct representation:
> 
> module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) :
>    sig
>      type _ is_t = Is: 'a ttype -> 'a T.t is_t
>      val check: 'a ttype -> 'a is_t option
>    end
> 
> The problem is that this doesn't work any more (because T.t is not injective).
> 
> For now, I think I'll use:
> 
> module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) :
>    sig
>      type _ is_t = Is: 'b ttype * ('a, 'b T.t) TypEq.t -> 'a is_t
>      val check : 'a ttype -> 'a is_t option
>    end
> 
> which is accepted and roughly equivalent (by opening the equality witness, one can retrieve the static equality 'a == 'b T.t).

Nice natural example, and nice workaround.

Of course, this is not strictly equivalent.
For instance suppose the following function:
  let f (type a) (tt : a T.t ttype) =
     match check tt with None -> assert false
     | Some (Is (tta, Eq)) -> (tta : a ttype)
The pattern matching will succeed, but tta will only have type "a ttype"
if T.t is injective. The nice part is that this is delayed to the use site,
where we may have more information about T.t, so this trick may still
be useful after introducing injectivity annotations.

Anyway, I suppose that this will work fine for you: check is intended
to be called on unknown types, so the missing equality should not
be a problem.

Jacques