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

[Alain Frisch <alain@frisch.fr>]

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.

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.


Alain