2015/03/14 by Jan Bessai, Boris Düdder, Andrej Dudenhefner +4
Computer Science · Mathematics · #Bounded function #Computer science #Data type #Dependent type #Double recursion #Formal Methods in Verification #Intersection (aeronautics) #Lambda calculus #Logic, programming, and type systems #Mathematics #Merge (version control) #Programming language #Recursion (computer science) #Simply typed lambda calculus #Software Engineering Research #Theoretical computer science #Type (biology) #Typed lambda calculus #cs.LO #cs.PL #cs.SE
paper · pdf · doi:10.4204/eptcs.177.7
published as EPTCS 177, 2015, pp. 79-93 · In Proceedings ITRS 2014, arXiv:1503.04377
openalex publication_date 2015/03/14 · arxiv created 2015/03/17 · arxiv updated 2015/03/18 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
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.