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

[Markus Mottl <markus.mottl@gmail.com>]

On Sat, Apr 27, 2013 at 8:02 PM, Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
> The fix is simple enough: we should track injectivity, and assume that abstract
> types are not injective by default.
> However, this also means that the first type I defined above (using Hashtbl.t)
> will be refused.

If I understand your proposal correctly, the first type would only be
refused unless the standard Hashtbl module were updated with
appropriate injectivity annotations.  The type variables in the GADT
would not need any annotations, because it is assumed that they have
to be injective there anyway for soundness.

> How many of you are using GADTs in this way, and how dependent are you on
> abstract types ?

This seems like a "one percenter" problem.  OTOH, I guess most people
also rarely run into problems where variance annotations matter, but
if they do, they have no option.  The question should therefore rather
be: what's the alternative?  Are there workarounds?  If not,
annotations may just be a necessity to support advanced use cases.

> If we need to be able to define GADTs relying on the injectivity of some abstract
> types, a straightforward solution is to add injectivity annotations on type parameters,
> the same way it was done for variance:
>
>   type #'a t
>
> would mean that t is injective.

Seems concise, but I'm just a little worried that we may be raising
the bar for beginners again.  The standard library would have to be
updated with another annotation that may seem as obscure to beginners
as variance annotations.  I hope we'll never have to explain to a
beginner the meaning of $%^&#-'a.  Maybe a more verbose type
constraint language would have been the better design choice here, but
I guess we've already left this path with variance annotations.

> If you are curious about other difficulties of GADTs, the is also branches/abstract-new
> which introduces a notion of new types, either concrete or abstract, which are guaranteed
> to be distinct from each other, and any other concrete type. This is useful when
> checking the exhaustiveness of pattern-matching, as we can then discard impossible
> branches. That branch is completely experimental.

I haven't looked at this feature yet, but would this require even more
annotations in the standard library?  If so, maybe it would indeed be
time to think about a more accessible syntax for type constraints.

Regards,
Markus

--
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com