Type inference, principal typings, and let-polymorphism for first-class mixin modules

module is a programming abstraction that simultaneously generalizes -abstractions, records, and mutually recursive definitions. Although various mixin module type systems have been developed, no one has investigated principal typings or developed type inference for first-class mixin modules, nor has anyone added Milner's let-polymorphism to such a system. This paper proves that typability is NP-complete for the naive approach followed by previous mixin module type systems. Because a -calculus extended with record concatenation is a simple restriction of our mixin module calculus, we also prove the folk belief that typability is NP-complete for the naive early type systems for record concatenation. To allow feasible type inference, we present Martini, a new system of simple types for mixin modules with principal typings. Martini is conceptually simple, with no subtyping and a clean and balanced separation between unification-based type inference with type and row variables and con...

• Type: Conference
• Year: 2005
• Where: ICFP
• Authors: Henning Makholm, J. B. Wells
• Keywords: First-class Mixin Modules, ICFP 2005, Mixin Module Calculus, Mixin Module Type, Programming Languages