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

[Alain Frisch <alain@frisch.fr>]

On 07/02/2013 01:20 AM, Jacques Garrigue wrote:
> 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.

Btw, this is also an example where type-based disambiguation in presence 
of a GADT would be useful.  For instance, we currently need to write:

     match StringMap_matcher.check t with
     | Some (StringMap_matcher.Is (s, TypEq.Eq)) -> vmap (StringMap.map 
(of_value ~t:s env) x)
     | None -> ...

while one could write:

     match StringMap_matcher.check t with
     | Some (Is (s, Eq)) -> vmap (StringMap.map (of_value ~t:s env) x)
     | None -> ...

(see http://caml.inria.fr/mantis/view.php?id=6023 )

> 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.

Indeed!

In some cases (in particular to add annotations to make sense of error 
messages), it would be useful to be able to name the type constructor 
introduced by opening the GADT to match the existential type.  (I'd put 
this rather high on my wish list around GADTs!)


Alain