Disjoint constraints for type parameters

[arseniiv]

I propose adding a new constraint T1, T2, …, Tn disjoint for signifying type parameters T1, T2, …, Tn are provably disjoint at compile-time with exactly the same algorithm as used for switch cases.

It should enable us to write e. g.

function sumMap<Value1, Value2, Return1, Return2>(Value1|Value2 val, Return1(Value1) f1, Return2(Value2) f2)
    given Value1, Value2 disjoint =>
  switch (val)
  case (is Value1) f1(val)
  case (is Value2) f2(val);

or maybe more useful

Return|Error map…<Value, Error, Return>(Value|Error val, Return(Value) f)
    given Value, Error disjoint =>
  switch (val)
  case (is Value) f(val)
  case (is Error) val;

without disabling any warnings.

Maybe examples aren’t comprehensive enough, but it occurred to me this could be a nice feature and maybe even not hard to implement.

[gavinking]

This is an interesting idea that we should certainly explore further. My immediate reactions:

1. In terms of the typing algorithms, it should indeed be easy enough to incorporate this kind of constraint into disjointness analysis.
2. On the other hand, I'm not certain what the impact on type argument inference would be. AFAIR we don't currently look at disjointness at all when doing type inference. But probably for this to be useful that would need changing. Needs to be thought through.
3. I don't like the proposed syntax much but I don't have a better idea.
4. I doubt that this would have much impact on the backends. Looks like a pure typechecker-level feature if I'm not mistaken.

[gavinking]

One option might be something like given Value satisfies ~Error. I'm not sure if the asymmetry of that is useful or harmful. The asymmetry might make it easier to make use of the constraint in type argument inference.

[gavinking]

i.e.

Return|Error map<Value, Error, Return>
   (Value|Error val, Return(Value) fun)
        given Value satisfies ~Error 
        => switch (val)
        case (is Value) fun(val)
        case (is Error) val;

[gavinking]

But type inference is definitely a real problem here. To see why, try out this code in current Ceylon:

Return|Error map<Value, Error, Return>
        (Value|Error val, Return(Value) fun)
        => switch (val)
        case (is Value) fun(val)
        else case (is Error) val;

String|Exception maybeString = "";
Integer int = map(maybeString, (String x)=>x.size);

Ceylon does an atrocious job of inferring Value and Error here. And that's because we just don't have any useful constraints. I can do slightly better if I mess with the variance of the type parameters, and possibly I could do even better again by taking into account a type constraint of the proposed form. But it's still going to be extremely fragile, it seems to me.

[arseniiv]

@gavinking

I don't like the proposed syntax much but I don't have a better idea.

I too. (Can’t say anything about satisfies ~T.)

[ePaul]

What about given T1 & T2 is Nothing?

Actually, we could also write it the other way around, and reuse the existing syntax: given Nothing satisfies T1 & T2.

This would allow for a future generalization like given String satisfies T1 & T2.

[RossTate]

Return|Error map<Value, Error, Return>
        (Value|Error val, Return(Value) fun)
        => switch (val)
        case (is Value) fun(val)
        else case (is Error) val;

String|Exception maybeString = "";
Integer int = map(maybeString, (String x)=>x.size);

Inference isn't the problem here. This code is ambiguous: given different inferred types for Value and Error it will produce different results. And requiring Value and Error to be disjoint doesn't solve the problem.

• Value inferred to be Nothing and Error inferred to be be String|Exception results in val always being returned.
• Value inferred to be String and Error inferred to be Exception results in what you were expecting.

Now suppose you had a generic method whose type arguments are inferable. Then further requiring type parameters to be disjoint won't affect inferability so long as you're only requiring covariant type parameters to be disjoint.

[phlopsi]

I like the given A satisfies ~B syntax the most, currrently. Slightly different syntax that comes to my mind would be either (1) given A satisfies -B or (2) given A satisfies !B, which could both possibly represent not/inverse of, as well.

Implementing this feature should make #4517 potentially easily solveable, by introducing Absent to several interfaces and disallowing Element/Type (or whatever) to satisfy Absent for several interfaces, e.g. Correspondence.