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

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

Dear Camlers,

First, let me reiterate my request for feedback:

What I want to know is whether anybody is using GADTs in a way that
would be broken if we disallow type variables under abstract types
(other  than the predefined ones) in the return type of GADTs.
I.e., for instance defining a type witness type involving such abstract types.

This is really the question I want you all to answer.

If this is not the case, we can safely prohibit that at this point, and take
our time to think about the solution.

But if there are some users, we had better provide at least some mechanism,
and injectivity annotations seem to be the less intrusive (they don't
break any code, at least any existing code).
We may need to make clear that they are experimental and might
disappear, but at least we are not in a complete void.

Now just my 2 centimes on alternative approaches

On 2013/04/29, at 16:58, Alain Frisch <alain@frisch.fr> wrote:

> On 04/29/2013 07:17 AM, Jacques Le Normand wrote:
>> Fully injective types are the norm. It would have been nice to have a
>> "non injectivity" or "phantom type" annotation. Since phantom types are
>> seldom used, beginners won't get confused. It might even help beginners
>> understand the concept of a phantom type.
> 
> I'd also prefer an annotation on "non injective" type parameters, rather than on "injective" one.  The problem with this approach is that it requires existing well-typed code to be rewritten, to add these annotations (while annotating injectivity will only impact code using GADTs).  I still believe this is less intrusive than requiring most parametrized abstract type to be annotated, or else making GADTs less useful.

This may be a good idea for 5.00, but honestly this is a big change.

Moreover it is not so clear that this is the right choice for functors:
when a functor takes an abstract type as argument, it usually doesn't care
whether it is injective or not. And in practice there is a technique of adding
a type parameter to abstract types just in case we want to pass a parameterized
type, but usually using this functor for non-parameterized types.

Another point is that I'm not sure how much "less useful" GADTs become when one
forgets an injectivity annotation somewhere.

> For the transition, we could have two compilation modes (decided on the command-line) for this feature.  In "non-injective" (legacy) mode, every parametrized abstract type would be assumed to be non-injective.  This would allow to compile existing code bases (at least those not relying on GADTs).  In "injective-by-default" mode, non-injective parameters would need to be marked as such.  Enabling this mode will require a few annotations to be added to existing code, but this will be very easy, so I guess we don't need to support "injectivity" annotations the "non-injective" mode.

Again, the defect of such a mode is that it is going to apply to everything, including functors.
A functor compiled in this mode might be not be applicable to some modules, whereas there was
no reason from the beginning to require injectivity there.

And just using variance to change the behavior is not going to work well:
a standard practice is to explicitly define module types for the input and output of
the functor. We want the output types to be injective, but we don't really need such
requirement for the input types. But they are just module type definitions…
(See hashtbl.mli for instance for this pattern.)

Jacques