Typing Classes and Mixins with Intersection Types
Jan Bessai (Technical University of Dortmund), Boris D\"udder, (Technical University of Dortmund), Andrej Dudenhefner (Technical University, of Dortmund), Tzu-Chun Chen (Technical University of Darmstadt), Ugo, de'Liguoro (University of Torino)

TL;DR
This paper develops an intersection type system for lambda-calculus with records and merge operators, enabling natural typing of mixins and classes without recursive types, and adapts these concepts to Java and C#.
Contribution
It introduces a novel intersection type system that handles mixins and classes with recursive records without recursive or F-bounded types, and demonstrates adaptation to mainstream languages.
Findings
Types are preserved under subject reduction and expansion.
Mixins and classes can be meaningfully typed without recursive types.
Code snippets in Java and C# are shown to be typable within the system.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
