3 ms·

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 unsoun

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.

kochthesecond 8y ago
I was about to say this. Most type systems in practical use are not mathematically sound.
- ionforce 8y ago
  Is there a way to understand this tradeoff in a principled way?
nine_k 8y ago
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.
hinkley 8y ago
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.
- moron4hire 8y ago
  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.

kochthesecond 8y ago

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

ionforce 8y ago
Is there a way to understand this tradeoff in a principled way?

nine_k 8y ago

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.

hinkley 8y ago

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.

moron4hire 8y ago
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.