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

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

On 2013/04/30, at 1:37, Nathan Mishra Linger <nathan.mishralinger@gmail.com> wrote:

> Our codebase at Jane Street would not suffer from the proposed fix.
> 
> In fact, we have previously wished the type system tracked injectivity of type
> constructors.  Because it didn't, we wrote Type_equal.Injective [^1] for cases
> when we need to track injectivity ourselves.
> 
> [^1] https://ocaml.janestreet.com/ocaml-core/latest/doc/core/Type_equal.Injective.html

Thank you for the pointer.

One could say this actually shows the need for injectivity annotations
(eventhough Core currently works around them).

To be more precise, injectivity has several uses:

1) To allow you to infer equations between types.
   For instance, assuming the standard equality witness type:

	type (_,_) equal = Eq : ('a,'a) equal

   the following function typeckecks

        let conv1 : type a b. (a array, b array) equal -> a -> b = fun Eq x -> x

   because array is known to be injective, but  this one doesn't

	let conv2 : type a b. (a Queue.t, b Queue.t) equal -> a -> b = fun Eq x -> x

   because Queue.t is an abstract type whose injectivity is unknown.

   This part was correctly handled since 4.00.0.

2) To allow you to prove exhaustiveness of pattern matching, by ensuring
   that other cases cannot happen. For instance,

	type (_,_) comp =
	  | Ceq : ('a,'a) comp
	  | Cany : ('a,'b) comp

	let f (x : (int array,bool array) comp) = match x with Cany -> ()
       
   causes no warning, because the type system can prove that Ceq since
   int array and bool array cannot be equal in any scope. However

	let f (x : (int Queue.t, bool Queue.t) comp) = match x with Cany -> 0

   should emit a warning, because we cannot prove that int Queue.t and
   bool Queue.t are distinct in the absence of injectivity information.
   Note that this is not correctly handled in 4.00, and you will get no warning
   in this situation. Worse, since the code is optimized accordingly (i.e. no
   runtime check is introduced), if the type is really not injective, and you
   pass Eq, you can use this as a hole in the type system.
   This now works correctly in trunk (PR#5981).

3) The problem I describe in my first mail. I.e. when defining a type,
   if you use type variables appearing in constrained type parameters,
   you need the type constructors leading to the type variables to be
   injective. This is PR#5985, and it is only fixed in branches/non-vanishing.

The goal of the Type_equal.Injective interface in Core  is to work around the
limitation on abstract types in (1), by letting you prove injectivity by hand.
But if we had injectivity annotations, this would solve simultaneously all 3
problems: no need to build proofs by hand anymore.

So I understand you answer as: Jane Street is not directly concerned by
(3) at this point, and has already developed a workaround for (1).
I suppose you could profit from injectivity annotations, since you had
to develop a workaround, but this may not be that urgent.

(2) is not so much a problem, since it only means that you may have to
add extra cases to pattern-matching.

Jacques Garrigue