User loginNavigation |
Type Theoretical Foundations for Data Structures, Classes, and ObjectsVia 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.and 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? :). By Andris Birkmanis at 2004-08-13 10:11 | LtU Forum | previous forum topic | next forum topic | other blogs | 7606 reads
|
Browse archives
Active forum topics |
Recent comments
1 week 3 days ago
41 weeks 5 days ago
41 weeks 5 days ago
41 weeks 5 days ago
1 year 11 weeks ago
1 year 16 weeks ago
1 year 17 weeks ago
1 year 17 weeks ago
1 year 20 weeks ago
1 year 24 weeks ago