While the definitions of covariance and contravariance in the article are correct, they are irrelevant to Dart. The heart of the author's mistake is here:

"A compile-time check has been moved to runtime, which means you don't know if your code is safe without running it."

In an optionally-typed language like Dart, this is always true. Dart doesn't require enough type information to allow the compiler to guarantee that code that passes the type checker won't throw a runtime exception. So whether a feature undermines type soundness is irrelevant. The important question is how big is the class of errors it fails to catch at compile-time versus what other benefits does it have.

"Unfortunately, I cannot shed any light on why Dart has covariant arrays"

Because covariant arrays are more consistent with programmer intent and in an optionally typed language don't appreciably undermine compile-time guarantees more than the "correct" rule. Good code avoids mutating arrays. Hence a rule that is correct for the common case of reading arrays makes sense. Moreover, such a rule keeps you from having to lie:

Given: Basket<Tomatos> HarvestTomatos()

MakeJuice(Basket<Fruit>)

MakeJuice(HarvestTomatos()) should Just Work (TM). The optional typing keeps me from accidentally passing MakeJuice a Basket<Insects> which is, as a dynamic language programmer, all I really want from the type system.

The solution to this problem is not to make arrays covariant, but to correctly specify the type signature of MakeJuice:

MakeJuice :: Basket<`a> -> void where `a <: Fruit

That is, of course, only if MakeJuice does not modify the array. In general, I think that often the biggest mistake is variance annotation of types. Instead, functions should have (in)variance annotation on every parameter and on the return value. Then, a function that only reads from an array would be covariant in the type of array elements, a function that only writes would be contravariant, and a function that does both would be invariant. No need to artificially limit the usecases of arrays.

I mean it really depends on what you conceive Basket<Fruit> as meaning in Dart. Essentially, Dart treats it as Basket<T> :: T <: Fruit. If you see it this way, then the obvious question is, how do you write a type declaration for T :: T <: Basket<Fruit>? The answer is: who wants to do that in a optionally typed language?

Generic container types should really have two parameters: one type that you're guaranteed to be able to put in, and one that you're guaranteed to get when you take it out. Then a Container<emits:A,accepts:B> is-a Container<emits:C,accepts:D> if A<C and B>D.

So, e.g., HarvestTomatoes() can return a Basket<Tomato>, which is shorthand for Basket<emits:Tomato,accepts:Tomato>, and MakeJuice can take a Basket<emits:Fruit,accepts:EMPTY_TYPE>, and it's safe to feed the former into something that wants the latter.

(Of course actual container objects will typically be of type Container<emits:T,accepts:T> for some specific T.)

In short, the problem with covariant generics is that you can put a Banana in a Basket<Apple> (because a Basket<Apple> IS A Basket<Fruit>).

So, are there any languages that actually get this right? I'm sure Haskell does, being a strongly-typed, side-effect-free language. Are there any other languages that have this working properly?

Haskell doesn't have any subtyping, so the problem doesn't come up.

For languages that implement generics in a way that takes variance into account, you can look at e.g. Java (ignore the array class, but look at Vector<E>) or Scala. OCaml also has subtyping (for records and variants) and variance-annotated type variables (http://ocaml.janestreet.com/?q=node/99).

> Haskell doesn't have any subtyping

Num looks like something that's been subtyped.

Well, it may look like but it isn't.

Num is a typeclass, not a type. Like yummyfajitas said, typeclasses are similar to interfaces or abstract classes in Java, but they aren't the same.

Consider Java's equals(). You can write 'a'.equals(foo) as long as foo is an Object.

In contrast, look at Haskell's (==) function declared in Eq (I'm not giving an example using Num because Haskell provides some implicit conversions for numeric literals, which would introduce an unrelated complication in the example).

    (==) :: (Eq a) => a -> a -> Bool

This functions accepts 2 arguments of any one type, as long that type is an instance of Eq. But we cannot use different types in the same call. That is, we can write ('a' == 'b') and ("foo" == "bar") but not ('a' = "foo"), because (==) is not defined for a Char and a String.

Java does; List<String> is not a subtype of List<Object>. This greatly confuses many programmers, since String[] is a subtype of Object[] (they made this mistake before Guy Steele got involved).

Naturally, SML does as well. SML also has immutable lists, which are covariant.

Haskell doesn't really have subtypes. Polymorphism in Haskell is typically implemented using typeclasses, which are closer to Java Interfaces than to subclasses.

I believe that C# 4 gives you the ability to specify the co- or contra variance of a generic type.

As does Java, but they get it wrong for arrays. I don't know if C# has that problem or not.

C# copied Java's mistake in this respect.

You can pass an Apple[] to something accepting a Fruit[] and get a runtime exception when you try to add a Banana to the Fruit[].

I agree that mutable-array covariance in a statically typed language is a Bad Idea (TM). But Dart's type checks at compile-time are so non-existent that array covariance is the least of my concerns. Take is simple example (you can run it on Dart's site [1]):

    applyShippingCost(num price) {
      return price + 10;
    }

    main() {
      print(applyShippingCost(100)); // Prints 110. Ok.
      var lol = "TROLOLO";
      num thisIsNotANum = applyShippingCost(lol); // Nothing explodes here...
      print(thisIsNotANum); // Prints TROLOLO10, Yeahh B)
    }

This runs well and compiles with no warnings. Types are not checked when assigning an untyped variable to a typed one, so while one would expect that type declarations should give us some form of type safety, they don't.

As I see it, with Dart's optionally typed system you get the worst part of two worlds (if you opt to type your variables): having to declare the types of variables, as in a static type system (with no compiler type inference); and having no guarantee about those type declarations at runtime, as in a duck-typing type system.

[1]: http://www.dartlang.org/

This is a function of pre-alpha tooling that doesn't do any type analysis. It would be trivial for the compiler to give you a warning in this circumstance with the type information you provided (and production compilers like SBCL will do so).

That is ultimately the point of optional typing. To let you gradually firm up the types in your program as the design gels. The technology is there to get quite a lot of mileage out of the resulting type information, though I think it would definitely behoove Google to make sure the tooling works well from 1.0.

E.g: https://gist.github.com/1325465

In the declaim I've specified the type of fib to be integer => integer. In the test function, I define a local function that calls a library function to concatenate two constants. The test function then calls fib with the result of calling the local function.

Compiling this, SBCL complains: https://gist.github.com/1325469

Here, the compiler starts with the known types of "hello" and " world", realizes that the result of CONCATENATE must be an array or null (strings are arrays in Common Lisp), realize that the function FUN always returns a sequence, and then realize that this result conflicts with the asserted type of FIB.

Indeed, if you define FIB inside TEST[1] you don't even need to declare the type of FIB, SBCL figures it out itself.

[1] This restriction is a limitation of the semantics of Common Lisp. Global definitions could be redefined, so SBCL will not flow types through them. Lexical definitions cannot be redefined, so SBCL will analyze them. Dart does not have this limitation.