That's a good example, albeit quite of a far-fetched one.
In Haskell land, where the type system is considered sound you have `head` functions of type `List a -> a` that are unsound too, because the list might be empty.
In Haskell land, where the type system is considered sound you have `head` functions of type `List a -> a` that are unsound too, because the list might be empty.
However this problem as stated is slightly different and has to do with a failure of OOP/subtyping to actually intermingle with our expectations of covariance.
So to just use classic "animal metaphor" OOP, if you have an Animal class with Dog and Cat subclasses, and you create an IORef<Cat>, a cell that can contain a cat, you would like to provide that to an IORef<Animal> function because you want to think of the type as covariant: Cat is a subtype of Animal, F<Cat> should be a subtype of F<Animal>. The problem is that this function now has the blessing of the type system to store a Dog in the cell, which can be observed by the parts that still consider this an IORef<Cat>.
Put slightly differently, in OOP, the methods of IORef<Cat> all accept an implicit IORef<Cat> called `this`, if those methods are part of what define an IORef<x> then an IORef<x> is necessarily invariant, not covariant, in <x>. And then you can't assume subtyping. So to be sound a subtype system would presumably have to actually mark contra/covariance around everything, and TypeScript very intentionally documents that they don't do this and are just trying to make a "best effort" pass because JavaScript has 0 types, and crappy types are better than no types, and we can't wait for perfect types to replace the crappy types.
Haskell's `head` not is not an example of the type system being unsound (I stress this point because we've been talking about type system soundness, not something-else-soundness).
From the view of the type system, `head` is perfectly sound: if the list is empty, the resulting value is ⊥ ("bottom"). And ⊥ is an inhabitant of every type. Therefore, `head` returning ⊥ when given an empty list is perfectly fine. When you force ⊥ (i.e. use it any way whatsoever), an exception is thrown. See https://wiki.haskell.org/Bottom
This is very much not the same thing (or remotely analogous) to what we have in my TypeScript example. There, the code fails at runtime when I attempt to call `toLowerCase`, yes; what's worse is the slightly different scenario where we succeed in calling something we shouldn't:
class Person {
name: string;
constructor(name: string) {
this.name = name;
}
kill() {
console.log("Killing: " + this.name);
}
}
class Murderer extends Person { }
class Innocent extends Person { }
function populatePeopleFromDatabase(people: Array<Innocent | Murderer>): void {
// imagine this came from a real SQL query
people.push(new Innocent("Bob"));
}
function populateMurderersFromDatabase(people: Array<Murderer>): void {
// TODO(Aleck): come back and replace this with a query that only selects murderers.
// i wanted to get the rest of the code in place, and this type checks,
// so I'll punt on this for now and come back later when I wrap my head
// around the proper SQL.
// we're not actually using this anywhere just yet, so no biggie ¯\_(ツ)_/¯
populatePeopleFromDatabase(people);
}
// ... some time later, Bob comes along and implements the murderer execution logic:
const murderers: Array<Murderer> = [];
populateMurderersFromDatabase(murderers);
// Bob is about to have a really shitty day:
murderer.forEach((murderer) => murderer.kill());