Henning Makholm
Abstract
A mixin 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 constraint solving for safety of linking and field extraction. We have implemented a type inference algorithm and we prove its complexity to be O(n2), or O(n) given a fixed bound on the number of field labels. To prove the complexity, we need to present an algorithm for row unification that may have been implemented by others, but which we could not find written down anywhere. Because Martini has principal typings, we successfully extend it with Milner's let-polymorphism.
- D. Ancona, S. Fagorzi, E. Moggi, E. Zucca. Mixin modules and computational effects. In Proc. 30th Int'l Coll. Automata, Languages, and Programming, vol. 2719 of LNCS. Springer-Verlag, 2003.]]Google Scholar
- D. Ancona, S. Fagorzi, E. Zucca. A calculus with lazy module operators. In IFIP TC1 3rd Int'l Conf. Theoret. Comput. Sci. (TCS '04). Kluwer Academic Publishers, 2004.]]Google Scholar
- D. Ancona, E. Zucca. A primitive calculus for module systems. In Proc. Int'l Conf. Principles & Practice Declarative Programming, vol. 1702 of LNCS. Springer-Verlag, 1999.]] Google ScholarDigital Library
- D. Ancona, E. Zucca. A calculus of module systems. J. Funct. Programming, 12(2), 2002. Extended version of {3}.]] Google ScholarDigital Library
- D. Duggan, C. Sourelis. Mixin modules. In Proc. 1996 Int'l Conf. Functional Programming. ACM Press, 1996.]] Google ScholarDigital Library
- Programming Languages & Systems, 9th European Symp. Programming, vol. 1782 of LNCS. Springer-Verlag, 2000.]]Google Scholar
- M. Flatt, M. Felleisen. Units: Cool modules for HOT languages. In Proc. ACM SIGPLAN '98 Conf. Prog. Lang. Design & Impl., 1998.]] Google ScholarDigital Library
- R. Harper, B. C. Pierce. A record calculus based on symmetric concatenation. Technical Report CMU-CS-90-157R, Carnegie Mellon Univ., 1991.]]Google ScholarDigital Library
- R. Harper, B. C. Pierce. A record calculus based on symmetric concatenation. In Conf. Rec. 18th Ann. ACM Symp. Princ. of Prog. Langs., 1991.]] Google ScholarDigital Library
- T. Hirschowitz. Mixin Modules, Modules, and Extended Recursion in a Call-by-Value Setting. PhD thesis, Université Paris 7, 2003.]]Google Scholar
- T. Hirschowitz. Rigid mixin modules. In Seventh International Symposium on Functional and Logic Programming (FLOPS 2004), 2004.]]Google ScholarCross Ref
- T. Hirschowitz, X. Leroy. Mixin modules in a call-by-value setting. In Programming Languages & Systems, 11th European Symp. Programming, vol. 2305 of LNCS. Springer-Verlag, 2002.]] Google ScholarDigital Library
- T. Hirschowitz, X. Leroy, J. B. Wells. Call-by-value mixin modules: Reduction semantics, side effects, types. In Programming Languages & Systems, 13th European Symp. Programming, vol. 2986 of LNCS. Springer-Verlag, 2004. More details can be found in {10}.]]Google Scholar
- H. Makholm, J. B. Wells. Type inference, principal typings, and letpolymorphism for first-class mixin modules. Technical report, Heriot-Watt Univ., School of Math. & Comput. Sci., 2005.]]Google Scholar
- A. Ohori, P. Buneman. Type inference in a database programming language. In Proc. 1988 ACM Conf. LISP Funct. Program., Snowbird, Utah, U.S.A., 1988.]] Google ScholarDigital Library
- J. Palsberg, T. Zhao. Type inference for record concatenation and subtyping. Inform. & Comput., 189, 2004.]] Google ScholarDigital Library
- F. Pottier. A 3-part type inference engine. In ESOP '00 {6}.]] Google ScholarDigital Library
- F. Pottier. A versatile constraint-based type inference system. Nordic Journal of Computing, 7(4), 2000.]] Google ScholarDigital Library
- F. Pottier. A constraint-based presentation and generalization of rows. In Proc. 18th Ann. IEEE Symp. Logic in Comput. Sci., 2003.]] Google ScholarDigital Library
- F. Pottier, D. Rémy. The essence of ML type inference. In B. C. Pierce, ed., Advanced Topics in Types and Programming Languages, chapter 10. MIT Press, Cambridge, Massachusetts, 2005.]]Google Scholar
- D. Rémy. Typing record concatenation for free. In Conf. Rec. 19th Ann. ACM Symp. Princ. of Prog. Langs., 1992. A later version is {22}.]] Google ScholarDigital Library
- D. Rémy. Typing record concatenation for free. In C. A. Gunter, J. C. Mitchell, eds., Theoretical Aspects Of Object-Oriented Programming: Types, Semantics and Language Design. MIT Press, 1993.]] Google ScholarDigital Library
- D. Rémy. A case study of typechecking with constrained types: Typing record concatenation. Presented at the workshop on Advances in Types for Computer Science at the Newton Institute, Cambridge, UK, 1995.]]Google Scholar
- R. E. Tarjan. Efficiency of a good but not linear set union algorithm. J. ACM, 22(2), 1975.]] Google ScholarDigital Library
- S. Vansummeren. On the complexity of deciding typability in the relational algebra. Acta Informatica, 200X. To appear.]] Google ScholarDigital Library
- M. Wand. Complete type inference for simple objects. In Proc. 2nd Ann. Symp. Logic in Comput. Sci., 1987. A corrigendum appeared at LICS 1988.]]Google Scholar
- M. Wand. Type inference for record concatenation and multiple inheritance. In Proc. 4th Ann. Symp. Logic in Comput. Sci., Pacific Grove, CA, U.S.A., 1989. IEEE Comput. Soc. Press.]] Google ScholarDigital Library
- M. Wand. Type inference for record concatenation and multiple inheritance. Inform. & Comput., 93, 1991.]] Google ScholarDigital Library
- J. B. Wells. The essence of principal typings. In Proc. 29th Int'l Coll. Automata, Languages, and Programming, vol. 2380 of LNCS. Springer-Verlag, 2002.]] Google ScholarDigital Library
- J. B.Wells, R. Vestergaard. Confluent equational reasoning for linking with first-class primitive modules (long version). A short version is {31}. Full paper, 3 appendices of proofs, 1999.]]Google Scholar
- J. B. Wells, R. Vestergaard. Equational reasoning for linking with first-class primitive modules. In ESOP '00 {6}. A long version is {30}.]] Google ScholarDigital Library
- J. Zwanenburg. A type system for record concatenation and subtyping. In K. Bruce, G. Longo, eds., Third Workshop on Foundations of Object Oriented Languages (FOOL 3), Rutgers Univ., NJ, USA, 1996.]]Google Scholar
Index Terms
- Type inference, principal typings, and let-polymorphism for first-class mixin modules
Recommendations
Type inference, principal typings, and let-polymorphism for first-class mixin modules
ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingA mixin 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 ...
Mixin’ Up the ML Module System
ML modules provide hierarchical namespace management, as well as fine-grained control over the propagation of type information, but they do not allow modules to be broken up into mutually recursive, separately compilable components. Mixin modules ...
Comments