I think it's useful mostly as a sort of Linnæan classification device—it's a lot easier to compare different type systems by placing them on a 'standard' cube, than by choosing ad hoc points of comparison.
Type theories are formal logic languages. People use formal logic for all sorts of things but mathematics has the longest history. This is where people first defined formal languages and assigned meaning (mathematical meaning.)
Starting from simply typed lambda calculus ("simple type theory", also "higher order logic"), one can make various extensions that make the logic language more expressive. The lambda cube is a way to systematically organize the space of type theories.
Interestingly, the theory has become very relevant for type systems of normal programming languages. Milner invented ML as "meta language" for helping with logic and theorem proving, but it was used widely and today everyone expects generics to work more or less as in System F polymorphic lambda calculus.
This is why people think these concepts aren’t useful, because this was a lot of words without any practical example of what it would be used for.
Here’s a practical example: there are type systems in the lambda cube that allow us to statically check that a list has a certain length. That means a compiler can prevent an out of bounds access error, without human intervention. I have written code that crashes because of an out of bounds access, so the idea is interesting to me.
JadeNB|4 years ago
viewfromafar|4 years ago
Starting from simply typed lambda calculus ("simple type theory", also "higher order logic"), one can make various extensions that make the logic language more expressive. The lambda cube is a way to systematically organize the space of type theories.
Interestingly, the theory has become very relevant for type systems of normal programming languages. Milner invented ML as "meta language" for helping with logic and theorem proving, but it was used widely and today everyone expects generics to work more or less as in System F polymorphic lambda calculus.
amw-zero|4 years ago
This answer was:
‘Assigning mathematical meaning.’
This is why people think these concepts aren’t useful, because this was a lot of words without any practical example of what it would be used for.
Here’s a practical example: there are type systems in the lambda cube that allow us to statically check that a list has a certain length. That means a compiler can prevent an out of bounds access error, without human intervention. I have written code that crashes because of an out of bounds access, so the idea is interesting to me.