Typechecker coverance difficulty with generics

[Dirk Lattermann]

On the first view, this seems like the typechecker could be able to
handle. Is it again a decidability problem?

Please consider this and see the comments in the test() method:

```ceylon
abstract class Node() {}
abstract class ParentNode<Child>() extends Node() satisfies List<Child>
given Child satisfies Node {
shared void add(Child child){}

// just to make compile
shared actual Child getFromFirst(Integer index) => nothing;
shared actual Integer lastIndex => nothing;
shared actual Boolean equals(Object other) => (this of
List<>).equals(other); shared actual Integer hash => (this of
List<>).hash; }

class NodeP1() extends ParentNode<NodeP2|NodeC1>(){}
class NodeP2() extends ParentNode<NodeP2|NodeC1|NodeC2>(){}
class NodeC1() extends Node(){}
class NodeC2() extends Node(){}

void test() {
// parent is set to NodeP1 just for illustration.
NodeP1|NodeP2 parent = NodeP1();
NodeC1 nodeC1 = NodeC1();

// following line gives compiler error
// (where does "out" come from?)

// Argument must be assignable to parameter child of add in
// ParentNode<out NodeP2|NodeC1|NodeC2>: NodeC1 is not
// assignable to Nothing
parent.add(nodeC1);

// the following works, but is it really the way to go?
// this seems ridiculous
if (is NodeP1 parent) {
parent.add(nodeC1);
}
else {
parent.add(nodeC1);
}
}
```

Additionally, instead of the 2nd line above, I'd like to write

```ceylon
abstract class ParentNode<Child>() of NodeP1 | NodeP2
satisfies List<Child>
```

but the compiler complains with

Case type must be a subtype of enumerated type for every type argument
of the generic enumerated type: NodeP1 is not assignable to
ParentNode<Child>

What's the rationale of this?

Thank you,
Dirk

[Gavin King]

On Sun, Jul 31, 2016 at 11:58 AM, Dirk Lattermann <dl...@alqualonde.de> wrote:


> // parent is set to NodeP1 just for illustration.
> NodeP1|NodeP2 parent = NodeP1();
> NodeC1 nodeC1 = NodeC1();
>
> // following line gives compiler error
> // (where does "out" come from?)
>
> // Argument must be assignable to parameter child of add in
> // ParentNode<out NodeP2|NodeC1|NodeC2>: NodeC1 is not
> // assignable to Nothing
> parent.add(nodeC1);

So what is going on here is that in order to assign a signature to
add(), the typechecker needs to form a principal instantiation of the
type ParentNode that declares add().

Unfortunately, ParentNode is invariant in its type parameter, which
makes this a tricky case. In theory, the correct result should be this
type, with a double-bounded wildcard:

ParentNode<out NodeP2|NodeC1|NodeC2 in NodeP2|NodeC1>

However, Ceylon doesn't (currently) support double-bounded wildcards
and so what it currently does in this case (i.e. where the upper bound
and lower bound are different) is it throws away the lower bound,
privileging covariance over contravariance, and assigns the type:

ParentNode<out NodeP2|NodeC1|NodeC2>

This is the type you'll see in the IDE if you hover over the call to add().

Of course, you can fix the problem easily by declaring add() on a
contravariant supertype, like this:


abstract class Node() {}
interface Parent<in Child> {
shared void add(Child child){}

}
abstract class ParentNode<Child>()
extends Node()

satisfies List<Child>&Parent<Child>
given Child satisfies Node { ... }

Which is the exact reason we have interfaces like ListMutator in the
collections hierarchy.

> Additionally, instead of the 2nd line above, I'd like to write
>
> ```ceylon
> abstract class ParentNode<Child>() of NodeP1 | NodeP2
> satisfies List<Child>
> ```
>
> but the compiler complains with
>
> Case type must be a subtype of enumerated type for every type argument
> of the generic enumerated type: NodeP1 is not assignable to
> ParentNode<Child>
>
> What's the rationale of this?

What you've defined here is not a plain sum type, but a "generalized"
algebraic type (GADT). GADTs exhibit decidability problem and for that
reason Ceylon doesn't (yet) support them.


--
Gavin King
ga...@ceylon-lang.org
http://profiles.google.com/gavin.king
http://ceylon-lang.org
http://hibernate.org
http://seamframework.org

[Dirk Lattermann]

Am Sun, 31 Jul 2016 16:06:59 +0200
schrieb Gavin King <gavin...@gmail.com>:

Ah, very interesting, thank you! That explains a lot.

>
> Of course, you can fix the problem easily by declaring add() on a
> contravariant supertype

Hehe, of course! ;-)
This sure takes some time to get used to. I was suspecting something in
this direction when I first spottet ListMutator, but didn't understand
fully. Doubt if I do know, but it's a lot clearer. Thanks!

>
>
> abstract class Node() {}
> interface Parent<in Child> {
> shared void add(Child child){}
> }
> abstract class ParentNode<Child>()
> extends Node()
> satisfies List<Child>&Parent<Child>
> given Child satisfies Node { ... }
>

.. and then use (parent of Parent<NodeP1|NodeC1>).add(nodeC1), right?

or rather, when using aliases

alias ChildrenP1 => NodeP2|NodeC1|NodeC2;
alias ChildrenP2 => NodeP2|NodeC1;

(parent of Parent<ChildrenP1&ChildrenP2>).add(nodeC1).

Are there performance differences writing the intersection like that
into the code or calculating it manually and writing the first version
above?

Thanks again.

> Which is the exact reason we have interfaces like ListMutator in the
> collections hierarchy.
>
>
>
> > Additionally, instead of the 2nd line above, I'd like to write
> >
> > ```ceylon
> > abstract class ParentNode<Child>() of NodeP1 | NodeP2
> > satisfies List<Child>
> > ```
> >
> > but the compiler complains with
> >
> > Case type must be a subtype of enumerated type for every type
> > argument of the generic enumerated type: NodeP1 is not assignable to
> > ParentNode<Child>
> >
> > What's the rationale of this?
>
> What you've defined here is not a plain sum type, but a "generalized"
> algebraic type (GADT). GADTs exhibit decidability problem and for that
> reason Ceylon doesn't (yet) support them.

I fear it takes more for me to understand, but never mind, I accept
that for now.

Dirk

[Gavin King]

On Wed, Aug 3, 2016 at 9:22 PM, Dirk Lattermann <dl...@alqualonde.de> wrote:

> .. and then use (parent of Parent<NodeP1|NodeC1>).add(nodeC1), right?
>
> or rather, when using aliases
>
> alias ChildrenP1 => NodeP2|NodeC1|NodeC2;
> alias ChildrenP2 => NodeP2|NodeC1;
>
> (parent of Parent<ChildrenP1&ChildrenP2>).add(nodeC1).

No, I don't see why you should need the use of "of". I didn't need to use it.