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

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

[Jacques Garrigue]

Some of you may already be aware of PR#5985
http://caml.inria.fr/mantis/view.php?id=5985

To explain very shortly what is happening, a bug was found in the ocaml
compiler, both 4.00 and the development version, such that one that
convert a value from any type to any other type, bypassing all checks.
This is what we call a soundness bug, a hole in the type system.

Such problems happen at times, and we are usually very fast to fix them.
However this time the problem is bit more subtle, because fixing it
straightforwardly may make impossible to write a whole category of
GADTs. Hence this request for feedback.

Practical description of the problem:

It is quite usual to write type witnesses using a GADT:

type _ ty =
  | Int : int ty
  | Pair : 'a ty * 'b ty -> ('a * 'b) ty
  | Hashtbl : 'a ty * 'b ty -> ('a, 'b) Hashtbl.t ty

This looks fine, but now suppose that we write the following code:

module F (X : sig type 'a t end) = struct
   type _ ty =
    | Int : int ty
    | Pair : 'a ty * 'b ty -> ('a * 'b) ty
    | T : 'a ty -> 'a X.t ty
end

The idea is to create a type witness with the
type constructor X.t instead of Hashtbl.t.
Now I can use it this way:

module U = struct type 'a t = unit end
module M = F(U)
let w = M.T M.Int
(* val w : int U.t M.ty *)
let w' = match w with M.T x -> x | _ -> assert false
(* val w' : '_a M.ty = M.Int *)

What this means is that we can now give an arbitrary type
to a witness for int. You can easily use it to build a function
from int to any  type:

let f : type a. a M.ty -> int -> a =
  fun w x -> match w with M.Int -> x | _ -> assert false;;
let g : int -> float = f w';;

If we look at the source of the problem, it lies in the fact U.t is not injective.
I.e. when we define a GADT, we assume that all the type variables in
the return type can be determined from the type parameter.
That is, from (int U.t M.ty) we assume that the type of the argument of T is (int M.ty).
However, since U.t is not injective, int U.t is actually equal to any type 'a U.t,
and we can convert.
Note that, for known types, injectivity was already checked.
I.e., the following definition is not accepted:

type _ ty =
  | Int : int ty
  | Pair : 'a ty * 'b ty -> ('a * 'b) ty
  | T : 'a ty -> 'a U.t ty

However, abstract types were assumed to be injective.
Here we see that you cannot take this for granted.

The problem is of course not limited to type witnesses, and not even GADTs:
types with constrained parameters (introduced at the very beginning of ocaml),
can also trigger it.
And you don't need a functor to trigger it: once you know that two types are equal
in some scope, there are many ways to leak that information.

=============================
Here comes the request for feedback:

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.

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


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.
This is implemented in branches/non-vanishing, in the subversion repository.
	svn checkout http://caml.inria.fr/svn/branches/non-vanishing
Note that in that branch Hashtbl.t in the standard library is marked as injective.
This introduces some new syntax, and libraries have to be modified to benefit,
so the question is do we really need it?


Jacques Garrigue

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

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

[Markus Mottl]

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

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

[Jacques Garrigue]

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

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

[Jacques Le Normand]

[-- Attachment #1: Type: text/plain, Size: 4709 bytes --]

do we need the injectivity annotation at the parameter level or at the type
declaration level?


On Sat, Apr 27, 2013 at 5:02 PM, Jacques Garrigue <
garrigue@math.nagoya-u.ac.jp> wrote:

> Some of you may already be aware of PR#5985
> http://caml.inria.fr/mantis/view.php?id=5985
>
> To explain very shortly what is happening, a bug was found in the ocaml
> compiler, both 4.00 and the development version, such that one that
> convert a value from any type to any other type, bypassing all checks.
> This is what we call a soundness bug, a hole in the type system.
>
> Such problems happen at times, and we are usually very fast to fix them.
> However this time the problem is bit more subtle, because fixing it
> straightforwardly may make impossible to write a whole category of
> GADTs. Hence this request for feedback.
>
> Practical description of the problem:
>
> It is quite usual to write type witnesses using a GADT:
>
> type _ ty =
>   | Int : int ty
>   | Pair : 'a ty * 'b ty -> ('a * 'b) ty
>   | Hashtbl : 'a ty * 'b ty -> ('a, 'b) Hashtbl.t ty
>
> This looks fine, but now suppose that we write the following code:
>
> module F (X : sig type 'a t end) = struct
>    type _ ty =
>     | Int : int ty
>     | Pair : 'a ty * 'b ty -> ('a * 'b) ty
>     | T : 'a ty -> 'a X.t ty
> end
>
> The idea is to create a type witness with the
> type constructor X.t instead of Hashtbl.t.
> Now I can use it this way:
>
> module U = struct type 'a t = unit end
> module M = F(U)
> let w = M.T M.Int
> (* val w : int U.t M.ty *)
> let w' = match w with M.T x -> x | _ -> assert false
> (* val w' : '_a M.ty = M.Int *)
>
> What this means is that we can now give an arbitrary type
> to a witness for int. You can easily use it to build a function
> from int to any  type:
>
> let f : type a. a M.ty -> int -> a =
>   fun w x -> match w with M.Int -> x | _ -> assert false;;
> let g : int -> float = f w';;
>
> If we look at the source of the problem, it lies in the fact U.t is not
> injective.
> I.e. when we define a GADT, we assume that all the type variables in
> the return type can be determined from the type parameter.
> That is, from (int U.t M.ty) we assume that the type of the argument of T
> is (int M.ty).
> However, since U.t is not injective, int U.t is actually equal to any type
> 'a U.t,
> and we can convert.
> Note that, for known types, injectivity was already checked.
> I.e., the following definition is not accepted:
>
> type _ ty =
>   | Int : int ty
>   | Pair : 'a ty * 'b ty -> ('a * 'b) ty
>   | T : 'a ty -> 'a U.t ty
>
> However, abstract types were assumed to be injective.
> Here we see that you cannot take this for granted.
>
> The problem is of course not limited to type witnesses, and not even GADTs:
> types with constrained parameters (introduced at the very beginning of
> ocaml),
> can also trigger it.
> And you don't need a functor to trigger it: once you know that two types
> are equal
> in some scope, there are many ways to leak that information.
>
> =============================
> Here comes the request for feedback:
>
> 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.
>
> How many of you are using GADTs in this way, and how dependent are you on
> abstract types ?
>
>
> 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.
> This is implemented in branches/non-vanishing, in the subversion
> repository.
>         svn checkout http://caml.inria.fr/svn/branches/non-vanishing
> Note that in that branch Hashtbl.t in the standard library is marked as
> injective.
> This introduces some new syntax, and libraries have to be modified to
> benefit,
> so the question is do we really need it?
>
>
> Jacques Garrigue
>
> P.S.
> 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.
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

[-- Attachment #2: Type: text/html, Size: 5933 bytes --]

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

[Ivan Gotovchits]

Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> writes:
>
> 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
>

I'm not sure that symbol '#' is a good choice. It is already used for
open types and may impose difficulties in undestanding code (and
compiler messages) when overriden. For me '#' is something polymorphic
and related to OOP. 

And indeed, «#'a» is to perlish... Personally, I would prefer something
like:

  type 'a t
  constraint 'a is injective


P.S. the following symbols looks more «injective» for me: '>', '^', '=',
though the last one can be confused with the invariance.



-- 
         (__) 
         (oo) 
   /------\/ 
  / |    ||   
 *  /\---/\ 
    ~~   ~~   
...."Have you mooed today?"...

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

[Ivan Gotovchits]

Ivan Gotovchits <ivg@ieee.org> writes:


> I'm not sure that symbol '#' is a good choice. It is already used for
> open types and may impose difficulties in undestanding code (and
> compiler messages) when overriden. For me '#' is something polymorphic
> and related to OOP. 
>
> And indeed, «#'a» is to perlish... Personally, I would prefer something
> like:
>
>   type 'a t
>   constraint 'a is injective
>
>
> P.S. the following symbols looks more «injective» for me: '>', '^', '=',
> though the last one can be confused with the invariance.

P.P.S. Here is one more: '~' as it stands for equivalence.

-- 
         (__) 
         (oo) 
   /------\/ 
  / |    ||   
 *  /\---/\ 
    ~~   ~~   
...."Have you mooed today?"...

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

[Jacques Le Normand]

[-- Attachment #1: Type: text/plain, Size: 4871 bytes --]

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.



On Sat, Apr 27, 2013 at 5:02 PM, Jacques Garrigue <
garrigue@math.nagoya-u.ac.jp> wrote:

> Some of you may already be aware of PR#5985
> http://caml.inria.fr/mantis/view.php?id=5985
>
> To explain very shortly what is happening, a bug was found in the ocaml
> compiler, both 4.00 and the development version, such that one that
> convert a value from any type to any other type, bypassing all checks.
> This is what we call a soundness bug, a hole in the type system.
>
> Such problems happen at times, and we are usually very fast to fix them.
> However this time the problem is bit more subtle, because fixing it
> straightforwardly may make impossible to write a whole category of
> GADTs. Hence this request for feedback.
>
> Practical description of the problem:
>
> It is quite usual to write type witnesses using a GADT:
>
> type _ ty =
>   | Int : int ty
>   | Pair : 'a ty * 'b ty -> ('a * 'b) ty
>   | Hashtbl : 'a ty * 'b ty -> ('a, 'b) Hashtbl.t ty
>
> This looks fine, but now suppose that we write the following code:
>
> module F (X : sig type 'a t end) = struct
>    type _ ty =
>     | Int : int ty
>     | Pair : 'a ty * 'b ty -> ('a * 'b) ty
>     | T : 'a ty -> 'a X.t ty
> end
>
> The idea is to create a type witness with the
> type constructor X.t instead of Hashtbl.t.
> Now I can use it this way:
>
> module U = struct type 'a t = unit end
> module M = F(U)
> let w = M.T M.Int
> (* val w : int U.t M.ty *)
> let w' = match w with M.T x -> x | _ -> assert false
> (* val w' : '_a M.ty = M.Int *)
>
> What this means is that we can now give an arbitrary type
> to a witness for int. You can easily use it to build a function
> from int to any  type:
>
> let f : type a. a M.ty -> int -> a =
>   fun w x -> match w with M.Int -> x | _ -> assert false;;
> let g : int -> float = f w';;
>
> If we look at the source of the problem, it lies in the fact U.t is not
> injective.
> I.e. when we define a GADT, we assume that all the type variables in
> the return type can be determined from the type parameter.
> That is, from (int U.t M.ty) we assume that the type of the argument of T
> is (int M.ty).
> However, since U.t is not injective, int U.t is actually equal to any type
> 'a U.t,
> and we can convert.
> Note that, for known types, injectivity was already checked.
> I.e., the following definition is not accepted:
>
> type _ ty =
>   | Int : int ty
>   | Pair : 'a ty * 'b ty -> ('a * 'b) ty
>   | T : 'a ty -> 'a U.t ty
>
> However, abstract types were assumed to be injective.
> Here we see that you cannot take this for granted.
>
> The problem is of course not limited to type witnesses, and not even GADTs:
> types with constrained parameters (introduced at the very beginning of
> ocaml),
> can also trigger it.
> And you don't need a functor to trigger it: once you know that two types
> are equal
> in some scope, there are many ways to leak that information.
>
> =============================
> Here comes the request for feedback:
>
> 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.
>
> How many of you are using GADTs in this way, and how dependent are you on
> abstract types ?
>
>
> 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.
> This is implemented in branches/non-vanishing, in the subversion
> repository.
>         svn checkout http://caml.inria.fr/svn/branches/non-vanishing
> Note that in that branch Hashtbl.t in the standard library is marked as
> injective.
> This introduces some new syntax, and libraries have to be modified to
> benefit,
> so the question is do we really need it?
>
>
> Jacques Garrigue
>
> P.S.
> 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.
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

[-- Attachment #2: Type: text/html, Size: 6145 bytes --]

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

[Alain Frisch]

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

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

[Jacques Garrigue]

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

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

[Alain Frisch]

On 04/29/2013 12:52 PM, Jacques Garrigue wrote:
> 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.

The only abstract types in the return type of GADTs in LexiFi's code 
base code are currently either non-parametrized ones or built-in types 
(array, lazy).  So we'd be fine with the proposed fix (assuming that 
abstract types are not injective).

-- Alain

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

[Nathan Mishra Linger]

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

On Mon, Apr 29, 2013 at 7:23 AM, Alain Frisch <alain@frisch.fr> wrote:
> On 04/29/2013 12:52 PM, Jacques Garrigue wrote:
>>
>> 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.
>
>
> The only abstract types in the return type of GADTs in LexiFi's code base
> code are currently either non-parametrized ones or built-in types (array,
> lazy).  So we'd be fine with the proposed fix (assuming that abstract types
> are not injective).
>
> -- Alain
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

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

[Jacques Garrigue]

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

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

[Jacques Garrigue]

I have now committed in trunk a fix to PR#5985.
You can use it to test whether your codebase runs into problems.
You can either obtain it from subversion directly
	svn checkout http://caml.inria.fr/svn/ocaml/trunk
or use opam to do it for you.

I checked that at least Core itself compiles without problems.

Again, if you run into problems, you can try branches/non-vanishing,
which allows you to annotate some abstract types are injective.

Jacques Garrigue

On 2013/04/29, at 19:52, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote:

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

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

[Jacques Garrigue]

On 2013/04/30, at 14:45, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote:

> I have now committed in trunk a fix to PR#5985.
> You can use it to test whether your codebase runs into problems.
> You can either obtain it from subversion directly
> 	svn checkout http://caml.inria.fr/svn/ocaml/trunk
> or use opam to do it for you.
> 
> I checked that at least Core itself compiles without problems.

Ironically, I have just found that lablgtk2 does not compile with the fixed version.
lablgtk2 does not use GADTs, but it uses constrained type parameters in classes.

The problem is as follows:

gobject.mli:
type -'a gobj

gContainer.mli:
class virtual ['a] item_container :
  object
    constraint 'a = < as_item : [>`widget] obj; .. >
    method add : 'a -> unit
    …
  end

File "gContainer.mli", line 126, characters 6-665:
Error: In this definition, a type variable cannot be deduced
       from the type parameters.

It is a bit surprising, since the said variable is the row variable
of the above [> `widget], and it is only referred through 'a.
The reason there is an error is that the checkability requirements
for the body of types and constrained type parameters differ:
to allow the row variable to appear in a position potentially
contravariant, we need it to know from the constraint that it
appears for sure in a negative or invariant position.
One way to solve this is to check that the type identified by 'a can
actually be handled as a real variable (its internal variables do
not occur out of it), which would solve the discrepancy.
However, checking this is going to be a pain.
And making gobj injective immediately solves the problem.

In the midtime, the problem is fixed in the git version of
lablgtk2 by pretending that gobj is a private sum type (whose
contents are abstract).

This also empasizes that the new restriction does not impact
only GADTs: all constrained type parameters are also concerned.

	Jacques Garrigue

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

[Gabriel Scherer]

> One way to solve this is to check that the type identified by 'a can
> actually be handled as a real variable (its internal variables do
> not occur out of it), which would solve the discrepancy.

If I understand correctly, you are saying that this "constraint", in
absence of injectivity, could be handled semantically like GADTs with
non-injective equations, that is as quantifying locally on a ("true")
existential variable?

Handling existential variables (in fact local type constructors)
attached to GADT constructors is well-understood as they have clear
introduction sites and scopes, exactly where their constructor is
matched. When you say that checking the "constraint" case is painful,
is it related to the fact that there is no such corresponding
term-level marker?

On Sat, May 4, 2013 at 8:46 AM, Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
> On 2013/04/30, at 14:45, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote:
>
>> I have now committed in trunk a fix to PR#5985.
>> You can use it to test whether your codebase runs into problems.
>> You can either obtain it from subversion directly
>>       svn checkout http://caml.inria.fr/svn/ocaml/trunk
>> or use opam to do it for you.
>>
>> I checked that at least Core itself compiles without problems.
>
> Ironically, I have just found that lablgtk2 does not compile with the fixed version.
> lablgtk2 does not use GADTs, but it uses constrained type parameters in classes.
>
> The problem is as follows:
>
> gobject.mli:
> type -'a gobj
>
> gContainer.mli:
> class virtual ['a] item_container :
>   object
>     constraint 'a = < as_item : [>`widget] obj; .. >
>     method add : 'a -> unit
>     …
>   end
>
> File "gContainer.mli", line 126, characters 6-665:
> Error: In this definition, a type variable cannot be deduced
>        from the type parameters.
>
> It is a bit surprising, since the said variable is the row variable
> of the above [> `widget], and it is only referred through 'a.
> The reason there is an error is that the checkability requirements
> for the body of types and constrained type parameters differ:
> to allow the row variable to appear in a position potentially
> contravariant, we need it to know from the constraint that it
> appears for sure in a negative or invariant position.
> One way to solve this is to check that the type identified by 'a can
> actually be handled as a real variable (its internal variables do
> not occur out of it), which would solve the discrepancy.
> However, checking this is going to be a pain.
> And making gobj injective immediately solves the problem.
>
> In the midtime, the problem is fixed in the git version of
> lablgtk2 by pretending that gobj is a private sum type (whose
> contents are abstract).
>
> This also empasizes that the new restriction does not impact
> only GADTs: all constrained type parameters are also concerned.
>
>         Jacques Garrigue
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

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

[Jacques Garrigue]

On 2013/05/04, at 16:09, Gabriel Scherer <gabriel.scherer@gmail.com> wrote:

>> One way to solve this is to check that the type identified by 'a can
>> actually be handled as a real variable (its internal variables do
>> not occur out of it), which would solve the discrepancy.
> 
> If I understand correctly, you are saying that this "constraint", in
> absence of injectivity, could be handled semantically like GADTs with
> non-injective equations, that is as quantifying locally on a ("true")
> existential variable?

I did not think of it that way, but this is something like that.
By abstracting on the (common) part of the types which contains
abstract type constructor, we can fall back to exact variance information.

> Handling existential variables (in fact local type constructors)
> attached to GADT constructors is well-understood as they have clear
> introduction sites and scopes, exactly where their constructor is
> matched. When you say that checking the "constraint" case is painful,
> is it related to the fact that there is no such corresponding
> term-level marker?

Well yes, you have to find the common parts yourself.
Actually this is not that bad.
I have committed a fix, which works by recursing on the body
of the definition, trying to find equal types inside the constrained
parameters. If the variance at this point is correct, one doesn't
need to look inside.
This may be a bit expensive, but usually constraints are not big.

In theory one could do even better, by abstracting on the "real"
variance of abstract types. Then the variance of an occurence
becomes a set of paths (composition of variances) from the root
of the type definition. However, this just looks too complicated to
me...

> On Sat, May 4, 2013 at 8:46 AM, Jacques Garrigue
> <garrigue@math.nagoya-u.ac.jp> wrote:
>> Ironically, I have just found that lablgtk2 does not compile with the fixed version.
>> lablgtk2 does not use GADTs, but it uses constrained type parameters in classes.
>> 
>> The problem is as follows:
>> 
>> gobject.mli:
>> type -'a gobj
>> 
>> gContainer.mli:
>> class virtual ['a] item_container :
>>  object
>>    constraint 'a = < as_item : [>`widget] obj; .. >
>>    method add : 'a -> unit
>>    …
>>  end
>> 
>> File "gContainer.mli", line 126, characters 6-665:
>> Error: In this definition, a type variable cannot be deduced
>>       from the type parameters.

This problem is now fixed, without needing to change lablgtk2 sources.

On 2013/04/30, at 22:06, Leo White <lpw25@cam.ac.uk> wrote:

>>>>      type 'a t = T;;
>>>>      type _ g = G : 'a -> 'a t g;;
>>> 
>>> I don't see why this could not be allowed without the restriction you
>>> propose. I thought that this was rejected in 4.00 because 4.00 used
>>> bi-variance as an (unsafe) approximation of non-injective. Since we now
>>> track injectivity separately from variance g be accepted (with 'a covariant).
>> 
>> In our work, this GADT definition would be accepted, and:
>> (1) matching on the constructor G does not give any information on the
>> value of the existential type 'a
>> (2) the parameter of g (not 'a, the one marked _ above) may marked
>> covariant or invariant, because the constructor t is upward-closed but
>> not downward-closed (private types)
> 
> I don't think the argument to G needs to be given an existential type,
> as long as the parameter of g is marked invariant.
> 
> The parameter to g should be marked invariant for two reasons:
> 1) It is constrained in the result type of a GADT constructor which, as
> discussed on this list previously, forces it to be invariant (at least
> for now, see Gabriel's paper for further details).
> 2) Marking it as anything other than invariant, would entail marking
> 'a as bi-variant, when it is in fact covariant.
> 
> This second reason also occurs in types with constraints, for example:
> 
>  type 'a s = 'b constraint 'a = 'b t
> 
> here 'b is covariant (used in covariant and bi-variant positions), but
> marking 'a as any variance other than invariant would entail marking 'b
> as bi-variant.

Sorry for the slow answer. The implementation was not correct yet...

I think there is a misunderstanding here.
The problem is that 'b has two variances: its internal one, inferred from
its occurrences inside the body of the type, and its external one, defined
by its occurences inside parameters of the type.
For the definition to be correct, we need the external variance to be
at least as rigid as the internal one.
The extra difficulty is that our knowledge of variances is only approximative
(due to abstraction), and we have to use lower bounds on external variances,
and an upper bounds on internal variances (to be sure that we are safe).
Here the lower bound says just that the external variance of 'b
is the composition of invariant and injective, while the internal one
is covariant. If invariant o injective were defined as only injective,
it would be less rigid than the internal version, hence the need to
have invariant o injective = invariant.
(But for the converse, we only have injective o invariant = injective)

Actually I realized that just positive, negative and injective are not sufficient.
To fully accommodate the need for upper and lower bounds, we end up
needing 7 different variance flags!
  may_pos, may_neg : the variable may appear at positive or negative
	occurrences in the real definition; this is an upper bound,
	corresponding to variance annotations on abstract types
  may_weak: needed to make type inference principal
  pos, neg: we now that the variable appears at positive or negative
	occurrences in the real definition; this is a lower bound
  inj: either pos, or neg, or parameter of a concrete definition;
	does not disappear by expansion
  inv: pos and neg simultaneously in a concrete definition; needed
	the above composition inv o inj = inv
We have the hierarchy unknown < inj < pos \/ neg < pos /\ neg < inv.
Of course not all combinations are valid, (for instance pos implies may_pos,
etc…) but this is still mind boggling.

But those are not sufficient to solve the lablgtk2 problem above:
calling 'b the row variable of [> `widget], its internal variance is
neg o pos o may_neg, but its external variance is inv o pos o may_neg.
The result is may_pos internally, but externally the result is
may_pos /\ may_neg, whose lower bound is just "unknown".

Hence the need to "abstract" on common types, when their internal
variables do not escape.
The variance of 'a internally is neg, and externally inv, so all is fine.

This is a bit complicated, but the full specification is clear enough.
Thanks to the detection of common types, the fact that the only flags
for abstract types are may_pos and may_neg is not too much
a problem for constrained parameters.

Jacques Garrigue

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

[Alain Frisch]

On 04/29/2013 12:52 PM, Jacques Garrigue wrote:
> 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.)

These are interesting arguments against the "injective by default" mode 
(explicit non-injectivity annotations).  I did not think about the 
consequences on functors indeed.  In practice, though, it might be ok to 
annotate, if needed, some module types used as functor arguments with 
non-injectivity annotations (or more precisely "not-necessarily 
injective" annotations).  But this certainly deserves some careful thinking.

It's reassuring to see that the conservative solution (not assuming 
injectivity of user defined abstract types) does not seem too bad for 
now, even if not very satisfying.


I'm only concerned with:

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


Do you think that fixing this unsoundness (without injectivity 
annotations) would lead to reject existing programs?


-- Alain

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

[Jacques Garrigue]

On 2013/04/30, at 15:59, Alain Frisch <alain@frisch.fr> wrote:

> It's reassuring to see that the conservative solution (not assuming injectivity of user defined abstract types) does not seem too bad for now, even if not very satisfying.
> 
> I'm only concerned with:
> 
>> 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.
> 
> Do you think that fixing this unsoundness (without injectivity annotations) would lead to reject existing programs?

Potentially yes.
But I don't know how it is in practice for code existing now.
Hence my question.

I have now committed the fix in trunk, so people can try it.

A reason the impact is going to be limited, is that usually when defining
a GADT for type witnesses, one only lists predefined types, and uses
another mechanism for user defined types, like what is done in Core.
If you use a mechanism based on equality witnesses, (lack of) injectivity
already came in the way before, so this is not a new phenomenon.

For other applications of GADTs, you are defining type indices yourself,
so you just have to be careful to use concrete types instead of abstract types.

Jacques Garrigue

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

[Alain Frisch]

On 04/30/2013 09:56 AM, Jacques Garrigue wrote:
> On 2013/04/30, at 15:59, Alain Frisch <alain@frisch.fr> wrote:
>
>> It's reassuring to see that the conservative solution (not assuming injectivity of user defined abstract types) does not seem too bad for now, even if not very satisfying.
>>
>> I'm only concerned with:
>>
>>> 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.
>>
>> Do you think that fixing this unsoundness (without injectivity annotations) would lead to reject existing programs?
>
> Potentially yes.
> But I don't know how it is in practice for code existing now.
> Hence my question.

Apart from GADTs, does your patch address the unsoundness with type 
constraints?


Alain

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

[Jacques Garrigue]

On 2013/04/30, at 17:02, Alain Frisch <alain@frisch.fr> wrote:

> On 04/30/2013 09:56 AM, Jacques Garrigue wrote:
>> On 2013/04/30, at 15:59, Alain Frisch <alain@frisch.fr> wrote:
>> 
>>> It's reassuring to see that the conservative solution (not assuming injectivity of user defined abstract types) does not seem too bad for now, even if not very satisfying.
>>> 
>>> I'm only concerned with:
>>> 
>>>> 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.
>>> 
>>> Do you think that fixing this unsoundness (without injectivity annotations) would lead to reject existing programs?
>> 
>> Potentially yes.
>> But I don't know how it is in practice for code existing now.
>> Hence my question.
> 
> Apart from GADTs, does your patch address the unsoundness with type constraints?

Sure, this is exactly the same mechanism.

The only other thing it does is a slight strengthening of variance checking.

Consider the type
   type 'a t = T                   (* 'a bi-variant and injective *)
   type 'a u = 'a t -> 'a t    (* 'a t occurs both at positive and negative positions *)

Originally, the parameter of u would have been bi-variant (or unrestricted)
since it is bi-variant in the definition of t.
However it is now invariant.
The reason is that you can only change it by subtyping in t, and u doesn't allow subtyping.
This is a reasonable restriction, and it is necessary to allow some GADT
definitions where we use concrete types as indices.

Jacques Garrigue

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

[Gabriel Scherer]

> The only other thing it does is a slight strengthening of variance checking.
>
> Consider the type
>    type 'a t = T                   (* 'a bi-variant and injective *)
>    type 'a u = 'a t -> 'a t    (* 'a t occurs both at positive and negative positions *)
>
> Originally, the parameter of u would have been bi-variant (or unrestricted)
> since it is bi-variant in the definition of t.
> However it is now invariant.
> The reason is that you can only change it by subtyping in t, and u doesn't allow subtyping.
> This is a reasonable restriction, and it is necessary to allow some GADT
> definitions where we use concrete types as indices.

I'm not sure about this. In our work on variance of GADTs (
http://arxiv.org/abs/1301.2903 ), we defined equality exactly as the
antisymmetric closure of the subtyping relation (as is done in the
previous work by Simonet and Pottier), and all type constructors are
functional: (a = b) implies (a t = b t). This means that in our
formalization, you ('a u = 'a bivar -> 'a bivar) is bivariant, because
('a bivar = 'b bivar) for any 'a and 'b implies (a u = 'a bivar -> 'a
bivar = 'b bivar -> 'b bivar = 'b u).

This vision of invariance as still functional also plays nicely with
the inversion principle: when you have (a t <= b t) when t covariant,
you can deduce (a <= b), when t is contravariant you have (a >= b),
and we can explain invariance as saying that you then have both, (a <=
b) and (b <= a), which coincides with the algorithmic notion of
"occurs both negatively and positively". The nice thing is that this
inversion criterion is also complete, from (a <= b) and (b <= a) you
can deduce (a t <= b t) for t invariant (in our system).

What is the reason for adding your strengthening? What I understood so
far is that unification, and therefore provable equality/inequalities,
were orthogonal to variance (eg. (type 'a t = T) is both bivariant and
injective). Is there a reason to tie them back together precisely in
the invariant case?

On Tue, Apr 30, 2013 at 10:18 AM, Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
> On 2013/04/30, at 17:02, Alain Frisch <alain@frisch.fr> wrote:
>
>> On 04/30/2013 09:56 AM, Jacques Garrigue wrote:
>>> On 2013/04/30, at 15:59, Alain Frisch <alain@frisch.fr> wrote:
>>>
>>>> It's reassuring to see that the conservative solution (not assuming injectivity of user defined abstract types) does not seem too bad for now, even if not very satisfying.
>>>>
>>>> I'm only concerned with:
>>>>
>>>>> 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.
>>>>
>>>> Do you think that fixing this unsoundness (without injectivity annotations) would lead to reject existing programs?
>>>
>>> Potentially yes.
>>> But I don't know how it is in practice for code existing now.
>>> Hence my question.
>>
>> Apart from GADTs, does your patch address the unsoundness with type constraints?
>
> Sure, this is exactly the same mechanism.
>
> The only other thing it does is a slight strengthening of variance checking.
>
> Consider the type
>    type 'a t = T                   (* 'a bi-variant and injective *)
>    type 'a u = 'a t -> 'a t    (* 'a t occurs both at positive and negative positions *)
>
> Originally, the parameter of u would have been bi-variant (or unrestricted)
> since it is bi-variant in the definition of t.
> However it is now invariant.
> The reason is that you can only change it by subtyping in t, and u doesn't allow subtyping.
> This is a reasonable restriction, and it is necessary to allow some GADT
> definitions where we use concrete types as indices.
>
> Jacques Garrigue
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

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

[Jacques Garrigue]

On 2013/04/30, at 18:11, Gabriel Scherer <gabriel.scherer@gmail.com> wrote:

>> The only other thing it does is a slight strengthening of variance checking.
>> 
>> Consider the type
>>   type 'a t = T                   (* 'a bi-variant and injective *)
>>   type 'a u = 'a t -> 'a t    (* 'a t occurs both at positive and negative positions *)
>> 
>> Originally, the parameter of u would have been bi-variant (or unrestricted)
>> since it is bi-variant in the definition of t.
>> However it is now invariant.
>> The reason is that you can only change it by subtyping in t, and u doesn't allow subtyping.
>> This is a reasonable restriction, and it is necessary to allow some GADT
>> definitions where we use concrete types as indices.
> 
> I'm not sure about this. In our work on variance of GADTs (
> http://arxiv.org/abs/1301.2903 ), we defined equality exactly as the
> antisymmetric closure of the subtyping relation (as is done in the
> previous work by Simonet and Pottier), and all type constructors are
> functional: (a = b) implies (a t = b t). This means that in our
> formalization, you ('a u = 'a bivar -> 'a bivar) is bivariant, because
> ('a bivar = 'b bivar) for any 'a and 'b implies (a u = 'a bivar -> 'a
> bivar = 'b bivar -> 'b bivar = 'b u).
> 
> This vision of invariance as still functional also plays nicely with
> the inversion principle: when you have (a t <= b t) when t covariant,
> you can deduce (a <= b), when t is contravariant you have (a >= b),
> and we can explain invariance as saying that you then have both, (a <=
> b) and (b <= a), which coincides with the algorithmic notion of
> "occurs both negatively and positively". The nice thing is that this
> inversion criterion is also complete, from (a <= b) and (b <= a) you
> can deduce (a t <= b t) for t invariant (in our system).

But it seems to me that this contradicts the definition of injectivity.
Namely, if we follow your definition, and have 'a bivar = 'b bivar, then
clearly bivar is not injective.
So there are two solutions: either we do not allow a bi-variant type
to be injective (breaking our simple statement that concrete types
are injective in all their parameters), or we consider bi-variance +
injectivity is some intermediary state, where we can use both directions
of subtyping, but not strong (unification) equality.

> What is the reason for adding your strengthening? What I understood so
> far is that unification, and therefore provable equality/inequalities,
> were orthogonal to variance (eg. (type 'a t = T) is both bivariant and
> injective). Is there a reason to tie them back together precisely in
> the invariant case?


The theoretical reason is above.
The practical reason is to make easier to define indices.
If we keep the bi-variance in an invariant context, then the following
type definition is refused:

	type 'a t = T;;
	type _ g = G : 'a -> 'a t g;;

In 4.00, this definition is refused because 'a in 'a t g is bi-variant, but 'a appears
in a covariant position.

Jacques Garrigue

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

[Leo White]

[Sorry if this is a repeat post]

> But it seems to me that this contradicts the definition of injectivity.
> Namely, if we follow your definition, and have 'a bivar = 'b bivar, then
> clearly bivar is not injective.

I think Gabriel meant that 'a bivar = 'b bivar were equal in the
subtyiping relationship, rather than in the unification
relationship. (Perhaps we should use a different symbol for subtyping
equality).

> So there are two solutions: either we do not allow a bi-variant type
> to be injective (breaking our simple statement that concrete types
> are injective in all their parameters), or we consider bi-variance +
> injectivity is some intermediary state, where we can use both directions
> of subtyping, but not strong (unification) equality.

I don't see how this implies the need for the strengthening you
describe. As I see it:

  type 'a t = T

creates a type that is bi-variant in its parameter, so all occurences of
'a in:

  type 'a u = 'a t -> 'a t

are in bi-variant positions, so u should also be bi-variant.

> The practical reason is to make easier to define indices.
> If we keep the bi-variance in an invariant context, then the following
> type definition is refused:
>
> 	type 'a t = T;;
> 	type _ g = G : 'a -> 'a t g;;
>
> In 4.00, this definition is refused because 'a in 'a t g is bi-variant, but 'a appears
> in a covariant position.

I don't see why this could not be allowed without the restriction you
propose. I thought that this was rejected in 4.00 because 4.00 used
bi-variance as an (unsafe) approximation of non-injective. Since we now
track injectivity separately from variance g be accepted (with 'a covariant).

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

[Gabriel Scherer]

Indeed, the (=) in my message above where in the context of the work
where it is define as ((<=) and (>=)), so in a sense "equality in the
sense of subtyping rather than unification". Sorry for the confusion.
I'll now mark this relation as <=>.

>> The practical reason is to make easier to define indices.
>> If we keep the bi-variance in an invariant context, then the following
>> type definition is refused:
>>
>>       type 'a t = T;;
>>       type _ g = G : 'a -> 'a t g;;
>>
>> In 4.00, this definition is refused because 'a in 'a t g is bi-variant, but 'a appears
>> in a covariant position.
>
> I don't see why this could not be allowed without the restriction you
> propose. I thought that this was rejected in 4.00 because 4.00 used
> bi-variance as an (unsafe) approximation of non-injective. Since we now
> track injectivity separately from variance g be accepted (with 'a covariant).

In our work, this GADT definition would be accepted, and:
(1) matching on the constructor G does not give any information on the
value of the existential type 'a
(2) the parameter of g (not 'a, the one marked _ above) may marked
covariant or invariant, because the constructor t is upward-closed but
not downward-closed (private types)

In particular, the following does not type-check:
  let extract : int t g -> int = function
    | G n -> n

The G constructor at type ('b t) has type (exists 'a ['a t <=> 'b].
'a); so in the G branch the type-checker introduces the hypothesis ('a
t <=> int t) for an existential variable 'a. This does not allows to
deduce ('a <=> int) and therefore the body does not type-check.

However, in the OCaml type system, GADT type equalities are understood
in the unification sense (because it is the one that mixes well with
the inference engine), so the constructor G at type ('b g) would have
type (exists 'a. ['a t = 'b]), with (=) in the unification sense. As
Jacques said, this means that we must either reject the definition of
('b g) as is currently done, or stop considering ('a t) injective.

PS: Note that you could understand type parameter constraints in the
same way, which makes them safe without requiring injectivity, but
Didier remarked that this will only delay failure as code writers
generally assume injectivity. It's before to fail at definition site
than at usage site if you know you should fail anyway.

On Tue, Apr 30, 2013 at 12:12 PM, Leo White <lpw25@cam.ac.uk> wrote:
> [Sorry if this is a repeat post]
>
>> But it seems to me that this contradicts the definition of injectivity.
>> Namely, if we follow your definition, and have 'a bivar = 'b bivar, then
>> clearly bivar is not injective.
>
> I think Gabriel meant that 'a bivar = 'b bivar were equal in the
> subtyiping relationship, rather than in the unification
> relationship. (Perhaps we should use a different symbol for subtyping
> equality).
>
>> So there are two solutions: either we do not allow a bi-variant type
>> to be injective (breaking our simple statement that concrete types
>> are injective in all their parameters), or we consider bi-variance +
>> injectivity is some intermediary state, where we can use both directions
>> of subtyping, but not strong (unification) equality.
>
> I don't see how this implies the need for the strengthening you
> describe. As I see it:
>
>   type 'a t = T
>
> creates a type that is bi-variant in its parameter, so all occurences of
> 'a in:
>
>   type 'a u = 'a t -> 'a t
>
> are in bi-variant positions, so u should also be bi-variant.
>
>> The practical reason is to make easier to define indices.
>> If we keep the bi-variance in an invariant context, then the following
>> type definition is refused:
>>
>>       type 'a t = T;;
>>       type _ g = G : 'a -> 'a t g;;
>>
>> In 4.00, this definition is refused because 'a in 'a t g is bi-variant, but 'a appears
>> in a covariant position.
>
> I don't see why this could not be allowed without the restriction you
> propose. I thought that this was rejected in 4.00 because 4.00 used
> bi-variance as an (unsafe) approximation of non-injective. Since we now
> track injectivity separately from variance g be accepted (with 'a covariant).

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

[Leo White]

>>>       type 'a t = T;;
>>>       type _ g = G : 'a -> 'a t g;;
>>
>> I don't see why this could not be allowed without the restriction you
>> propose. I thought that this was rejected in 4.00 because 4.00 used
>> bi-variance as an (unsafe) approximation of non-injective. Since we now
>> track injectivity separately from variance g be accepted (with 'a covariant).
>
> In our work, this GADT definition would be accepted, and:
> (1) matching on the constructor G does not give any information on the
> value of the existential type 'a
> (2) the parameter of g (not 'a, the one marked _ above) may marked
> covariant or invariant, because the constructor t is upward-closed but
> not downward-closed (private types)

I don't think the argument to G needs to be given an existential type,
as long as the parameter of g is marked invariant.

The parameter to g should be marked invariant for two reasons:
1) It is constrained in the result type of a GADT constructor which, as
discussed on this list previously, forces it to be invariant (at least
for now, see Gabriel's paper for further details).
2) Marking it as anything other than invariant, would entail marking
'a as bi-variant, when it is in fact covariant.

This second reason also occurs in types with constraints, for example:

  type 'a s = 'b constraint 'a = 'b t

here 'b is covariant (used in covariant and bi-variant positions), but
marking 'a as any variance other than invariant would entail marking 'b
as bi-variant.

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

[Gabriel Scherer]

On Mon, Apr 29, 2013 at 7:17 AM, Jacques Le Normand
<rathereasy@gmail.com> 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.

In practice most definitions using what we call a "phantom type" are
in fact injective (because sum and record types are injective in all
parameters if your notion of type equality is unification), so it
would be more dangerous than helpful to link the two concepts.

You are right however to remark that in a sense the "right default" is
to be injective rather than be potentially non-injective. If we were
starting from void, it would make sense to pick (type 'a t) as meaning
that 'a is injective, and a different syntax for maybe-non-injective¹
types (this was suggested by other people in the discussion). However,
this would break backward compatibility as code that is working now,
providing a non-injective type to a signature (type 'a t), would then
fail to type-check.

There are two different design principles in tension here:
- the least path of resistance: the shortest syntax should have the
most common and useful meaning, and it is suboptimal to add a
complication that would apply in almost all cases
- pay (only) for what you use: if you don't use GADTs, you most
probably don't care about injectivity, so it would be wrong to break
existing code to facilitate a feature that authors of said code do not
use

I tend to think that having an explicit syntax for
potentially-non-injective types would be the best choice starting from
scratch (users will be surprised if their non-injective type fail to
satisfy a signature, but the error message can easily guide them
towards the right, local fix). But breaking compatibility is generally
not considered an option when evolving the OCaml language.

¹: there is a difference between "I guarantee you that this type is
not injective in this parameter" and "You cannot assume that this type
is injective in this parameter", and the latter is "more abstract"
than the former; it is the better notion for an abstract type about
which we know nothing at all (so that any type declaration may be an
instance of it). The former, stronger notion seems less useful, and so
far nobody has suggested to allow to express it.


> On Sat, Apr 27, 2013 at 5:02 PM, Jacques Garrigue
> <garrigue@math.nagoya-u.ac.jp> wrote:
>>
>> Some of you may already be aware of PR#5985
>> http://caml.inria.fr/mantis/view.php?id=5985
>>
>> To explain very shortly what is happening, a bug was found in the ocaml
>> compiler, both 4.00 and the development version, such that one that
>> convert a value from any type to any other type, bypassing all checks.
>> This is what we call a soundness bug, a hole in the type system.
>>
>> Such problems happen at times, and we are usually very fast to fix them.
>> However this time the problem is bit more subtle, because fixing it
>> straightforwardly may make impossible to write a whole category of
>> GADTs. Hence this request for feedback.
>>
>> Practical description of the problem:
>>
>> It is quite usual to write type witnesses using a GADT:
>>
>> type _ ty =
>>   | Int : int ty
>>   | Pair : 'a ty * 'b ty -> ('a * 'b) ty
>>   | Hashtbl : 'a ty * 'b ty -> ('a, 'b) Hashtbl.t ty
>>
>> This looks fine, but now suppose that we write the following code:
>>
>> module F (X : sig type 'a t end) = struct
>>    type _ ty =
>>     | Int : int ty
>>     | Pair : 'a ty * 'b ty -> ('a * 'b) ty
>>     | T : 'a ty -> 'a X.t ty
>> end
>>
>> The idea is to create a type witness with the
>> type constructor X.t instead of Hashtbl.t.
>> Now I can use it this way:
>>
>> module U = struct type 'a t = unit end
>> module M = F(U)
>> let w = M.T M.Int
>> (* val w : int U.t M.ty *)
>> let w' = match w with M.T x -> x | _ -> assert false
>> (* val w' : '_a M.ty = M.Int *)
>>
>> What this means is that we can now give an arbitrary type
>> to a witness for int. You can easily use it to build a function
>> from int to any  type:
>>
>> let f : type a. a M.ty -> int -> a =
>>   fun w x -> match w with M.Int -> x | _ -> assert false;;
>> let g : int -> float = f w';;
>>
>> If we look at the source of the problem, it lies in the fact U.t is not
>> injective.
>> I.e. when we define a GADT, we assume that all the type variables in
>> the return type can be determined from the type parameter.
>> That is, from (int U.t M.ty) we assume that the type of the argument of T
>> is (int M.ty).
>> However, since U.t is not injective, int U.t is actually equal to any type
>> 'a U.t,
>> and we can convert.
>> Note that, for known types, injectivity was already checked.
>> I.e., the following definition is not accepted:
>>
>> type _ ty =
>>   | Int : int ty
>>   | Pair : 'a ty * 'b ty -> ('a * 'b) ty
>>   | T : 'a ty -> 'a U.t ty
>>
>> However, abstract types were assumed to be injective.
>> Here we see that you cannot take this for granted.
>>
>> The problem is of course not limited to type witnesses, and not even
>> GADTs:
>> types with constrained parameters (introduced at the very beginning of
>> ocaml),
>> can also trigger it.
>> And you don't need a functor to trigger it: once you know that two types
>> are equal
>> in some scope, there are many ways to leak that information.
>>
>> =============================
>> Here comes the request for feedback:
>>
>> 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.
>>
>> How many of you are using GADTs in this way, and how dependent are you on
>> abstract types ?
>>
>>
>> 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.
>> This is implemented in branches/non-vanishing, in the subversion
>> repository.
>>         svn checkout http://caml.inria.fr/svn/branches/non-vanishing
>> Note that in that branch Hashtbl.t in the standard library is marked as
>> injective.
>> This introduces some new syntax, and libraries have to be modified to
>> benefit,
>> so the question is do we really need it?
>>
>>
>> Jacques Garrigue
>>
>> P.S.
>> 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.
>>
>>
>> --
>> Caml-list mailing list.  Subscription management and archives:
>> https://sympa.inria.fr/sympa/arc/caml-list
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

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

[Alain Frisch]

On 04/28/2013 02:02 AM, Jacques Garrigue 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.
>
> How many of you are using GADTs in this way, and how dependent are you on
> abstract types ?

FWIW, it turns out that we have very recently introduced such a case 
(and I realized it while synchronizing our version of OCaml with the trunk).

We used to have a functor with this signature:

module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) :
     sig
       module type S = sig
         type s
         type t
         val t: t ttype
         val eq: (s, t T.t) TypEq.t
       end
       val check: 'a ttype -> (module S with type s = 'a) option
     end

ttype is our type representing type structures at runtime.  The functors 
returns a function that checks if a given runtime type represents an 
instance of an unary abstract type constructor passed in argument to the 
functor (the functors check that this is indeed an abstract type).   In 
case of success, the function returns the ttype of the type constructor 
argument.  The existential is encoded with a first-class module and the 
type-equality is encoded in the classical way (('a, 'b) TypEq.t 
witnesses the equality of 'a and 'b:  type (_, _) t = Eq: ('a, 'a) t).

A GADT was recently introduced to replace this with a more direct 
representation:

module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) :
     sig
       type _ is_t = Is: 'a ttype -> 'a T.t is_t
       val check: 'a ttype -> 'a is_t option
     end

The problem is that this doesn't work any more (because T.t is not 
injective).

For now, I think I'll use:


module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) :
     sig
       type _ is_t = Is: 'b ttype * ('a, 'b T.t) TypEq.t -> 'a is_t
       val is_t: 'a ttype -> 'a is_t option
     end


which is accepted and roughly equivalent (by opening the equality 
witness, one can retrieve the static equality 'a == 'b T.t).


Alain

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

[Jacques Garrigue]

On 2013/07/01, at 23:47, Alain Frisch <alain@frisch.fr> wrote:

> A GADT was recently introduced to replace this with a more direct representation:
> 
> module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) :
>    sig
>      type _ is_t = Is: 'a ttype -> 'a T.t is_t
>      val check: 'a ttype -> 'a is_t option
>    end
> 
> The problem is that this doesn't work any more (because T.t is not injective).
> 
> For now, I think I'll use:
> 
> module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) :
>    sig
>      type _ is_t = Is: 'b ttype * ('a, 'b T.t) TypEq.t -> 'a is_t
>      val check : 'a ttype -> 'a is_t option
>    end
> 
> which is accepted and roughly equivalent (by opening the equality witness, one can retrieve the static equality 'a == 'b T.t).

Nice natural example, and nice workaround.

Of course, this is not strictly equivalent.
For instance suppose the following function:
  let f (type a) (tt : a T.t ttype) =
     match check tt with None -> assert false
     | Some (Is (tta, Eq)) -> (tta : a ttype)
The pattern matching will succeed, but tta will only have type "a ttype"
if T.t is injective. The nice part is that this is delayed to the use site,
where we may have more information about T.t, so this trick may still
be useful after introducing injectivity annotations.

Anyway, I suppose that this will work fine for you: check is intended
to be called on unknown types, so the missing equality should not
be a problem.

Jacques

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

[Alain Frisch]

On 07/02/2013 01:20 AM, Jacques Garrigue wrote:
> On 2013/07/01, at 23:47, Alain Frisch <alain@frisch.fr> wrote:
>
>> A GADT was recently introduced to replace this with a more direct representation:
>>
>> module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) :
>>     sig
>>       type _ is_t = Is: 'a ttype -> 'a T.t is_t
>>       val check: 'a ttype -> 'a is_t option
>>     end
>>
>> The problem is that this doesn't work any more (because T.t is not injective).
>>
>> For now, I think I'll use:
>>
>> module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) :
>>     sig
>>       type _ is_t = Is: 'b ttype * ('a, 'b T.t) TypEq.t -> 'a is_t
>>       val check : 'a ttype -> 'a is_t option
>>     end
>>
>> which is accepted and roughly equivalent (by opening the equality witness, one can retrieve the static equality 'a == 'b T.t).
>
> Nice natural example, and nice workaround.

Btw, this is also an example where type-based disambiguation in presence 
of a GADT would be useful.  For instance, we currently need to write:

     match StringMap_matcher.check t with
     | Some (StringMap_matcher.Is (s, TypEq.Eq)) -> vmap (StringMap.map 
(of_value ~t:s env) x)
     | None -> ...

while one could write:

     match StringMap_matcher.check t with
     | Some (Is (s, Eq)) -> vmap (StringMap.map (of_value ~t:s env) x)
     | None -> ...

(see http://caml.inria.fr/mantis/view.php?id=6023 )

> Of course, this is not strictly equivalent.
> For instance suppose the following function:
>    let f (type a) (tt : a T.t ttype) =
>       match check tt with None -> assert false
>       | Some (Is (tta, Eq)) -> (tta : a ttype)
> The pattern matching will succeed, but tta will only have type "a ttype"
> if T.t is injective. The nice part is that this is delayed to the use site,
> where we may have more information about T.t, so this trick may still
> be useful after introducing injectivity annotations.
>
> Anyway, I suppose that this will work fine for you: check is intended
> to be called on unknown types, so the missing equality should not
> be a problem.

Indeed!

In some cases (in particular to add annotations to make sense of error 
messages), it would be useful to be able to name the type constructor 
introduced by opening the GADT to match the existential type.  (I'd put 
this rather high on my wish list around GADTs!)


Alain

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

[Gabriel Scherer]

> In some cases (in particular to add annotations to make sense of error
> messages), it would be useful to be able to name the type constructor
> introduced by opening the GADT to match the existential type.  (I'd put this
> rather high on my wish list around GADTs!)

Indeed, virtually anyone that used GADTs in OCaml encountered that
problem and has a way to name existential type high on his/her
wishlist. We discussed a few ideas in the following bugtracking
dicussion:

  http://caml.inria.fr/mantis/view.php?id=5780

On Wed, Jul 3, 2013 at 6:08 PM, Alain Frisch <alain@frisch.fr> wrote:
> On 07/02/2013 01:20 AM, Jacques Garrigue wrote:
>>
>> On 2013/07/01, at 23:47, Alain Frisch <alain@frisch.fr> wrote:
>>
>>> A GADT was recently introduced to replace this with a more direct
>>> representation:
>>>
>>> module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) :
>>>     sig
>>>       type _ is_t = Is: 'a ttype -> 'a T.t is_t
>>>       val check: 'a ttype -> 'a is_t option
>>>     end
>>>
>>> The problem is that this doesn't work any more (because T.t is not
>>> injective).
>>>
>>> For now, I think I'll use:
>>>
>>> module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) :
>>>     sig
>>>       type _ is_t = Is: 'b ttype * ('a, 'b T.t) TypEq.t -> 'a is_t
>>>       val check : 'a ttype -> 'a is_t option
>>>     end
>>>
>>> which is accepted and roughly equivalent (by opening the equality
>>> witness, one can retrieve the static equality 'a == 'b T.t).
>>
>>
>> Nice natural example, and nice workaround.
>
>
> Btw, this is also an example where type-based disambiguation in presence of
> a GADT would be useful.  For instance, we currently need to write:
>
>     match StringMap_matcher.check t with
>     | Some (StringMap_matcher.Is (s, TypEq.Eq)) -> vmap (StringMap.map
> (of_value ~t:s env) x)
>     | None -> ...
>
> while one could write:
>
>     match StringMap_matcher.check t with
>     | Some (Is (s, Eq)) -> vmap (StringMap.map (of_value ~t:s env) x)
>     | None -> ...
>
> (see http://caml.inria.fr/mantis/view.php?id=6023 )
>
>
>> Of course, this is not strictly equivalent.
>> For instance suppose the following function:
>>    let f (type a) (tt : a T.t ttype) =
>>       match check tt with None -> assert false
>>       | Some (Is (tta, Eq)) -> (tta : a ttype)
>> The pattern matching will succeed, but tta will only have type "a ttype"
>> if T.t is injective. The nice part is that this is delayed to the use
>> site,
>> where we may have more information about T.t, so this trick may still
>> be useful after introducing injectivity annotations.
>>
>> Anyway, I suppose that this will work fine for you: check is intended
>> to be called on unknown types, so the missing equality should not
>> be a problem.
>
>
> Indeed!
>
> In some cases (in particular to add annotations to make sense of error
> messages), it would be useful to be able to name the type constructor
> introduced by opening the GADT to match the existential type.  (I'd put this
> rather high on my wish list around GADTs!)
>
>
> Alain
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

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

[oleg]

> Indeed, virtually anyone that used GADTs in OCaml encountered that
> problem and has a way to name existential type high on his/her
> wishlist. We discussed a few ideas in the following bugtracking
> dicussion:
>
>   http://caml.inria.fr/mantis/view.php?id=5780

Just in case, here is the error message produced by GHC for the
equivalent example. 

Code:

{-# LANGUAGE GADTs #-}

data E a where
    B :: Bool -> E Bool
    A :: E (a -> b) -> E a -> E b

eval :: E a -> a
eval (B x)   = x
eval (A f x) = (eval f) x

The error message:

/tmp/ga.hs:9:25:
    Couldn't match type `a1' with `E a1'
      `a1' is a rigid type variable bound by
           a pattern with constructor
             A :: forall b a. E (a -> b) -> E a -> E b,
           in an equation for `eval'
           at /tmp/ga.hs:9:7
    In the second argument of `eval', namely `x'
    In the expression: (eval f) x
    In an equation for `eval': eval (A f x) = (eval f) x

The gist is using the type variable name 'a' from the definition of
GADT, and attaching the numeric suffix to disambiguate. (GHC does that all
the time -- and I believe OCaml does something similar in many cases,
only not for GADTs.) What helps in particular I believe is quoting the
clause from the GADT declaration, so we can see where the name 'a'
comes from. So, perhaps if the error message can be improved with
giving more information about the error, the problem will be solved
without additional syntax?

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

[Alain Frisch]

On 07/04/2013 08:07 AM, oleg@okmij.org wrote:
> The gist is using the type variable name 'a' from the definition of
> GADT, and attaching the numeric suffix to disambiguate. (GHC does that all
> the time -- and I believe OCaml does something similar in many cases,
> only not for GADTs.) What helps in particular I believe is quoting the
> clause from the GADT declaration, so we can see where the name 'a'
> comes from. So, perhaps if the error message can be improved with
> giving more information about the error, the problem will be solved
> without additional syntax?

Naming types created by opening GADT existentials is useful not only for 
error messages, but also to have a way to refer to that type in the 
branch (for instance to instantiate locally a functor whose argument 
refers to that type).

-- Alain

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

[oleg]

> Naming types created by opening GADT existentials is useful not only for 
> error messages, but also to have a way to refer to that type in the 
> branch (for instance to instantiate locally a functor whose argument 
> refers to that type).

That is true, but isn't this a separate problem? Do you often need to
refer to the type in a branch? On the other hand, good error messages
are needed often, or all the time. 

BTW, GHC does allow naming the type of the existential (I can't
remember the last time I used that for real though). For example,

data E a where
    B :: Bool -> E Bool
    A :: E (a -> b) -> E a -> E b

eval :: E a -> a
eval (B x)   = x
eval (A (f::E (u->v)) x) = (eval f) ((eval x)::u)

Here, I named the type of the argument, which is quantified by the
existential, as u. However, GHC does not use those types in the error
message. For example, if I make a mistake

eval :: E a -> a
eval (B x)   = x
eval (A (f::E (u->v)) x) = (eval f) (x::u)

I get the error message which talks about the type a
/tmp/ga.hs:9:38:
    Couldn't match type `a1' with `E a1'
      `a1' is a rigid type variable bound by
           a pattern with constructor
             A :: forall b a. E (a -> b) -> E a -> E b,
           in an equation for `eval'
           at /tmp/ga.hs:9:7
    In the second argument of `eval', namely `(x :: u)'
    In the expression: (eval f) (x :: u)
    In an equation for `eval':
        eval (A (f :: E (u -> v)) x) = (eval f) (x :: u)

I would argue that is reasonable: the error message quotes the
declaration of GADT; it is only logical it would use the types from
that declaration.

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

[Alain Frisch]

On 07/05/2013 12:30 PM, oleg@okmij.org wrote:
>> Naming types created by opening GADT existentials is useful not only for
>> error messages, but also to have a way to refer to that type in the
>> branch (for instance to instantiate locally a functor whose argument
>> refers to that type).
>
> That is true, but isn't this a separate problem? Do you often need to
> refer to the type in a branch? On the other hand, good error messages
> are needed often, or all the time.

To be clear: the GHC way to report errors seems good to me.  But even if 
the default error message is improved, it is still helpful to be able to 
name the existential type simply to be able to write a type annotation 
mentioning that type somewhere deep in the branch (as a way to track 
down the actual error).  Typically, only a very small number of #exN 
types exist in a given scope, so the fact that the error message does 
not tell where they come from is not a blocking point in making sense of 
the error, and not being able to name the type is more problematic.

And of course, there are many other cases where it is useful to name the 
type, not only to track errors, but as ways to document the code or 
simply to be able to write it at all (especially when using local modules).

And to answer your question: yes, I've had to introduce a local 
polymorphic function (with a locally abstract type) quite often to 
work-around the lack of naming facility.

-- Alain

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

[Jacques Garrigue]

On 2013/07/04, at 1:08, Alain Frisch <alain@frisch.fr> wrote:

> Btw, this is also an example where type-based disambiguation in presence of a GADT would be useful.  For instance, we currently need to write:
> 
>    match StringMap_matcher.check t with
>    | Some (StringMap_matcher.Is (s, TypEq.Eq)) -> vmap (StringMap.map (of_value ~t:s env) x)
>    | None -> ...
> 
> while one could write:
> 
>    match StringMap_matcher.check t with
>    | Some (Is (s, Eq)) -> vmap (StringMap.map (of_value ~t:s env) x)
>    | None -> ...
> 
> (see http://caml.inria.fr/mantis/view.php?id=6023 )

In theory, it would be OK to assume that all pattern-matchings may contain GADT type constructors.
The only real problem is with let's: if they contain GADTs, we must use the code for pattern-matching, which doesn't handle unused definition warnings in the same way… Having all non recursive let's go through this code would have a high impact on warnings.

If unused definition warnings could be separated from type checking this would be much easier.

> In some cases (in particular to add annotations to make sense of error messages), it would be useful to be able to name the type constructor introduced by opening the GADT to match the existential type.  (I'd put this rather high on my wish list around GADTs!)

I did to.
As Gabriel mentioned, there was a discussion about syntax on Mantis.

 http://caml.inria.fr/mantis/view.php?id=5780

As is often the case with syntax, this ended with no agreement, so there is no such feature…

Actually, the problem with syntax is a bit deeper than that.
Namely, my real concern is that currently locally abstract types cannot handle abstract row types.
I think this is a severe limitation, at least for some applications.
Maybe this problem should be solved first, as adding new syntax for existential types without solving this will only make it deeper.

	Jacques

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

[Alain Frisch]

On 07/04/2013 03:00 AM, Jacques Garrigue wrote:
> In theory, it would be OK to assume that all pattern-matchings may contain GADT type constructors.
> The only real problem is with let's: if they contain GADTs, we must use the code for pattern-matching, which doesn't handle unused definition warnings in the same way… Having all non recursive let's go through this code would have a high impact on warnings.

If this is the only problem with the direct approach (not depending on 
backtracking), maybe the treatment of warnings can be parametrized to 
behave as expected?


> If unused definition warnings could be separated from type checking this would be much easier.

Maybe I'm wrong, but it seems to me that achieving the same behavior 
would require to duplicate of lot of the "data-flow" logic in the 
type-checker, thus increasing the global complexity (and the risk to 
have diverging behaviors).



Alain

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

[Jacques Garrigue]

On 2013/07/04, at 17:14, Alain Frisch <alain@frisch.fr> wrote:

> On 07/04/2013 03:00 AM, Jacques Garrigue wrote:
>> In theory, it would be OK to assume that all pattern-matchings may contain GADT type constructors.
>> The only real problem is with let's: if they contain GADTs, we must use the code for pattern-matching, which doesn't handle unused definition warnings in the same way… Having all non recursive let's go through this code would have a high impact on warnings.
> 
> If this is the only problem with the direct approach (not depending on backtracking), maybe the treatment of warnings can be parametrized to behave as expected?

This does not remove the need for backtracking, as the backtracking occurs in the code for typing pattern-matching.
It is needed to detect where GADTs are actually used.
(By the way this backtracking concerns only the typing of pattern-matching, and it is not costly, so there is no real need to avoid it).
The goal is to allow to switch between the code for let-in and the code for match freely.

>> If unused definition warnings could be separated from type checking this would be much easier.
> 
> Maybe I'm wrong, but it seems to me that achieving the same behavior would require to duplicate of lot of the "data-flow" logic in the type-checker, thus increasing the global complexity (and the risk to have diverging behaviors).

I just mean that if it could abstracted so that one could call the same use-tracking function for type_cases and type_let, things would be simpler. The goal here is factoring, not duplicating.

Jacques Garrigue