Many people are riled up that Dart’s type system proudly features covariant generics and so “is unsound”. The basic problem with covariant generics is that it lets you take a bowl of apples and call it a bowl of fruit. That’s fine if you’re just going to eat from the bowl and you like all fruits, but what if you decide to contribute a banana to the fruit bowl? Someone taking from the bowl expecting an apple might choke. And someone else could call the same bowl a bowl of things then put a pencil in it, just to spite you.

… because they are unsound?

We all seem to agree that it’s bad for an apple eater to choke on a banana or a fruit eater to choke on a pencil. (Wittgenstein and Turing similarly agreed that it’s bad for a bridge to fall and kill people.) For example, Java seems to agree: it detects at run time when such choking is about to occur and throws an exception instead, so no immediate harm is done. There is less agreement as to whether a static type system must prevent such choking before run time. One argument for early prevention is that it’s the whole point of having a static type system—why even bother with a static type system if it’s unsound?

But plenty of static type systems are unsound yet respectable. For example, many dependent type systems are unsound, either because their term languages are blatantly non-terminating or because they include the Type:Type rule. (I faintly recall that Conor McBride calls Type:Type “radical impredicativity”.) So it doesn’t seem that unsoundness per se should rile people up about Dart in particular.

Perhaps it’s time to distinguish different sorts of unsoundness: a type system can be unsound because it fails normalization or because it fails subject reduction. In the former case, a program (or the type checker) might promise an apple but never produce one; in the latter case, the program might promise an apple then produce a banana. The unsoundness of a dependent type system tends to be of the former sort, whereas the unsoundness of covariant generics seems to be of the latter sort. And the former sort of unsoundness seems more benign than the latter sort (and more deserving of the term “radical impredicativity”). So, by calling for subject reduction but not normalization, it seems we can drive a wedge between the acceptable unsoundness of many dependent type systems and the unacceptable unsoundness of Dart.

But it is very easy to turn a failure of subject reduction detected at run time into a failure of normalization: just go into an infinite loop whenever choking is about to occur! In Java, we can write catch (Exception e) { for (;;) {} }. (In math, we can restore subject reduction by letting an uncaught exception take any type, as is standard.) Is that really better? Does this move really answer the critics? I don’t feel so. For one thing, this move makes it harder, not easier, to write better programs: I want my program to stop and tell me when it’s choking.

Just as it’s only useful for type systems to allow a program if it’s something good that a programmer might write, it’s only useful for type systems to disallow a program if it’s something bad that a programmer might write. In other words, both incompleteness and unsoundness “may appear to be a steep price to pay” yet “work well in practice”. Does Type:Type abet many bad programs that people produce? Perhaps not. Do covariant generics abet many bad programs that people produce? Perhaps not. Are untyped bowls and naive set theory terribly dangerous? Perhaps not. (Proof rules and programming facilities that are unsound may even encourage useful abstraction and reduce the proliferation of bugs by copy-and-paste.)

… because they are meaningless?

To summarize so far, I don’t think we should dislike covariant generics for its unsoundness in general or for its failure of subject reduction in particular. Why do covariant generics bother me, then? I think it’s because they dash my hope for types to have crisp meanings.

When I write down an expression, whether it’s a term or a type, I want it to refer to something else, whether in my mind or in the world. When I write that a certain term has a certain type (say, alice:person or 2+3:nat), I want to write about some entity, to mean that it has some property. That is not subject reduction, but to have a subject and a predicate in the first place, which is prior to subject reduction. I would be dissatisfied if there is no subject and predicate to be found outside the syntax and operational semantics of a formal language. After all, my desire to assert that 2+3:nat is not fueled by any interest in the curly symbols 2 and 3 or the binary node label +. In short, I want to denote.

Of course, it’s not entirely a formal language’s fault if I can’t use it to denote, if it’s hard to program in. Syntax only goes so far, and cognition must carry the rest of the way. But it does get easier to denote and program if how expressions combine inside the language matches how their referents tend to interact outside the language. For example, FORTRAN made it easier to denote numbers than in assembly language: having written 2+3 to denote a number, and knowing that numbers have absolute values, I can write abs(2+3) to denote the absolute value of the number denoted by 2+3. Numbers are outside FORTRAN, yet FORTRAN matches my knowledge that numbers have absolute values. In contrast, if you can hardly put a banana in a bowl of apples in reality but you can easily put(banana, bowl:Bowl<Apple>) in formality, or vice versa, then I have trouble seeing what banana and bowl mean.

This match I want is a kind of modular reasoning. Now, the word “modular” has been used to mean many things, but what I mean here is this. To combine two objects inside a language, I might need to worry about whether their types match, whether they live on the same machine, whether they use the same calling convention, etc. To combine two objects outside a language, I might need to worry about how big they are, whose kitchen it is, and whether fruit flies would come. Ideally, my worries inside the language should match my worries outside the language. Ideally, a combination should make sense inside a language just in case the referents of the combined expressions are compatible outside the language. If the language implementation could keep track of my worries and discharge them as early as possible for me, then so much the better, but that’s secondary and orthogonal—I’d be plenty happy if I can just talk about worrisome things without also worrying about the language at the same time.

I feel it’s hopeless to match a language with covariant generics against things we want to talk about. Why? I don’t have proof. For all I can show, the worries of a Dart programmer inside and outside the language will match perfectly, just as Java exceptions precisely simulate the material effects of putting a pencil in a bowl of apples. In the end, my feeling boils down to the unreasonable and unusual effectiveness of mathematics and logic.

Not only might this effectiveness be fallible, but it’s also possible that my hopelessness is misplaced. I said I want expressions to match their referents more closely so that denoting and programming becomes easier. But maybe the match we have today is the best we can do because the world has too many shades of gray to be modeled in the black-and-white terms provided by mathematics and logic. Maybe the world simply refuses to provide crisp referents for any expression to mean. Maybe, when lexical references slip and uncaught exceptions fire, it’s just collateral damage from the fact that life is messy. After all, it is one thing for a bridge engineer to leave gravity unquantified because calculus is hard; it is another thing for a bridge architect to leave beauty unquantified because psychology is hard. To avoid variance rules just because they ”fly in the face of programmer intuition” feels like the former to me, but what do I know?

… because they are not even unsound?

Well, I do my best. I do my best to understand whether and how reference and truth can help programming. I do my best to enlist syntax and pragmatics. I’m not yet ready to give up just because so many people are confused by noun-noun compounds in English (what’s an “apple bowl”?) and by variance rules in Java today. To me, the notion of being sound or unsound only makes sense if expressions have meanings outside the language. I do my best so that Bowl<Apple> means something, so that when I claim ”it is easy for tools to provide a sound type analysis if they choose” I know what I mean by “sound”. To not even worry about what expressions mean is not even unsound.

(Rob Simmons beat me to a blog post. He makes good, related points.)