Covariance and contravariance in generic types

[asterite]

(spawned from #1294)

Motivating example:

class Base
end

class Child < Base
end

def enumerable_base(x : Enumerable(Base))
end

def array_base(x : Array(Base))
end

base_ary = Array(Base).new
child_ary = Array(Child).new

# Which of the following methods should give an error?
enumerable_base(base_ary)
array_base(base_ary)
enumerable_base(child_ary)
array_base(child_ary)

The questions are:

#1.
Array(Base).new.is_a?(Enumerable(Base))
Array(Base).new.is_a?(Array(Base))         

There are true, not a lot to discuss here.

#2.
Array(Child).new.is_a?(Enumerable(Base))

This is a bit more difficult to answer. The thing is, you read from an enumerable, you don't put things inside it. So this question should be true, because Child.new.is_a?(Base).

#3.
Array(Child).new.is_a?(Array(Base))

Now, Child.new.is_a?(Base), but if the above is true, say we replace Array(Child).new with exp, we get:

exp.is_a?(Array(Base)) #=> true

Good, it's an Array(Base) so lets put some elements into it:

exp << Base.new # ERROR

Oops, but exp was Array(Child), we can't put a Base inside it. So maybe the answer to is_a? should be false here.

So, we have two cases of Child vs. Base in generic types, and in one case we'd like the answer to be true and in another one we'd like it to be false.

The "solution" is to mark the T in Enumerable as covariant. In C# they do it like IEnumerable<out T>. There's also in. I think in Scala they use + and -. And, as far as I know, these are difficult to grasp. So, we'll go from an untyped language (Ruby) to a language with some type annotations (generic types, captured blocks), to a language with covariance/contravariance type annotations. I'm not sure I like that idea, but we'll see.

The way it works right now is that Array(Child).is_a?(Array(Base)) will give false, but the call array_base(child_ary) succeeds. And, as long as you only read from the array, everything will compile fine. So, in a way, this is safe, but maybe not very intuitive.

We should decide what to do with this.

[bcardiff]

So, its a good thing to allow more programs to succeed the type checker if they would be able to run without type restrictions. That's the half of the whole point. (The other half is not make the type system catch all program that would fail in runtime)

With this in mind, allowing Enumerable(T) <: Enumerable(S) when T <: S is a good thing. Specifying per generic param if its <, = or > regarding subtyping rules is an easy way to express them.

But, as we discussed IRL. This will affect the method lookup / is_a? results.

Crystal, due to how class/methods/macros are expanded does not follow some rules as other languages.
That is, type restriction plays in choosing the method but does not restrict which methods can be called. Sounds tricky.

Compare:
http://play.crystal-lang.org/#/r/cyq
http://play.crystal-lang.org/#/r/cyr

So, allowing covariance/contravariance, at least in the first stage, might be "only" about method type restriction. I'm a bit uncertain about the following steps.

[mverzilli]

Wouldn't something like protocols be an alternative solution?

1. If your use case doesn't require thinking about variance/covariance, you just keep using your generics as they are today.
2. If you need to mix different (but related) things inside a generic without resorting to unions (which as far as I understand is the motivation behind exploring this feature), you define a protocol and use that to type the generic. Crystal would be able to check that a given type conforms to a protocol, so as long as you only push instances of types that conform you'd be safe.

[whorbowicz]

I worked mostly with Java and Scala so I am used to using types and relying on them. I can understand that when you come from dynamic languages the approach can be different. (That's why type inference is a great thing) For me, however, having types and inheritance implies that you can rely on them.

Java handled variance in generics by making them invariant.
In Scala as @asterite mentioned there are + and - for denoting covariance and contravariance of type parameter. Invariance is default.
From what I've seen so far in Crystal (and I don't know the whole language yet) type arguments of generics are covariant.
One of more interesting cases where this is not good are functions:

Say you have a function that takes as an argument function from type A to type B
def foo(funct: A -> B)
From signature it's pretty clear that what you expect inside foo is

• pass any value that is_a?(A) and
• receive value that is_a?(B).

More interesting is the question: what I can pass to foo as funct? or more precisely:
what is_a?(A->B)?
If in A -> B A and B are invariant - it's A ->B only. This is quite restrictive.
If we want to use variance then the it would be good if we could pass any A* -> B* where A < A* (contravariant A) and B* < B (covariant B). Then requirements from foo are still satisfied as

• for every input is_a?(A) => is_a?(A*) - passed function will be able to handle it
• for every output is_a?(B*) => is_a?(B) - returned value is of expected type.

Currently in Crystal it's not possible and due to covariance on input you can actually pass A*-> B where A* < A and fail compilation on missing method if someone passes value of type A.
I wonder if it will fail if foo would be in a library.
http://play.crystal-lang.org/#/r/d0z
Actually it gets even crazier as Child->Child fails is_a?(Parent->Parent) test but you can still pass it to foo(Parent->Parent). Is this another bug?

So my point is that Crystal already has covariance and this does not work in every case as a person with typed language background would expect it to. So I would suggest approach similar to Scala if it's possible.

[stugol]

+1 for + and - annotations

[bcardiff]

I was thinkg of using < and > for annotations.

So

class Foo(A<)
end

corresponds to covariance

        A < B
---------------------
   Foo(A) < Foo(B)

And

class Foo(A>)
end

corresponds to contravariance

        A > B                              B < A
---------------------       =      ---------------------
   Foo(A) < Foo(B)                    Foo(A) < Foo(B)

I think +/- is better than in/out thou. But I find >/< more straight forward to the semantics.

[stugol]

Sure, that works too.

[js-ojus]

I support @asterite! There is little point in Crystal becoming a "Scala with Ruby syntax" ;-).

Somehow, most programmers think about only reading, when they think of covariance. And then get tripped by it in endless ways. In my limited experience, variance is one of the darkest corners of type systems.

If you haven't already seen them, I highly recommend that you watch:

1. Paul Phillips' 2014 talk at LinkedIn (on Scala's collections; he talks a good deal about variance), and
2. Andrei Alexandrescu's talk at DConf 2015 (about what he called "Design by Introspection").

I request you all to consider a combination of:

• type bounds on generic parameters,
• separating modules from the class hierarchy (lateral look-up path vs. vertical look-up path), and
• normal boolean logic on the above at the time of generic type specification.

Such a combination can address a vast majority of scenarios, without introducing covariance and contravariance.

Remember that a departure from invariance is a one way ticket. It taints the language and a lot of the standard library irrevocably!

---

Edit: Correct Phillips' spelling.

[whorbowicz]

@js-ojus As I already pointed out Crystal is not invariant ATM.
As for Paul Phillips' talk - I would recommend checking every point he makes if it's really valid. There are things worth taking into consideration while in other places he is just incorrect eg. trying to prove that map on Set works incorrectly by using functions with side effects in his example.

[js-ojus]

@whorbowicz Yes, I realise that Crystal currently has some covariance. The question that I was trying to surface was: should Crystal embrace invariance or continue down the path to full covariance/contravariance?

We have to remember that covariance is unsound, unless everything is contravariant on the input side and covariant on the output side. Else, we leak, and become unsound. This is one of the biggest reasons why delegates in C# are contravariant in their input types.

And, we only need a glance at StackOverflow to see thousands of C# programmers who got tripped by the above.

Also, there is nothing wrong with invariance and existential types. It has been proved formally to be sound (e.g. Igarashi and Viroli). Torgersen, Ernst and Hansen's paper "Wild FJ" is a good read, as well.

On the second point, I did not mean to imply that everything that Paul Phillips said was correct :-). Nonetheless, I am curious about what you say. Could you point to the specific example of map over a set that you think was incorrect? Thanks.

---

Edit: Formatting.

[whorbowicz]

@js-ojus I'll give you the details, but let's move this subject to some private channel (eg. G+) - we are drifting away from the topic. :)

[ozra]

For notation the <, > makes sense. However, @js-ojus makes some good points. Generics type bounds and 'concept'-like features could be more helpful practically.

[asterite]

Closed in favor of #2665