[amw-zero]

The question was ‘why is the lambda cube useful?’

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.

[guerrilla]

> This answer was:

> ‘Assigning mathematical meaning.’

No, you misread. The answer was

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

[acchow]

You're mostly describing why dependent types are useful (in preventing an entire class of errors).

The lambda cube is useful in comparing and reasoning about the features of type systems across languages.