Typing Classes and Mixins with Intersection Types
We study an assignment system of intersection types for a lambda-calculus with records and a record-merge operator, where types are preserved both under subject reduction and expansion. The calculus is expressive enough to naturally represent mixins as functions over recursively defined classes, who...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2015-03-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1503.04911v1 |
| _version_ | 1811261652636532736 |
|---|---|
| author | Jan Bessai Boris Düdder Andrej Dudenhefner Tzu-Chun Chen Ugo de'Liguoro |
| author_facet | Jan Bessai Boris Düdder Andrej Dudenhefner Tzu-Chun Chen Ugo de'Liguoro |
| author_sort | Jan Bessai |
| collection | DOAJ |
| description | We study an assignment system of intersection types for a lambda-calculus with records and a record-merge operator, where types are preserved both under subject reduction and expansion. The calculus is expressive enough to naturally represent mixins as functions over recursively defined classes, whose fixed points, the objects, are recursive records. In spite of the double recursion that is involved in their definition, classes and mixins can be meaningfully typed without resorting to neither recursive nor F-bounded polymorphic types.
We then adapt mixin construct and composition to Java and C#, relying solely on existing features in such a way that the resulting code remains typable in the respective type systems. We exhibit some example code, and study its typings in the intersection type system via interpretation into the lambda-calculus with records we have proposed. |
| first_indexed | 2024-04-12T19:09:30Z |
| format | Article |
| id | doaj.art-dcfc56705adf4c97b44b686c6221480d |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-12T19:09:30Z |
| publishDate | 2015-03-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-dcfc56705adf4c97b44b686c6221480d2022-12-22T03:19:56ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802015-03-01177Proc. ITRS 2014799310.4204/EPTCS.177.7:8Typing Classes and Mixins with Intersection TypesJan Bessai0Boris Düdder1Andrej Dudenhefner2Tzu-Chun Chen3Ugo de'Liguoro4 Technical University of Dortmund Technical University of Dortmund Technical University of Dortmund Technical University of Darmstadt University of Torino We study an assignment system of intersection types for a lambda-calculus with records and a record-merge operator, where types are preserved both under subject reduction and expansion. The calculus is expressive enough to naturally represent mixins as functions over recursively defined classes, whose fixed points, the objects, are recursive records. In spite of the double recursion that is involved in their definition, classes and mixins can be meaningfully typed without resorting to neither recursive nor F-bounded polymorphic types. We then adapt mixin construct and composition to Java and C#, relying solely on existing features in such a way that the resulting code remains typable in the respective type systems. We exhibit some example code, and study its typings in the intersection type system via interpretation into the lambda-calculus with records we have proposed.http://arxiv.org/pdf/1503.04911v1 |
| spellingShingle | Jan Bessai Boris Düdder Andrej Dudenhefner Tzu-Chun Chen Ugo de'Liguoro Typing Classes and Mixins with Intersection Types Electronic Proceedings in Theoretical Computer Science |
| title | Typing Classes and Mixins with Intersection Types |
| title_full | Typing Classes and Mixins with Intersection Types |
| title_fullStr | Typing Classes and Mixins with Intersection Types |
| title_full_unstemmed | Typing Classes and Mixins with Intersection Types |
| title_short | Typing Classes and Mixins with Intersection Types |
| title_sort | typing classes and mixins with intersection types |
| url | http://arxiv.org/pdf/1503.04911v1 |
| work_keys_str_mv | AT janbessai typingclassesandmixinswithintersectiontypes AT borisdudder typingclassesandmixinswithintersectiontypes AT andrejdudenhefner typingclassesandmixinswithintersectiontypes AT tzuchunchen typingclassesandmixinswithintersectiontypes AT ugodeliguoro typingclassesandmixinswithintersectiontypes |