The ML module system stands as a high-water mark of programming language support for data abstraction. Nevertheless, it is not in a fully evolved state. One prominent weakness is that module interdependencies in ML are restricted to be acyclic, which means that mutually recursive functions and data types must be written in the same module even if they belong conceptually in different modules. Existing efforts to remedy this limitation either involve drastic changes to the notion of what a module is, or fail to allow mutually recursive modules to hide type information from one another. Another issue is that there are several dialects of ML, and the module systems of these dialects differ in subtle yet semantically significant ways that have been difficult to account for in any rigorous way. It is important to come to a clear assessment of the existing design space and consolidate what is meant by “the ML module system” before embarking on such a major extension as recursive modules.
In this dissertation I contribute to the understanding and evolution of the ML module system by: (1) developing a unifying account of the ML module system in which existing variants may be understood as subsystems that pick and choose different features, (2) exploring how to extend ML with recursive modules in a way that does not inhibit data abstraction, and (3) incorporating the understanding gained from (1) and (2) into the design of a new, evolved dialect of ML. I formalize the language of part (3) using the framework of Harper and Stone, in which the meanings of “external” ML programs are interpreted by translation into an “internal” type system.
In my exploration of the recursive module problem, I also propose a type system for statically detecting whether or not recursive module definitions are “safe”—that is, whether they can be evaluated without referring to one another prematurely—thus enabling more efficient compilation of recursive modules. Future work remains, however, with regard to type inference and type system complexity, before my proposal can be feasibly incorporated into ML.
Cited By
- Sterling J and Harper R (2021). Logical Relations as Types: Proof-Relevant Parametricity for Program Modules, Journal of the ACM, 68:6, (1-47), Online publication date: 31-Dec-2022.
- MacQueen D, Harper R and Reppy J (2020). The history of Standard ML, Proceedings of the ACM on Programming Languages, 4:HOPL, (1-100), Online publication date: 14-Jun-2020.
- Crary K (2019). Fully abstract module compilation, Proceedings of the ACM on Programming Languages, 3:POPL, (1-29), Online publication date: 2-Jan-2019.
- Radanne G and Vouillon J Tierless Web Programming in the Large Companion Proceedings of the The Web Conference 2018, (681-689)
- Crary K (2017). Modules, abstraction, and parametric polymorphism, ACM SIGPLAN Notices, 52:1, (100-113), Online publication date: 11-May-2017.
- Crary K Modules, abstraction, and parametric polymorphism Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, (100-113)
- Tan Y, Owens S and Kumar R A verified type system for CakeML Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages, (1-12)
- Rossberg A (2015). 1ML – core and modules united (F-ing first-class modules), ACM SIGPLAN Notices, 50:9, (35-47), Online publication date: 18-Dec-2015.
- Rossberg A 1ML – core and modules united (F-ing first-class modules) Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, (35-47)
- Rossberg A and Dreyer D (2013). Mixin’ Up the ML Module System, ACM Transactions on Programming Languages and Systems, 35:1, (1-84), Online publication date: 1-Apr-2013.
- Im H, Nakata K, Garrigue J and Park S (2011). A syntactic type system for recursive modules, ACM SIGPLAN Notices, 46:10, (993-1012), Online publication date: 18-Oct-2011.
- Im H, Nakata K, Garrigue J and Park S A syntactic type system for recursive modules Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications, (993-1012)
- Rossberg A, Russo C and Dreyer D F-ing modules Proceedings of the 5th ACM SIGPLAN workshop on Types in language design and implementation, (89-102)
- Rossberg A (2008). Dynamic Translucency with Abstraction Kinds and Higher-Order Coercions, Electronic Notes in Theoretical Computer Science (ENTCS), 218, (313-336), Online publication date: 1-Oct-2008.
- Sasitorn J and Cartwright R (2007). Component nextgen, ACM SIGPLAN Notices, 42:10, (153-170), Online publication date: 21-Oct-2007.
- Sasitorn J and Cartwright R Component nextgen Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems, languages and applications, (153-170)
- Dreyer D (2007). A type system for recursive modules, ACM SIGPLAN Notices, 42:9, (289-302), Online publication date: 1-Oct-2007.
- Dreyer D A type system for recursive modules Proceedings of the 12th ACM SIGPLAN international conference on Functional programming, (289-302)
- Lee D, Crary K and Harper R Towards a mechanized metatheory of standard ML Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (173-184)
- Mandelbaum Y, Fisher K, Walker D, Fernandez M and Gleyzer A PADS/ML Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (77-83)
- Dreyer D, Harper R, Chakravarty M and Keller G Modular type classes Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (63-70)
- Lee D, Crary K and Harper R (2007). Towards a mechanized metatheory of standard ML, ACM SIGPLAN Notices, 42:1, (173-184), Online publication date: 17-Jan-2007.
- Mandelbaum Y, Fisher K, Walker D, Fernandez M and Gleyzer A (2007). PADS/ML, ACM SIGPLAN Notices, 42:1, (77-83), Online publication date: 17-Jan-2007.
- Dreyer D, Harper R, Chakravarty M and Keller G (2007). Modular type classes, ACM SIGPLAN Notices, 42:1, (63-70), Online publication date: 17-Jan-2007.
- Rossberg A (2006). The missing link, ACM SIGPLAN Notices, 41:9, (99-110), Online publication date: 16-Sep-2006.
- Owens S and Flatt M (2006). From structures and functors to modules and units, ACM SIGPLAN Notices, 41:9, (87-98), Online publication date: 16-Sep-2006.
- Nakata K and Garrigue J (2006). Recursive modules for programming, ACM SIGPLAN Notices, 41:9, (74-86), Online publication date: 16-Sep-2006.
- Rossberg A The missing link Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, (99-110)
- Owens S and Flatt M From structures and functors to modules and units Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, (87-98)
- Nakata K and Garrigue J Recursive modules for programming Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, (74-86)
- Dreyer D (2005). Recursive type generativity, ACM SIGPLAN Notices, 40:9, (41-53), Online publication date: 12-Sep-2005.
- Dreyer D Recursive type generativity Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, (41-53)
Recommendations
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 ...
Mixin' up the ML module system
ICFP '08: Proceedings of the 13th ACM SIGPLAN international conference on Functional programmingML 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 ...
Mixin' up the ML module system
ICFP '08ML 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 ...