Lambda the Ultimate

Via MetaPRL

Type Theoretical Foundations for Data Structures, Classes, and Objects

We will show that records and objects can be defined in a powerful enough type theory. We will also show how to use these type constructors to define abstract data structure.

Here we extend the constructive type theory with a simpler type constructor dependent intersection, i.e., the intersection of two types, where the second type may depend on elements of the first one (not to be confused with the intersection of a family of types). This new type constructor allows us to define dependent records in a very simple way.

Dependent intersection looks worth attention for many reasons, e.g. providing a simpler alternative to very dependent functions. I especially liked how it simplifies treatment of coincident labels (multiple inheritance, anyone? :).