Lambda the Ultimate

Abstract: The expression families problem can be defined as the problem of achieving reusability and composability across the components involved in a family of related datatypes and corresponding operations over those datatypes. Like with the traditional expression problem, adding new components (either variants or operations) should be possible while preserving modular and static type-safety. Moreover, different combinations of components should have different type identities and the subtyping relationships between the different combinations should be preserved. By generalizing previous work that explored the connection between type-theoretic encodings of datatypes and visitors, we propose two solutions for this problem in Scala using modular visitor components. These components can be grouped into features that can be easily composed in a feature-oriented programming style to obtain customized datatypes and operations.

This is a draft paper on a topic that I think is of the interest of the readers of this forum. It motivates a variation of the expression problem and proposes two solutions in Scala inspired by type-theoretic encodings of datatypes.

In the lambda cube, the three axes are terms-depending-on-types, types-depending-on-types and types-depending-on-types. To check my intuition:

Isn't sub-typing, in the manner of Java, C++ and C#, an example of plain terms-depending-on-types?

Are prototype-based languages, such as Javascript, plain terms-depending-on-terms?

Are multi-parameter typeclasses, C++ templates and "generics" examples of types-depending-on-types? Are associated types (for example, the iterator for a certain collection) "higher-order" or are they essentially the same thing?