[Caml-list] Variance of GADT parameters

[Caml-list] Variance of GADT parameters

[Gabriel Scherer]

I've been playing with GADTs and noticed that the condition on
parameter variance is very restrictive.

The two following examples fail:

  type +_ const =
  | Const : int -> int expr

  type +_ expr =
  | Const : 'a -> 'a expr
  | Prod : 'a expr * 'b expr -> ('a * 'b) expr

  Error: In this GADT definition, the variance of some parameter
  cannot be checked

I looked at the source, and this is what I could infer of the current
typer behavior: parameter variance check will fail (on non-invariant
parameters) as soon as they appear *instantiated* (not just
a variable) in one of the GADT branch return type. The two examples
above fail for this reason: `const` parameter is instantiated with int
and `expr` with ('a * 'b).

Would it be possible to relax this condition a bit? Intuitively, I
would say that:
1. variables that do not appear in the instantiations of the return
   type always satisfy their variance constraint (for the branch)
2. variables that appear covariantly in the instantiations of the
   return type should satisfy their constraints on the argument types
3. variables that appaear contravariantly should satisfy the
   *reversed* constraints on the argument type

For example, with a GADT having some argument type σ('a) using
a variable instantiated in its return type :

  type +_ t = | C : σ('a) -> ('a -> unit) t

If α ≤ β, then α t ≤ β t only if α, β are of the form α' → unit, β' →
unit, so α' *≥* β' and α t ≤ β t only if σ(α') ≤ σ(β'), that is 'a
appears *contravariantly* in σ.

Is the above condition sound? It would allow my two examples above. If
not, or if it's not reasonable to implement, is there a weaker
condition that would make those example work?

Having a powerful enough variance inference is important if we want to
use GADTs to implement abstract data types – that's how I ran into
this problem.

Re: [Caml-list] Variance of GADT parameters

[Jeremy Yallop]

Dear Gabriel,

Here's an example of the sort of misbehaviour that the variance
condition on GADTs is intended to prevent.  Consider what happens when
we decorate our old friend the equality GADT with a variance
annotation on one of the type parameters (it doesn't matter which):

 type (_, +_) eq = Refl : ('a, 'a) eq

Even this fairly harmless looking addition allows us to write the
dreaded 'magic' function of type 'a -> 'b.  Here's how (somewhat
untested):

 let magic : 'a 'b. 'a -> 'b =
     (* Dramatis personae:
      * i, the input type
      * o, the output type
      * x, a value of the input type
      *)
  fun (type i) (type o) (x : i) ->

   (* Step 1. Coerce a (legitimate) proof of <m:t> = <m:t> (any t) to a
    *         (dodgy) proof of <m:t> = < >.
    *)
   let bad_proof (type t) = (Refl : (<m:t>, <m:t>) eq :>
                               (<m:t>, < >) eq) in

   (* Step 2. Use GADT pattern matching / type refinement to write a
    *         (legitimate) function from a proof of t = < > (any t) and a
    *         value of < > to a value of t.
    *)
   let downcast_1 : type a. (a, < >) eq -> < > -> a =
                      fun (type a) (Refl : (a, < >) eq) (s : < >) ->
                           (s :> a) in

   (* Step 3. Apply the (legitimate) function to the (dodgy) proof to
    *         obtain a (dodgy) conversion from < > to <m:o>.
    *)
   let downcast_2 : < > -> <m:o> = downcast_1 bad_proof in

   (* Step 4. Wrap up x in an object, and hide it behind a (legitimate)
    *         upcast to < >.
    *)
   let wrapped_x = ((object method m = x end) :> < >) in

   (* Step 5. Apply the (dodgy) conversion to the wrapped x to obtain a
    *         value of type <m:o>, from which we can extract x at type o.
    *)
     (downcast_2 wrapped_x) # m

If I understand correctly, constraints 1-3 alone wouldn't be enough to
prevent this sort of thing.

Kind regards,

Jeremy.

[Caml-list] Re: Variance of GADT parameters

[Jacques Garrigue]

On 2012/02/10, at 19:11, Gabriel Scherer wrote:

> I've been playing with GADTs and noticed that the condition on
> parameter variance is very restrictive.
> 
> The two following examples fail:
> 
>   type +_ const =
>   | Const : int -> int expr
> 
>   type +_ expr =
>   | Const : 'a -> 'a expr
>   | Prod : 'a expr * 'b expr -> ('a * 'b) expr
> 
>   Error: In this GADT definition, the variance of some parameter
>   cannot be checked
> 
> I looked at the source, and this is what I could infer of the current
> typer behavior: parameter variance check will fail (on non-invariant
> parameters) as soon as they appear *instantiated* (not just
> a variable) in one of the GADT branch return type. The two examples
> above fail for this reason: `const` parameter is instantiated with int
> and `expr` with ('a * 'b).
> 
> Would it be possible to relax this condition a bit? Intuitively, I
> would say that:
> 1. variables that do not appear in the instantiations of the return
>   type always satisfy their variance constraint (for the branch)
> 2. variables that appear covariantly in the instantiations of the
>   return type should satisfy their constraints on the argument types
> 3. variables that appaear contravariantly should satisfy the
>   *reversed* constraints on the argument type
> 
> For example, with a GADT having some argument type σ('a) using
> a variable instantiated in its return type :
> 
>   type +_ t = | C : σ('a) -> ('a -> unit) t
> 
> If α ≤ β, then α t ≤ β t only if α, β are of the form α' → unit, β' →
> unit, so α' *≥* β' and α t ≤ β t only if σ(α') ≤ σ(β'), that is 'a
> appears *contravariantly* in σ.
> 
> Is the above condition sound? It would allow my two examples above. If
> not, or if it's not reasonable to implement, is there a weaker
> condition that would make those example work?
> 
> Having a powerful enough variance inference is important if we want to
> use GADTs to implement abstract data types – that's how I ran into
> this problem.

As Jeremy pointed already, the question of variance in presence of GADTs
is devilishly complicated.
Your conditions are much too simple to be sufficient.
They seem to be the conditions we already have for constrained types.

I'm ready to buy anything, but at least I need a proof of soundness.

At the very least, the conditions seem to be
1) an instantiated type cannot include type variables that appear elsewhere in the return type
     (Jeremy's example)
2) if an instantiated type is marked as contravariant, it should not be possible to smuggle
     a value of this type through the arguments
     (the example in the ocamlgadt tutorial)
3) something similar for the contravariant case

However this is completely unclear whether this would be sufficient.

For your first example, the contravariant version is clearly unsound:

type pint = private int
type -_ const = Const : int -> int const

let eval : type a. a t -> a = fun (Const c) -> c
let make_pint (x : int) : pint = eval (Const x :> pint const)

I think that your examples are ok, but I'm not sure how to generalize that.

	Jacques Garrigue

[Caml-list] Re: Variance of GADT parameters

[Gabriel Scherer]

Thank you, Jacques and Jeremy, for the examples. Indeed that looks quite subtle.

I found it helpful to write an informal proof of covariance of the
following type:

  type +_ expr =
    | Val : 'a -> 'a expr
    | Prod : 'a expr * 'b expr -> ('a * 'b) expr

Or, in a more explicit formulation using imaginary syntax with
explicit existential variables and equalities.

  type +'a expr =
    | Val of 'b . 'b with ('a = 'b)
    | Prod of 'b 'c. 'b expr * 'c expr with ('a = 'b * 'c)

The informal proof goes as follow: assuming α ≤ α', we wish to show
that α expr ≤ β expr. For a given (t : α expr):
  - if (t) is (Val (v : α)), then by α ≤ α' we have (v : α') so (Val v
: α' expr)
  - if (t) is Prod((t1 : β expr), (t2 : γ expr)), with (α = β * γ), then
    we have (β * γ ≤ α'). *By inversion* we know that there must exist
β', γ' with
    α' = β' * γ', β ≤ β' and γ ≤ γ'. We therefore have (t1 : β' expr),
(t2 : γ' expr),
    and therefore (Prod(t1,t2) : α' expr)

The core of the proof is an inversion lemma for subtyping at product types:
    if β*γ ≤ α' then α' is of the form β'*γ' with β≤β', γ≤γ'

I believe this is true of OCaml product types, and can be generalized
to some other OCaml types. It would not be true if we had a top type,
and it would be unsafe to coerce (Prod (t1, t2)) into (⊤ expr) – this
is clear if we remove the Val case: if expr only had a Prod case, one
could write a function (⊤ expr → ⊥), with no case at all, that would
be accepted by the type-checker as ⊤ and ∃βγ.β*γ do not overlap.

The strength of the inversion lemma depends a lot on the details of
the theory. For example, if α = int and α ≤ α', do we have α' = int?
And if α ≥ α'? I believe the answer to the α ≤ α' case is "yes", which
would make the (type +_ expr = Const : int -> int expr) case correctly
covariant, but as Jacques showed the answer is no in the contravariant
case α ≥ α', we have (int ≥≠ private int).

I think this technique of inversion can be generalized to arbitrary
GADT constructors
  type (α₁,α₂..αm) t =
    ...
  | C of ∃β₁β₂...βn. σ with (α₁ = τ₁, α₂ = τ₂... αm = τm)

I'm under the impression that they give something that looks a bit
like my previous conditions, with additional restrictions –
eg. restricted to types where suitable inversion principles apply. In
particular, existential variables of the instances of the parameters
(that is, the set of βi that appear in each τj) must not overlap –
this rules out the (('a,+'a) eq) example of Jeremy.

I'm going to think a bit more about this. What do you think of the
"proof" in the Prod case? Is there such an inversion principle for the
OCaml type theory?

On Sat, Feb 11, 2012 at 2:51 AM, Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
> On 2012/02/10, at 19:11, Gabriel Scherer wrote:
>
>> I've been playing with GADTs and noticed that the condition on
>> parameter variance is very restrictive.
>>
>> The two following examples fail:
>>
>>   type +_ const =
>>   | Const : int -> int expr
>>
>>   type +_ expr =
>>   | Const : 'a -> 'a expr
>>   | Prod : 'a expr * 'b expr -> ('a * 'b) expr
>>
>>   Error: In this GADT definition, the variance of some parameter
>>   cannot be checked
>>
>> I looked at the source, and this is what I could infer of the current
>> typer behavior: parameter variance check will fail (on non-invariant
>> parameters) as soon as they appear *instantiated* (not just
>> a variable) in one of the GADT branch return type. The two examples
>> above fail for this reason: `const` parameter is instantiated with int
>> and `expr` with ('a * 'b).
>>
>> Would it be possible to relax this condition a bit? Intuitively, I
>> would say that:
>> 1. variables that do not appear in the instantiations of the return
>>   type always satisfy their variance constraint (for the branch)
>> 2. variables that appear covariantly in the instantiations of the
>>   return type should satisfy their constraints on the argument types
>> 3. variables that appaear contravariantly should satisfy the
>>   *reversed* constraints on the argument type
>>
>> For example, with a GADT having some argument type σ('a) using
>> a variable instantiated in its return type :
>>
>>   type +_ t = | C : σ('a) -> ('a -> unit) t
>>
>> If α ≤ β, then α t ≤ β t only if α, β are of the form α' → unit, β' →
>> unit, so α' *≥* β' and α t ≤ β t only if σ(α') ≤ σ(β'), that is 'a
>> appears *contravariantly* in σ.
>>
>> Is the above condition sound? It would allow my two examples above. If
>> not, or if it's not reasonable to implement, is there a weaker
>> condition that would make those example work?
>>
>> Having a powerful enough variance inference is important if we want to
>> use GADTs to implement abstract data types – that's how I ran into
>> this problem.
>
> As Jeremy pointed already, the question of variance in presence of GADTs
> is devilishly complicated.
> Your conditions are much too simple to be sufficient.
> They seem to be the conditions we already have for constrained types.
>
> I'm ready to buy anything, but at least I need a proof of soundness.
>
> At the very least, the conditions seem to be
> 1) an instantiated type cannot include type variables that appear elsewhere in the return type
>     (Jeremy's example)
> 2) if an instantiated type is marked as contravariant, it should not be possible to smuggle
>     a value of this type through the arguments
>     (the example in the ocamlgadt tutorial)
> 3) something similar for the contravariant case
>
> However this is completely unclear whether this would be sufficient.
>
> For your first example, the contravariant version is clearly unsound:
>
> type pint = private int
> type -_ const = Const : int -> int const
>
> let eval : type a. a t -> a = fun (Const c) -> c
> let make_pint (x : int) : pint = eval (Const x :> pint const)
>
> I think that your examples are ok, but I'm not sure how to generalize that.
>
>        Jacques Garrigue
>

[Caml-list] Re: Variance of GADT parameters

[Jacques Garrigue]

On 2012/02/13, at 2:36, Gabriel Scherer wrote:

> Thank you, Jacques and Jeremy, for the examples. Indeed that looks quite subtle.
> 
> I found it helpful to write an informal proof of covariance of the
> following type:
> 
>  type +_ expr =
>    | Val : 'a -> 'a expr
>    | Prod : 'a expr * 'b expr -> ('a * 'b) expr
> 
> Or, in a more explicit formulation using imaginary syntax with
> explicit existential variables and equalities.
> 
>  type +'a expr =
>    | Val of 'b . 'b with ('a = 'b)
>    | Prod of 'b 'c. 'b expr * 'c expr with ('a = 'b * 'c)
> 
> The informal proof goes as follow: assuming α ≤ α', we wish to show
> that α expr ≤ β expr. For a given (t : α expr):
>  - if (t) is (Val (v : α)), then by α ≤ α' we have (v : α') so (Val v
> : α' expr)
>  - if (t) is Prod((t1 : β expr), (t2 : γ expr)), with (α = β * γ), then
>    we have (β * γ ≤ α'). *By inversion* we know that there must exist
> β', γ' with
>    α' = β' * γ', β ≤ β' and γ ≤ γ'. We therefore have (t1 : β' expr),
> (t2 : γ' expr),
>    and therefore (Prod(t1,t2) : α' expr)
> 
> The core of the proof is an inversion lemma for subtyping at product types:
>    if β*γ ≤ α' then α' is of the form β'*γ' with β≤β', γ≤γ'
> 
> The strength of the inversion lemma depends a lot on the details of
> the theory. For example, if α = int and α ≤ α', do we have α' = int?
> And if α ≥ α'? I believe the answer to the α ≤ α' case is "yes", which
> would make the (type +_ expr = Const : int -> int expr) case correctly
> covariant, but as Jacques showed the answer is no in the contravariant
>  case α ≥ α', we have (int ≥≠ private int).

[...]

> I'm going to think a bit more about this. What do you think of the
> "proof" in the Prod case? Is there such an inversion principle for the
> OCaml type theory?

The proof looks fine.
Subtyping in OCaml has not been much studied.
You can find a short draft attempting to specify the current behavior
on my publication page.
Again I wonder whether you are not going to get problems with abstraction.
At first sight, no: if when you define a GADT t, the type u is abstract, then
it will have no supertype in any environment where we use t.
But if you think more carefully, you realize that if in the future we allow
(gadt-)unification between abstract types, everything breaks, since abstract
types may end up having supertypes in a local environment.
So it looks like the only types you can allow for instantiation are concrete
datatypes and well-known types (abstract types defined in the initial environment
or in the current module).

Jacques Garrigue

[Caml-list] Re: Variance of GADT parameters

[Jacques Garrigue]

Dear Gabriel,

Thank you for this detailed analysis.
It is comforting to know that the current criterion is sound!

I have a few remarks/questions.

> # A criterion in the general case
> 
> I believe (and have a draft of proof in the attached technical annex)
> that the requirement of Simonet&Pottier is equivalent, in the equality
> case, to the following criterion that *could* be implemented in
> a type-checker – more easily than by adding a general constraint
> solver.
> 
>  Given variance annotations (≤i) for the type ᾱ t, the type
>  constructor
>    K : ∀ᾱ∀β̄[α₁ = T₁(β̄), α₂ = T₂(β̄)...] τ̄ → ᾱ t
>  or equivalently (in OCaml syntax)
>    K : τ̄ → (T₁(β̄),T₂(β̄)...) t
>  respects the variance if all the conditions below are met:
> 
>  1. Non-interference: if an existential variable β appears in several
>     Ti(β̄), then all its occurences in the whole type expression
>     (T₁(β̄),T₂(β̄)...) t must be in invariant position.
> 
>  2. Upward/downward closure, or eliminability: for each i, β̄, α', if
>     (Ti(β̄) ≤i α') holds then α' is of the form Ti(β̄').
> 
>  3. Constructor parameters variance: the variance of the β̄ in the
>     type expression (T₁(β̄),T₂(β̄)...) t must respect their variance in
>     the constructor parameters τ̄ – just like if we had a non-GADT
>     declaration in term of the β̄, (type β̄ t = K of τ̄ | ...).
> 
> I believe this is sound, not unreasonably difficult to check, and
> would help in a lot of concrete cases that are currently rejected.

Have you considered my comment on the interaction with abstraction:

>> Again I wonder whether you are not going to get problems with abstraction.
>> At first sight, no: if when you define a GADT t, the type u is abstract, then
>> it will have no supertype in any environment where we use t.
>> But if you think more carefully, you realize that if in the future we allow
>> (gadt-)unification between abstract types, everything breaks, since abstract
>> types may end up having supertypes in a local environment.
>> So it looks like the only types you can allow for instantiation are concrete
>> datatypes and well-known types (abstract types defined in the initial environment
>> or in the current module).

In the future, we really want to be able to instantiate normal abstract types with
GADT pattern matching, not just local ones.
Wouldn't it mean that you can never now whether an abstract type is upward closed?

module M : sig type t type u = private int val eq : (t,u) eq end =
  struct type u = int  type t = u  let eq : (t,u) eq = Eq end

Note that this doesn't means that I could build a proof of unsoundness.
You criterion may actually be too restrictive.
Actually, my counter-example with a private type used a contravariant gadt.

> # Discussion of private types and contravariance
> 
> There is something quite disturbing in the idea that the mere
> existence of private types creates a strong asymmetry between
> covariant and contravariant parameters for GADTs: while upward-closed
> types are relatively common (so that we can expect "the usual
> examples" of GADTs to have "the expected variance"), there are no more
> downward-closed types, which means no contravariant constrained
> parameter.
> 
> Upward or downward closure can be easily decided on fully transparent
> types (types whose definition is known). But there is a problem with
> opaque types: as we don't know how they were defined, we can't check
> if they are upward/downward closed.

Sorry about the above comment.
This seems to be what you are referring to here.
I would just remind you that we have lots of opaque types around,
so that this may be a strong limitation in practice.
Of course we can still apply the criterion that opaque types in
the initial environment (builtin + pervasives) cannot be circumvented,
but this a kind of hack.

A stronger approach would be to check interfaces to ensure that abstraction
cannot be broken.
I was already thinking about that for making abstract types covariant when
the module interface only allows covariant uses.
But this can be very tricky.

> From a design point of view, the "right thing" would be to let people
> publish this information in the signature for an opaque type. Just as
> we can annotate the type with variance information, we should be able
> to publish its upward/downward closure properties.

This is rather heavy-weight...

> Another natural question is: what if we added the symmetric of the
> "private" concept, a type (blind σ) strictly above σ for all types?
> Would we lose all reasonable variance properties on OCaml types?

Is there any use for these "blind" types ?
What do you mean by "all reasonable variance properties" ?
This should only have an impact on GADTs, isn'it ?

> One idea from Didier Rémy is to allow, when defining a new type 't'
> (not a type synonym), to define it as "non-privatizable"
> (and correspondingly non-blindable). We or another programmer would
> then not be allowed to define a type 'private t'. In exchange for this
> lost flexibility, 't' would be downward-closed. The idea is that
> introducing private types increased our freedom, and reciprocally
> lessened our ability to reason about "what cannot be done";
> non-privatizable annotations allow to locally make the inverse choice
> of losing 'private' for better subtyping properties.

This one would really go against abstraction...

> From a pragmatic standpoint, I suspect the current restrictions
> 'private' entails on the GADT variance checks are not going to be
> really problematic in practice. We tend to use covariant types
> (data) more often than contravariant types (computations). The OCaml
> type system is already skewed towards covariance in one place: while
> the relaxed value restriction (which, I recall, is the reason why
> I needed GADT variance in the first place) would work equally well
> to generalize variables that appear only in covariant or only in
> contravariant positions, the relaxation is implemented in the
> type-checker only for covariant parameters. And I have not yet heard
> of someone requesting generalization of only-contravariant
> parameters, so apparently treating contravariant parameters as
> second-class citizens is ok among OCaml users.

Contravariant parameters are not generalized because this would
be unsound:

let f : 'a -> unit = let r = ref [| |] in
  fun x -> if !r = [| |] then r := [|x|] else (!r).(0) <- x

let crash = f 1.0; f 1

It is unsound to add a top type to the ocaml type hierarchy.
But the "blind" types would of course be sound.

> # A theoretical open-world approach
> 
> Some people may consider the upward-downward criterion as
> fundamentally unsatisfying because of the closed-world assumption it
> makes: it is not preserved by enrichment of the OCaml subtyping
> lattice.
> 
> There is another possibility to get some variance properties out of
> GADTs that still works in an open-world system: allow GADTs
> constraints to have subtyping constraints, instead of only equality
> constraint.
> 
> For example we could define the type of well-typed expressions in
> this way (note the ≥ in constraints):
>  type +α expr =
>    | Val : ∀α. α → α expr
>    | Prod : ∀α∀βγ[α ≥ β*γ] β*γ → α expr
>    | Priv : ∀α[α ≥ priv_int] priv_int → α expr
> 
> It is trivial that this definition is covariant in its type parameter,
> because covariance was baked in the definition. Indeed, if α≤α'
> and α≥β*γ, then α'≥β*γ by transitivity: the constraint is preserved by
> going to a larger type. In the soundness requirement of
> Simonet&Pottier, one can use the exact same existential variables on
> both sides (β̄':=β̄), and the constraints will be satisfied.
> 
> The downside of this easier covariance property is that we get weaker
> types on deconstruction (pattern matching of GADT values): when
> matching on a (α t), in the Prod clause, we only know that (α ≥ β*γ)
> rather than (α = β*γ) – note that we could regain the stronger
> hypothesis by locally using the closed-world assumption.
> 
> This simple idea has two potential problems:
> 
> 1. This may not be implementable as part of the current OCaml
>   type-checker, which uses type equalities internally and has more
>   limited subtyping support (in particular we can't abstract over
>   arbitrary subtyping assumptions). That said, this particular way of
>   adding subtyping hypothesis in the context might be simple enough
>   for it to handle.
> 
> 2. Getting a weaker hypothesis may be unusable: maybe the usual GADT
>   programs really make use of the equality assumptions, and going for
>   subtyping assumptions would make untypable programs that would be
>   perfectly fine under the closed-world assumption.
> 
> 
> Jacques can tell us about point 1.

This does not seem particularly difficult: we already extend the type environment
for GADTs, so it would only mean using private or "blind" types in place of
aliases.

> Regarding point 2., I'm not sure
> and have not thoroughly checked examples, but my intuition is that it
> is actually not a problem. I think that the types we naturally want to be
> covariant are also the types we want to manipulate as data (so it's ok
> if the type is larger than what we expect), rather than consumers, and
> conversely.
> 
> For example, the idiomatic use of the (+α expr) datatype is the
> (eval : ∀α. α expr → α) function, and it can be written on this
> monotonous version.
> 
> let rec eval : ∀α. α expr → α = function
>  | Val (v : α)                        → (v : α)
>  | Prod ∃βγ[α≥β*γ] (b:β, c:γ)        → ((b, c) : β*γ :> α)
>  | Priv [α ≥ priv_int] (n : priv_int) → (n : priv_int :> α)
> 
> One would need to study more examples to get a better understanding of
> this question.

There are certainly examples in both directions.
For instance the "print" example in the manual uses the opposite direction.
And in some cases you are going to want both simultaneously.
Moreover this is very heavy: all subtyping requires type annotations,
while type equalities are directly handled by unification.
This may look like you don't need that many here, but in general
we only currently require type annotations on ambiguous types
when they escape the current case. In some cases this is a tiny
fraction of the uses of equality.

On the other hand, if you really want variance, this looks like a cleaner solution.

> # Conclusion and questions
> 
> We have a relaxed criterion that we're confident is sound and can
> plausibly be implemented in OCaml (including possibly before the
> next release). But it relies on a closed-world assumption that is
> currently skewed towards covariance because of private types -- not
> a problem for our use case, the relaxed value restriction. Finally, it
> would suggest some language extensions to benefit fully from it, by
> enabling upward/downward closure specification for abstract types, and
> allowing to forbid making a new type `private` in the future
> (or blind) to gain stronger variance properties.
> 
> On the other hand, we know that this criterion would not hold as is in
> an open world scenario. Is this consideration relevant to the OCaml
> type system? If one wants to keep the door open to the open world
> case, would the suggested approach (reasoning under subtyping
> constraints in pattern clauses) be implementable?

For OCaml the problem is abstraction.
I think it has consequences very close to open world, except if you're
willing to add lots of information to interfaces.

> I don't believe the two choices are exclusive: if we have an
> annotation to say "this type will never be marked private", it becomes
> downward-closed even in an open-world scenario, and we can recover the
> current behavior by saying that all types, by default, "will never be
> marked blind" but "may be marked private". Those defaults are design
> areas to explore.
> 
> I would welcome feedback on the current state of affairs. Given what
> we know, is there a hope of relaxing the variance check for GADT at
> some short-to-medium-term point?

Well, your simplest criterion (just check that the instantiated parameter
is upward-closed, failing on "unknown" abstract types) seems easy enough to check.
The question is whether is it really sufficient in practice.
For all the other annotations, there would need to be a very strong justification.
Honestly, my feeling is just that GADTs do not play well with subtyping, and
there is no really satisfactory solution (except maybe subtyping constraints, but
they are going to be very heavy).

	Jacques Garrigue

[Caml-list] Re: Variance of GADT parameters

[Gabriel Scherer]

Dear list, I'm afraid my last e-mail was rejected because it was too
long. This is probably a good indication that it would be too long for
you as well, but for the record I have uploaded the email content and
the attached technical development:

  http://gallium.inria.fr/~scherer/variance_gadts/second_email.text
  http://gallium.inria.fr/~scherer/variance_gadts/interference_proof.text

> A stronger approach would be to check interfaces to ensure that abstraction
> cannot be broken.
> I was already thinking about that for making abstract types covariant when
> the module interface only allows covariant uses.
> But this can be very tricky.

If I understand correctly, you are suggesting allowing to annotate
abstract types at a module boundary with a variance that contradicts
the internal type implementation, as long as the operations proposed
in the interface respect this stronger variance.

For example, we could have covariant immutable arrays by just
restricting the existing invariant implementation and interface.

This is something interesting, but indeed it seems difficult and is,
I think, relatively orthogonal to the present discussion. It would be
a new way to enrich variance information (and possibly
upward/downward closure) at abstraction boundaries but, if I understand
correctly, it does not subsume the expressivity of variance
(or possibly upward/downward closure) information:

  type +α t
  val weird_id : α t → α → α

>> From a design point of view, the "right thing" would be to let people
>> publish this information in the signature for an opaque type. Just as
>> we can annotate the type with variance information, we should be able
>> to publish its upward/downward closure properties.
>
> This is rather heavy-weight...

Variance annotations on abstract types are already in the domain of
experts library writers, not simple users – most people have never
heard of them. I don't think the upward/downward closure criterion is
much harder to understand or would have much cognitive burden.

(There would be the same problem with current variant annotations,
that you may have to rely on third-party code defining abstract types
that haven't been richly annotated enough by ignorance. I don't think
this would make the problem worse.)

>> Another natural question is: what if we added the symmetric of the
>> "private" concept, a type (blind σ) strictly above σ for all types?
>> Would we lose all reasonable variance properties on OCaml types?
>
> Is there any use for these "blind" types ?

I don't know what those "blind" types could be useful for, and I'm
certainly not asking for them. Intuitively I'd say that there are
situations where one works in a negated world, where what was
naturally covariance becomes contravariant, and what should usually be
made private would now require such "blind" types. But as said with my
previous mail, favoring covariance does not seem to be problematic in
practice.

This is more of a design argument: we have added a construct but not
the symmetric one; what if we had done this, just for the sake of
regularity? If something changes from usable to unusable because of
this fairly gratuitous move, maybe there is a problem of design
fragility.

> What do you mean by "all reasonable variance properties" ?
> This should only have an impact on GADTs, isn'it ?

I mean that upward-closure is currently a fairly natural notion for
ordinary types (yes, if a tuple (x,y) can be given a type, then it
must be a cartesian product type), which would be broken by adding
those types. I informally and nearly unconsciously assumed it held
when reasoning about my (Prod : α expr * β expr → (α * β) expr)
constructor.

Yes, among the type-system features I know of, this would only impact
GADTs. More precisely, that would only impact GADTs whose constraint
are equality constraints. Still that is something to take into
account. I suppose you were not aware, at the time of introducing
private types, that this added feature could negatively impact other
areas of the type system; we now have the opportunity to ponder this
tension more carefully.

(I don't know which of GADTs or private types people would find more
useful; that surely depends on one's domain and programming
style. What would we do if we were given the opportunity to go back in
time and remove private types to strengthen equality GADTs?)

I believe saying "this new type will never be made private in the
future" is the good way to control this tension. I didn't like the
idea at first, but that's a way to have our two cakes (private types
and equality GADTs) and eat them both, without either one putrefying
the other.

Indeed this must be transmitted through abstraction boundaries, but
I don't think this "go against abstraction", or at least
encapsulation. Marking a new type as "non-privatizable" is not
revealing some of its internal aspects, but making a design choice for
its future use, just as OOP programmers often decide to mark their
classes "final" to get stronger reasoning principles on them.

Again, I don't say we should add this to the OCaml interface language
in a few days/months. I'm only trying to establish that making the
design choice of using the upward/downward closure criterion would not
close us doors in the future, that it is possible to control it finely
without giving away the designer's freedom to evolve the subtyping
lattice.
On a pragmatic level, I would be fine with keeping the current
situations where no type is "non-privatizable" but (indeed) all types
are "non-blindable" and not adding the ability to change this
locally. This means we can't have equality-constrained contravariant
GADT parameters, but the situation on covariant types, which is my
main point of interest, is quite reasonable.


> Contravariant parameters are not generalized because this would
> be unsound:

Oh, I was not aware of this. Thanks for the correction. If
I understand correctly, the reason is that values do not have an
uniform runtime representation.


> This does not seem particularly difficult: we already extend the type environment
> for GADTs, so it would only mean using private or "blind" types in place of
> aliases.

That is good news. I had not realized that, just as a local abstract
types serves as existential variables, a local private type is in some
way a "canonical" smaller type.


>> For example, the idiomatic use of the (+α expr) datatype is the
>> (eval : ∀α. α expr → α) function, and it can be written on this
>> monotonous version.
>
> There are certainly examples in both directions.
> For instance the "print" example in the manual uses the opposite direction.

There is a strong difference between the types "expr" and "ty"

  type α expr
    | Val : α → α expr
    | Prod : α expr * β expr -> (α * β) expr

  type α ty
    | Ty : α expr
    | Prod : α ty * β ty → (α * β) ty

`expr` carries data so is intuitively covariant. `ty` carries no data
so could be used in either directions. Note that the printing function
for `expr` does not require contravariance, as its type is
`α expr → string`.

So I believe that the `print : α ty → α → string` is an example of
GADT that should be invariant – rather than an example of GADT that we
want to make covariant but couldn't this an open-world presentation,
whatever that may mean.

> On the other hand, if you really want variance, this looks like a cleaner solution.

That's the idea. Having the option to use subtyping constraints rather
than equality constraints would allow a library designer to make
compromises. Invariance is easier to handle for everyone, but in case
covariance is really important it can be done – which is not currently
the case.

Note that the two ideas, one of using upward/downward closure to
strengthen variance properties in the equality case, the other of
using subtyping constraints to gain covariance at the cost of weaker
elimination, are not mutually exclusive.

You can even factor upward/downward considerations through the
subtyping constraint approach: instead of checking that equality is
sound at constructor definition site, you can check at each
elimination site that you can regain a full equality constraint from
the subtyping hypothesis through an upward/downward closure argument.

I think a reasonable design process for a library writer would be to
first go for the easy equality case and, if one discovers a need for
{co,contra}variance, wonder about upward/downward closure properties
and, if they don't hold, weaken the type to subtyping constraints in
the good direction. Each step is potentially more expressive, but also
more costly (in term of required annotations, etc.).

> Well, your simplest criterion (just check that the instantiated parameter
> is upward-closed, failing on "unknown" abstract types) seems easy enough to check.
> The question is whether is it really sufficient in practice.
> For all the other annotations, there would need to be a very strong justification.

I agree with your evaluation of the situation.

Thanks for answering so carefully.

On Fri, Apr 13, 2012 at 5:45 AM, Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
> Dear Gabriel,
>
> Thank you for this detailed analysis.
> It is comforting to know that the current criterion is sound!
>
> I have a few remarks/questions.
>
>> # A criterion in the general case
>>
>> I believe (and have a draft of proof in the attached technical annex)
>> that the requirement of Simonet&Pottier is equivalent, in the equality
>> case, to the following criterion that *could* be implemented in
>> a type-checker – more easily than by adding a general constraint
>> solver.
>>
>>  Given variance annotations (≤i) for the type ᾱ t, the type
>>  constructor
>>    K : ∀ᾱ∀β̄[α₁ = T₁(β̄), α₂ = T₂(β̄)...] τ̄ → ᾱ t
>>  or equivalently (in OCaml syntax)
>>    K : τ̄ → (T₁(β̄),T₂(β̄)...) t
>>  respects the variance if all the conditions below are met:
>>
>>  1. Non-interference: if an existential variable β appears in several
>>     Ti(β̄), then all its occurences in the whole type expression
>>     (T₁(β̄),T₂(β̄)...) t must be in invariant position.
>>
>>  2. Upward/downward closure, or eliminability: for each i, β̄, α', if
>>     (Ti(β̄) ≤i α') holds then α' is of the form Ti(β̄').
>>
>>  3. Constructor parameters variance: the variance of the β̄ in the
>>     type expression (T₁(β̄),T₂(β̄)...) t must respect their variance in
>>     the constructor parameters τ̄ – just like if we had a non-GADT
>>     declaration in term of the β̄, (type β̄ t = K of τ̄ | ...).
>>
>> I believe this is sound, not unreasonably difficult to check, and
>> would help in a lot of concrete cases that are currently rejected.
>
> Have you considered my comment on the interaction with abstraction:
>
>>> Again I wonder whether you are not going to get problems with abstraction.
>>> At first sight, no: if when you define a GADT t, the type u is abstract, then
>>> it will have no supertype in any environment where we use t.
>>> But if you think more carefully, you realize that if in the future we allow
>>> (gadt-)unification between abstract types, everything breaks, since abstract
>>> types may end up having supertypes in a local environment.
>>> So it looks like the only types you can allow for instantiation are concrete
>>> datatypes and well-known types (abstract types defined in the initial environment
>>> or in the current module).
>
> In the future, we really want to be able to instantiate normal abstract types with
> GADT pattern matching, not just local ones.
> Wouldn't it mean that you can never now whether an abstract type is upward closed?
>
> module M : sig type t type u = private int val eq : (t,u) eq end =
>  struct type u = int  type t = u  let eq : (t,u) eq = Eq end
>
> Note that this doesn't means that I could build a proof of unsoundness.
> You criterion may actually be too restrictive.
> Actually, my counter-example with a private type used a contravariant gadt.
>
>> # Discussion of private types and contravariance
>>
>> There is something quite disturbing in the idea that the mere
>> existence of private types creates a strong asymmetry between
>> covariant and contravariant parameters for GADTs: while upward-closed
>> types are relatively common (so that we can expect "the usual
>> examples" of GADTs to have "the expected variance"), there are no more
>> downward-closed types, which means no contravariant constrained
>> parameter.
>>
>> Upward or downward closure can be easily decided on fully transparent
>> types (types whose definition is known). But there is a problem with
>> opaque types: as we don't know how they were defined, we can't check
>> if they are upward/downward closed.
>
> Sorry about the above comment.
> This seems to be what you are referring to here.
> I would just remind you that we have lots of opaque types around,
> so that this may be a strong limitation in practice.
> Of course we can still apply the criterion that opaque types in
> the initial environment (builtin + pervasives) cannot be circumvented,
> but this a kind of hack.
>
> A stronger approach would be to check interfaces to ensure that abstraction
> cannot be broken.
> I was already thinking about that for making abstract types covariant when
> the module interface only allows covariant uses.
> But this can be very tricky.
>
>> From a design point of view, the "right thing" would be to let people
>> publish this information in the signature for an opaque type. Just as
>> we can annotate the type with variance information, we should be able
>> to publish its upward/downward closure properties.
>
> This is rather heavy-weight...
>
>> Another natural question is: what if we added the symmetric of the
>> "private" concept, a type (blind σ) strictly above σ for all types?
>> Would we lose all reasonable variance properties on OCaml types?
>
> Is there any use for these "blind" types ?
> What do you mean by "all reasonable variance properties" ?
> This should only have an impact on GADTs, isn'it ?
>
>> One idea from Didier Rémy is to allow, when defining a new type 't'
>> (not a type synonym), to define it as "non-privatizable"
>> (and correspondingly non-blindable). We or another programmer would
>> then not be allowed to define a type 'private t'. In exchange for this
>> lost flexibility, 't' would be downward-closed. The idea is that
>> introducing private types increased our freedom, and reciprocally
>> lessened our ability to reason about "what cannot be done";
>> non-privatizable annotations allow to locally make the inverse choice
>> of losing 'private' for better subtyping properties.
>
> This one would really go against abstraction...
>
>> From a pragmatic standpoint, I suspect the current restrictions
>> 'private' entails on the GADT variance checks are not going to be
>> really problematic in practice. We tend to use covariant types
>> (data) more often than contravariant types (computations). The OCaml
>> type system is already skewed towards covariance in one place: while
>> the relaxed value restriction (which, I recall, is the reason why
>> I needed GADT variance in the first place) would work equally well
>> to generalize variables that appear only in covariant or only in
>> contravariant positions, the relaxation is implemented in the
>> type-checker only for covariant parameters. And I have not yet heard
>> of someone requesting generalization of only-contravariant
>> parameters, so apparently treating contravariant parameters as
>> second-class citizens is ok among OCaml users.
>
> Contravariant parameters are not generalized because this would
> be unsound:
>
> let f : 'a -> unit = let r = ref [| |] in
>  fun x -> if !r = [| |] then r := [|x|] else (!r).(0) <- x
>
> let crash = f 1.0; f 1
>
> It is unsound to add a top type to the ocaml type hierarchy.
> But the "blind" types would of course be sound.
>
>> # A theoretical open-world approach
>>
>> Some people may consider the upward-downward criterion as
>> fundamentally unsatisfying because of the closed-world assumption it
>> makes: it is not preserved by enrichment of the OCaml subtyping
>> lattice.
>>
>> There is another possibility to get some variance properties out of
>> GADTs that still works in an open-world system: allow GADTs
>> constraints to have subtyping constraints, instead of only equality
>> constraint.
>>
>> For example we could define the type of well-typed expressions in
>> this way (note the ≥ in constraints):
>>  type +α expr =
>>    | Val : ∀α. α → α expr
>>    | Prod : ∀α∀βγ[α ≥ β*γ] β*γ → α expr
>>    | Priv : ∀α[α ≥ priv_int] priv_int → α expr
>>
>> It is trivial that this definition is covariant in its type parameter,
>> because covariance was baked in the definition. Indeed, if α≤α'
>> and α≥β*γ, then α'≥β*γ by transitivity: the constraint is preserved by
>> going to a larger type. In the soundness requirement of
>> Simonet&Pottier, one can use the exact same existential variables on
>> both sides (β̄':=β̄), and the constraints will be satisfied.
>>
>> The downside of this easier covariance property is that we get weaker
>> types on deconstruction (pattern matching of GADT values): when
>> matching on a (α t), in the Prod clause, we only know that (α ≥ β*γ)
>> rather than (α = β*γ) – note that we could regain the stronger
>> hypothesis by locally using the closed-world assumption.
>>
>> This simple idea has two potential problems:
>>
>> 1. This may not be implementable as part of the current OCaml
>>   type-checker, which uses type equalities internally and has more
>>   limited subtyping support (in particular we can't abstract over
>>   arbitrary subtyping assumptions). That said, this particular way of
>>   adding subtyping hypothesis in the context might be simple enough
>>   for it to handle.
>>
>> 2. Getting a weaker hypothesis may be unusable: maybe the usual GADT
>>   programs really make use of the equality assumptions, and going for
>>   subtyping assumptions would make untypable programs that would be
>>   perfectly fine under the closed-world assumption.
>>
>>
>> Jacques can tell us about point 1.
>
> This does not seem particularly difficult: we already extend the type environment
> for GADTs, so it would only mean using private or "blind" types in place of
> aliases.
>
>> Regarding point 2., I'm not sure
>> and have not thoroughly checked examples, but my intuition is that it
>> is actually not a problem. I think that the types we naturally want to be
>> covariant are also the types we want to manipulate as data (so it's ok
>> if the type is larger than what we expect), rather than consumers, and
>> conversely.
>>
>> For example, the idiomatic use of the (+α expr) datatype is the
>> (eval : ∀α. α expr → α) function, and it can be written on this
>> monotonous version.
>>
>> let rec eval : ∀α. α expr → α = function
>>  | Val (v : α)                        → (v : α)
>>  | Prod ∃βγ[α≥β*γ] (b:β, c:γ)        → ((b, c) : β*γ :> α)
>>  | Priv [α ≥ priv_int] (n : priv_int) → (n : priv_int :> α)
>>
>> One would need to study more examples to get a better understanding of
>> this question.
>
> There are certainly examples in both directions.
> For instance the "print" example in the manual uses the opposite direction.
> And in some cases you are going to want both simultaneously.
> Moreover this is very heavy: all subtyping requires type annotations,
> while type equalities are directly handled by unification.
> This may look like you don't need that many here, but in general
> we only currently require type annotations on ambiguous types
> when they escape the current case. In some cases this is a tiny
> fraction of the uses of equality.
>
> On the other hand, if you really want variance, this looks like a cleaner solution.
>
>> # Conclusion and questions
>>
>> We have a relaxed criterion that we're confident is sound and can
>> plausibly be implemented in OCaml (including possibly before the
>> next release). But it relies on a closed-world assumption that is
>> currently skewed towards covariance because of private types -- not
>> a problem for our use case, the relaxed value restriction. Finally, it
>> would suggest some language extensions to benefit fully from it, by
>> enabling upward/downward closure specification for abstract types, and
>> allowing to forbid making a new type `private` in the future
>> (or blind) to gain stronger variance properties.
>>
>> On the other hand, we know that this criterion would not hold as is in
>> an open world scenario. Is this consideration relevant to the OCaml
>> type system? If one wants to keep the door open to the open world
>> case, would the suggested approach (reasoning under subtyping
>> constraints in pattern clauses) be implementable?
>
> For OCaml the problem is abstraction.
> I think it has consequences very close to open world, except if you're
> willing to add lots of information to interfaces.
>
>> I don't believe the two choices are exclusive: if we have an
>> annotation to say "this type will never be marked private", it becomes
>> downward-closed even in an open-world scenario, and we can recover the
>> current behavior by saying that all types, by default, "will never be
>> marked blind" but "may be marked private". Those defaults are design
>> areas to explore.
>>
>> I would welcome feedback on the current state of affairs. Given what
>> we know, is there a hope of relaxing the variance check for GADT at
>> some short-to-medium-term point?
>
> Well, your simplest criterion (just check that the instantiated parameter
> is upward-closed, failing on "unknown" abstract types) seems easy enough to check.
> The question is whether is it really sufficient in practice.
> For all the other annotations, there would need to be a very strong justification.
> Honestly, my feeling is just that GADTs do not play well with subtyping, and
> there is no really satisfactory solution (except maybe subtyping constraints, but
> they are going to be very heavy).
>
>        Jacques Garrigue

[Caml-list] Re: Variance of GADT parameters

[Jacques Garrigue]

On 2012/04/13, at 19:51, Gabriel Scherer wrote:

>>> From a design point of view, the "right thing" would be to let people
>>> publish this information in the signature for an opaque type. Just as
>>> we can annotate the type with variance information, we should be able
>>> to publish its upward/downward closure properties.
>> 
>> This is rather heavy-weight...
> 
> Variance annotations on abstract types are already in the domain of
> experts library writers, not simple users – most people have never
> heard of them. I don't think the upward/downward closure criterion is
> much harder to understand or would have much cognitive burden.

Maybe they have never heard of them, but I believe variance annotations are really intuitive.
However, understanding upward/downward closure is another story.
Actually, this property itself seems in contradiction with subtyping:
it says that a type is outside of the subtyping hierarchy.
I understand that this may make some things easier (in relation with
subtyping), but I'm afraid you will end-up wanting it both inside and outside...

Moreover, if we add "blind" types, which would be needed for subtyping
constraints in GADTs, don't you end-up losing both closure properties
on all types?

>> What do you mean by "all reasonable variance properties" ?
>> This should only have an impact on GADTs, isn'it ?
> 
> I mean that upward-closure is currently a fairly natural notion for
> ordinary types (yes, if a tuple (x,y) can be given a type, then it
> must be a cartesian product type), which would be broken by adding
> those types. I informally and nearly unconsciously assumed it held
> when reasoning about my (Prod : α expr * β expr → (α * β) expr)
> constructor.
> 
> Yes, among the type-system features I know of, this would only impact
> GADTs. More precisely, that would only impact GADTs whose constraint
> are equality constraints. Still that is something to take into
> account. I suppose you were not aware, at the time of introducing
> private types, that this added feature could negatively impact other
> areas of the type system; we now have the opportunity to ponder this
> tension more carefully.
> 
> (I don't know which of GADTs or private types people would find more
> useful; that surely depends on one's domain and programming
> style. What would we do if we were given the opportunity to go back in
> time and remove private types to strengthen equality GADTs?)
> 
> I believe saying "this new type will never be made private in the
> future" is the good way to control this tension. I didn't like the
> idea at first, but that's a way to have our two cakes (private types
> and equality GADTs) and eat them both, without either one putrefying
> the other.

Let us not mix things up.
The tension is not between GADTs and private types, but between one
way to add variance annotations to GADTs and private types.
Since variance annotations are originally for subtyping, it is actually
a tension between two extensions to subtyping.
And I don't think that restricting subtyping is a good way to strengthen it :-)
So my intuition is that relying on upward/downward closure is fundamentally
wrong, because it restricts the subtyping relation you are allowed to use.

>> This does not seem particularly difficult: we already extend the type environment
>> for GADTs, so it would only mean using private or "blind" types in place of
>> aliases.
> 
> That is good news. I had not realized that, just as a local abstract
> types serves as existential variables, a local private type is in some
> way a "canonical" smaller type.

I forgot to mention that if we want both covariant and contravariant annotations,
we also need "blind" types...

>>> For example, the idiomatic use of the (+α expr) datatype is the
>>> (eval : ∀α. α expr → α) function, and it can be written on this
>>> monotonous version.
>> 
>> There are certainly examples in both directions.
>> For instance the "print" example in the manual uses the opposite direction.
> 
> There is a strong difference between the types "expr" and "ty"
> 
>  type α expr
>    | Val : α → α expr
>    | Prod : α expr * β expr -> (α * β) expr
> 
>  type α ty
>    | Ty : α expr
>    | Prod : α ty * β ty → (α * β) ty
> 
> `expr` carries data so is intuitively covariant. `ty` carries no data
> so could be used in either directions. Note that the printing function
> for `expr` does not require contravariance, as its type is
> `α expr → string`.
> 
> So I believe that the `print : α ty → α → string` is an example of
> GADT that should be invariant – rather than an example of GADT that we
> want to make covariant but couldn't this an open-world presentation,
> whatever that may mean.

OK, I understand better.
This seems to make sense.
Of course in many situations one would want equation constraints rather
than subtyping constraints, but this is really a choice about the semantics
of your type.

>> On the other hand, if you really want variance, this looks like a cleaner solution.
> 
> That's the idea. Having the option to use subtyping constraints rather
> than equality constraints would allow a library designer to make
> compromises. Invariance is easier to handle for everyone, but in case
> covariance is really important it can be done – which is not currently
> the case.
> 
> Note that the two ideas, one of using upward/downward closure to
> strengthen variance properties in the equality case, the other of
> using subtyping constraints to gain covariance at the cost of weaker
> elimination, are not mutually exclusive.

As I mentioned above, we would need "blind" types, which breaks upward closure.
Or is there a way out?

> I think a reasonable design process for a library writer would be to
> first go for the easy equality case and, if one discovers a need for
> {co,contra}variance, wonder about upward/downward closure properties
> and, if they don't hold, weaken the type to subtyping constraints in
> the good direction. Each step is potentially more expressive, but also
> more costly (in term of required annotations, etc.).

Actually, if variance is only obtained through subtyping constraints,
variance annotations could exactly mean that. I.e., you would just write

 type +_ expr =
   | Val : α → α expr
   | Prod : β*γ → β*γ expr
   | Priv : priv_int → priv_int expr

and it would automatically generate subtyping constraints for the relevant  cases.
(I.e. only the Prod and Priv cases)

I agree that code using this would still require much more type annotations.
If there are many applications for this, maybe we could infer simple cases of subtyping
(at least not to have to write the same annotation in each branch of the pattern matching)

Jacques Garrigue