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

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

On 2013/04/28, at 11:45, Markus Mottl <markus.mottl@gmail.com> wrote:

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

Yes, only abstract types need to be annotated.
Injectivity only makes sense for type aliases and abstract types (and private row types,
which hide an abstract type), since concrete types are always injective. For instance,
   type 'a t = T of int
is injective (you cannot unify  int t with bool t).

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

At this point I think very few people are concerned.
So it might be the case that we could delay injectivity annotations until 4.02.
However, there is no easy workaround for abstract types.
The simplest one I can think of is duplicating types:

   type ('a,'b) t_impl
   type ('a, 'b) = Hashtbl of ('a,'b) t_impl

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

As Jacques Le Normand pointed, injectivity is a property of parameters,
not of the whole type. (But in most cases a type is injective in all its parameters).

The addition of hard to read information is indeed the main drawback.
The fortunate part here is that, as long as you don't use GADTs, you need not
understand the meaning.

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

This is not really a replacement, since the requirements to be "new" are rather
restrictive. However, as a new type is automatically injective in all its parameters,
you would never need to make its injectivity explicit.
But we need indeed to think about the syntax.
All the more as other features, like the addition of runtime type information,
may also require annotations on types.

	Jacques