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

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

> 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!)

Indeed, virtually anyone that used GADTs in OCaml encountered that
problem and has a way to name existential type high on his/her
wishlist. We discussed a few ideas in the following bugtracking
dicussion:

  http://caml.inria.fr/mantis/view.php?id=5780

On Wed, Jul 3, 2013 at 6:08 PM, Alain Frisch <alain@frisch.fr> wrote:
> 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
>
>
> --
> 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