ABSTRACT
ML is two languages in one: there is the core, with types and expressions, and there are modules, with signatures, structures and functors. Modules form a separate, higher-order functional language on top of the core. There are both practical and technical reasons for this stratification; yet, it creates substantial duplication in syntax and semantics, and it reduces expressiveness. For example, selecting a module cannot be made a dynamic decision. Language extensions allowing modules to be packaged up as first-class values have been proposed and implemented in different variations. However, they remedy expressiveness only to some extent, are syntactically cumbersome, and do not alleviate redundancy. We propose a redesign of ML in which modules are truly first-class values, and core and module layer are unified into one language. In this "1ML", functions, functors, and even type constructors are one and the same construct; likewise, no distinction is made between structures, records, or tuples. Or viewed the other way round, everything is just ("a mode of use of") modules. Yet, 1ML does not require dependent types, and its type structure is expressible in terms of plain System Fω, in a minor variation of our F-ing modules approach. We introduce both an explicitly typed version of 1ML, and an extension with Damas/Milner-style implicit quantification. Type inference for this language is not complete, but, we argue, not substantially worse than for Standard ML. An alternative view is that 1ML is a user-friendly surface syntax for System Fω that allows combining term and type abstraction in a more compositional manner than the bare calculus.
- H. Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, vol. 2, chapter 2, pages 117–309. Oxford University Press, 1992. Google ScholarDigital Library
- S. K. Biswas. Higher-order functors with transparent signatures. In POPL, 1995. Google ScholarDigital Library
- L. Damas and R. Milner. Principal type-schemes for functional programs. In POPL, 1982. Google ScholarDigital Library
- D. Dreyer. Understanding and Evolving the ML Module System. PhD thesis, CMU, 2005. Google ScholarDigital Library
- D. Dreyer and M. Blume. Principal type schemes for modular programs. In ESOP, 2007. Google ScholarDigital Library
- D. Dreyer, K. Crary, and R. Harper. A type system for higher-order modules. In POPL, 2003. Google ScholarDigital Library
- J. Garrigue and A. Frisch. First-class modules and composable signatures in Objective Caml 3.12. In ML, 2010.Google Scholar
- J. Garrigue and D. Rémy. Semi-explicit first-class polymorphism for ML. Information and Computation, 155(1-2), 1999. Google ScholarDigital Library
- R. Harper and M. Lillibridge. A type-theoretic approach to higherorder modules with sharing. In POPL, 1994. Google ScholarDigital Library
- R. Harper and J. C. Mitchell. On the type structure of Standard ML. In ACM TOPLAS, volume 15(2), 1993. Google ScholarDigital Library
- R. Harper, J. C. Mitchell, and E. Moggi. Higher-order modules and the phase distinction. In POPL, 1990. Google ScholarDigital Library
- R. Harper and B. Pierce. Design considerations for ML-style module systems. In B. C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 8, pages 293–346. MIT Press, 2005.Google Scholar
- R. Harper and C. Stone. A type-theoretic interpretation of Standard ML. In Proof, Language, and Interaction: Essays in Honor of Robin Milner. MIT Press, 2000. Google ScholarDigital Library
- D. Le Botlan and D. Rémy. MLF: Raising ML to the power of System F. In ICFP, 2003. Google ScholarDigital Library
- X. Leroy. Applicative functors and fully transparent higher-order modules. In POPL, 1995. Google ScholarDigital Library
- M. Lillibridge. Translucent Sums: A Foundation for Higher-Order Module Systems. PhD thesis, CMU, 1997.Google Scholar
- D. MacQueen. Using dependent types to express modular structure. In POPL, 1986. Google ScholarDigital Library
- R. Milner. A theory of type polymorphism in programming languages. JCSS, 17:348–375, 1978.Google ScholarCross Ref
- R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997. Google ScholarDigital Library
- J. C. Mitchell and G. D. Plotkin. Abstract types have existential type. ACM TOPLAS, 10(3):470–502, July 1988. Google ScholarDigital Library
- D. Rémy. Records and variants as a natural extension of ML. In POPL, 1989.Google Scholar
- A. Rossberg. The Missing Link – Dynamic components for ML. In ICFP, 2006. Google ScholarDigital Library
- A. Rossberg. 1ML – Core and modules united (Technical Appendix), 2015. mpi-sws.org/˜rossberg/1ml/.Google Scholar
- A. Rossberg and D. Dreyer. Mixin’ up the ML module system. ACM TOPLAS, 35(1), 2013. Google ScholarDigital Library
- A. Rossberg, C. Russo, and D. Dreyer. F-ing modules. JFP, 24(5):529–607, 2014.Google Scholar
- C. Russo. Non-dependent types for Standard ML modules. In PPDP, 1999. Google ScholarDigital Library
- C. Russo. First-class structures for Standard ML. Nordic Journal of Computing, 7(4):348–374, 2000. Google ScholarDigital Library
- C. Russo. Types for Modules. ENTCS, 60, 2003.Google Scholar
- C. Russo and D. Vytiniotis. QML: Explicit first-class polymorphism for ML. In ML, 2009. Google ScholarDigital Library
- Z. Shao. Transparent modules with fully syntactic signatures. In ICFP, 1999. Google ScholarDigital Library
- C. A. Stone and R. Harper. Extensional equivalence and singleton types. ACM TOCL, 7(4):676–722, 2006. Google ScholarDigital Library
- J.-P. Talpin and P. Jouvelot. Polymorphic type, region and effect inference. JFP, 2(3):245271, 1992.Google Scholar
- D. Vytiniotis, S. Weirich, and S. Peyton Jones. FPH: First-class polymorphism for Haskell. In ICFP, 2008. Google ScholarDigital Library
- P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad hoc. In POPL, 1989. Google ScholarDigital Library
- A. Wright. Simple imperative polymorphism. LASC,8:343–356, 1995. Google ScholarDigital Library
Index Terms
- 1ML – core and modules united (F-ing first-class modules)
Recommendations
1ML – core and modules united (F-ing first-class modules)
ICFP '15ML is two languages in one: there is the core, with types and expressions, and there are modules, with signatures, structures and functors. Modules form a separate, higher-order functional language on top of the core. There are both practical and ...
F-ing modules
TLDI '10: Proceedings of the 5th ACM SIGPLAN workshop on Types in language design and implementationML modules are a powerful language mechanism for decomposing programs into reusable components. Unfortunately, they also have a reputation for being "complex" and requiring fancy type theory that is mostly opaque to non-experts. While this reputation is ...
Type inference, principal typings, and let-polymorphism for first-class mixin modules
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 ...
Comments