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

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

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