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.
> The lambda cube is a way to systematically organize the space of type theories.
All of this was already meaningful before the lambda cube. The cube just organizes what we knew in a systematic way. It shows the relationships between the various systems that exist when they are differentiated on the features that describe their expressive power.
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.