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.
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.