It should be noted that soundness is not a common feature for type systems in the wild. It sounds kind of scary, "X programming language's type system is unsound", but that's pretty much been the status quo for most of programming.

Our intuition about inheritance is pretty much all wrong.

I make analogies to taxonomy because before I learned software a biology teacher told me that taxonomy is also broken, so when I learned type theory it felt like a similar kind of broken.

We think putting wings to a mammal is adding behavior, when in fact it is subtracting it. Adding wings on a mammal means you have a bat, or a flying squirrel.

You have narrowed the potential of this type, not enhanced it. Anything else a mammal might do that bats can't? You've taken all of that away. Mammals with fly() aren't the fastest land animals. They don't have the record for holding their breath, or hibernation time. They can't dive(), speak() or useTool(). Really they're kinda useless except for vermin control.

This is probably why it's important to not anthropomorphize your code. Code abstractions do pretty much one thing: they prevent the duplication of code. They each do this in their own ways that make certain deduplications easier than others. If you focus on that, the broken analogy of taxonomy doesn't matter, and you can easily hop between the religious war camps of "OOP vs FP" and "Inheritance vs Composition". Figure out what you want your ergonomics to be and just go with that.

This is a correct observation, and also something to always remember. There are dark corners where unsound type systems fail, they inevitably exist in most practical languages, so you can wander into one in daily practice.

I was about to say this. Most type systems in practical use are not mathematically sound.

Is there a way to understand this tradeoff in a principled way?

Wouldn't that be a problem in most languages? Even Haskell allows for it through Data.Dynamic

If I can serialize to String, and then deserialize a String to any type of class, I can effectively "cast" anything to anything.

The point is not that you can do explicit casts, it's that because you can form a (fake) instance for impossible types you can do invalid type conversions without doing anything that looks unsafe.

In Haskell you can certainly achieve the same thing with various common extensions ( http://okmij.org/ftp/Haskell/impredicativity-bites.html ). Possibly not in vanilla Haskell '98, at the price of being not a very nice language to work in. (A total language like Idris should permit GADT-like functionality without allowing this kind of issue).

The actual correspondence in haskell are GADTs:

    data EqualityProof a b where
        Refl :: (a ~ b) => EqualityProof a b

    -- compiler error because we don't check that the equality proof is actually Refl
    coerce :: EqualityProof a b -> a -> b
    coerce _ a = a

    -- this works
    coerce Refl a = a

    -- here the Refl pattern match catches the undefined
    -- this is like forcing the programmer to do a null check before the equality is in scope
    -- and throwing a runtime exception when it's null
    coerce undefinded 3 :: String

By “convert” here I mean convince the compiler that any thing of type A is any type B, when it definitely isn't, without using an explicit cast.

Data.Dynamic is type safe. It performs a run-time type check.

Haskell can be made to be unsound using 'unsafeCoerce', but as you'll note, there is a giant unsafe in front of it.

Haskell is unsound because of 'undefined :: a'. There you go - a proof of every proposition by the Curry-Howard isomorphism.

It's still safe, though, as it diverges at run time. Much like the ClassCastException coming from the JVM prevents the unsoundness in the original article from being a safety error.

'unsafeCoerce' (and things that can implement it, like creating a polymorphic mutable cell with 'unsafePerformIO') are worse than unsound - they are also unsafe.

Read about Bottom (⊥).

null can be considered bottom (if it were not for primitives)