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?