In this essay, I will consider two approaches to integrating a module system into a programming language: one by Harper and Lillibridge [7], and one by Rossberg et al. [12]. By contrasting their designs, I will strive to answer the question “Is there a canonical approach for building a programming language with modules?”
The Many Faces of Modules
To consider how modules should fit into a programming language, I shall first consider what they are.
Modules, as Seen by Programmers
To the programmer, module systems manage a tension between separation and integration [5]. Programming-in-the-large involves integrating code separated by time and space, with the module the unit of integration. Integration, while necessary to programming at scale, creates inter-dependencies that increase the fragility of a system. Integration should thus be explicit, and carefully mediated by signatures: minimal and explicit descriptions of the extensional characteristics of a module [3]. These signatures choose what to keep hidden (separate) and what to expose (integrate) and therefore make manifest the key problem of module systems.
In my opinion, therefore, the programmer’s experience with modules is chiefly determined by three orthogonal qualities:
- Expressiveness of signatures. The degree of control signatures offer in fine-tuning separation and integration,
- Modularity between signature and module. The ability to ascribe one signature to many modules, and vice versa, without prior arrangement [3], and
- Compositionality of signatures. The ability to specify equational constraints between signatures. Examples include sharing and parameterisation (functors) [10].
To expand on the first point, note that by balancing separation and integration, signatures manage a tension between internal prescriptiveness and external descriptiveness. For example, consider the following signature for an integer stack [8]
sig { type T = int;
type Stack = T list ref;
val new: unit -> Stack;
val push: Stack -> T -> Stack; }
This “transparent” signature hides no implementation details. It is extremely descriptive, but at the cost of being extremely prescriptive: implementations must commit to using int list ref to implement the stack. Excess transparency results in unnecessary integration, increasing the brittleness of large systems.
In contrast, consider the following “opaque” signature, that obscures implementation details
sig { type T;
type Stack;
val new: unit -> Stack;
val push: Stack -> T -> Stack; }
This signature is less descriptive, and in doing so buys the implementer more flexibility. There is, however, a problem. Assuming M is a module with the aforementioned signature, the following code does not type-check:
M.push(M.new(), 1)
It does not type-check because the signature is too opaque: without explicit description, the type-checker cannot conclude that int is equal to type M.T.
The programmer experience can be improved by allowing some transparency and some opacity in the same signature. In this scenario, we want a signature in which T is transparent but Stack is opaque
sig { type T = int;
type Stack;
val new: unit -> Stack;
val push: Stack -> T -> Stack; }
This is precisely the functionality offered by Harper and Lillibridge’s [7] translucent sums, which have superseded preceding approaches [2]. If there is a canonical module system, a programmer might expect it to contain translucent sums.
Modules, as Seen by Language Designers
While from a programmer’s point-of-view, the desiderata of a module system are clear, the responsibility of a programming language designer is not to build a good module system, but a good programming language. Hence, one has to consider how modules interact with various other aspects of language design. Unfortunately, the story here is not quite as straightforward.
Cognisant that Harper and Lillibridge merely show that translucent sums can be built, and do not claim that their design is canonical, I now take their design as an example of this complexity.
Building on an approach by MacQueen [9], Harper and Lillibridge’s [7] very first step is to take System \(F_\omega\), cross out products, functions, and universal abstraction, and replace them with the “more powerful” translucent sum and dependent product. This has several undesirable effects.
First, it “severely complicates the type system” [2], making implementation challenging. Consider a language without dependent types, like ML. The ML type system that handles core terms is “too weak” to support dependent types [11]. Modules must thus be introduced as a secondary sub-language, creating “two languages in one” [11].
Second, the introduction of dependent types threatens phase distinction: since types may now contain terms, type-checking may require evaluation. This trade-off might be expected if one is designing a language with dependent types, but is a high cost if the goal is simply to build a module system. In order to circumvent this problem, Harper and Lillibridge only allow “extended values” in types. Equating “extended values” does not require evaluation. Further, they do not use the “traditional elimination rules” for dependent sums and products, since it requires “substitution of arbitrary terms into types”. Concretely, it means that functor application is typed like non-dependent application and module projection is typed like non-dependent projection. Lillibridge [8] argues that this covers “most cases”, since fully transparent signatures and named modules feature no real dependencies between declarations, and thus can be typed non-dependently. This “solution”, however, means that the use of modules is governed by special cases, not universal laws. Hence, modules might not compose as expected. For example, assuming X is a name for a module and \(M\) a module expression, the following equality does not hold
\[ \texttt{module X = }M\texttt{ in X.T} \neq M\texttt{.T} \]
since the former always type-checks and the latter does not [8].
There is nothing inherently wrong with special cases! For example, pure terms can be seen as a special case of impure terms. In my opinion, complexity in a programming language system is bad insofar as it threatens the formation of a cohesive conceptual model. This is, again in my opinion, the true purpose of a metatheory. Properties like soundness and preservation are desirable because they provide means of extrapolation in a conceptual model: “if \(e\) has type \(T\) then it will always remain of type \(T\)”. While some special cases can be mapped onto a conceptual model, it is also easy to invent artificial ones that cannot. Viewed through this lens, “computational trinitarianism” [4] is nothing but a litmus test – if an idea has meaning in type theory, proof theory, and category theory, then it is more likely that one can lift it out of a synthetic system and into some conceptual model (in fact, precisely the model that carries intuitions from one theory to another). Harper and Lillibridge present their special cases as necessary adaptations rather than elements of a bigger picture, and thus I remain sceptical.
The Power of Starting Afresh
Can we do away with artificial complexity? Does the long arc of programming language design bend towards a clear conceptual model?
At least in the example of dependent types, the answer seems to be: “yes”. Rossberg et al. set out to give an account of modules independent of “opaque” or bespoke techniques – in other words, a clearer conceptual model.
Unlike Harper and Lillibridge, their model (which includes translucent sums) does not modify \(F_\omega\), but rather elaborates into \(F_\omega\). Modules elaborate into introduction (pack) and elimination (unpack) rules for existential types, much like how let bindings elaborate into introduction and elimination rules for function types. Thus, modules are “a particular mode of use of \(F_\omega\)”. The key idea is that in a signature, dependent sums are really only useful for capturing internal dependencies. For example, consider the following signature declaration:
{ module A: { type T; val x: T }
signature S: { val f: A.T -> int } }If we are allowed to disregard the internal ordering of A and S, then we can lift an internal dependency out, turning it into an external dependence on an existentially-bound variable
\[ \exists \ca{\alpha}. \texttt{\{ A : \{t : [= }\ca{\alpha}\texttt{], v : [}\alpha\texttt{]\}; S : [= \{f: [}\ca{\alpha}\texttt{ -> int]\}]\} } \]
A similar trick can be employed for functors: the result of a functor is not parameterised by the input module, but by its abstract types [8].
By avoiding using dependent sums and products, we avoid their complexities. For example, we resolve the phase distinction problem – types do not depend on terms.
Simplicity buys conceptual clarity. As a means for understanding their elaboration, Rossberg et al. encourage thinking about modules through the lens of monads. Module creation via pack should be thought of as monadic return, and unpack as monadic bind. For example, assuming the module expression \(M\) is elaborated into \(e\), then the module binding module X = \(M\) is elaborated into a form resembling monadic bind:
\[ \texttt{unpack(x, }\bar\alpha\texttt{) = }e\texttt{ in pack(\{X = x\}, }\bar\alpha\texttt{)} \]
This interpretation aids conceptual clarity. It explains the inequality
\[ \texttt{module X = }M\texttt{ in X.T} \neq M\texttt{.T} \]
module is monadic bind, so the RHS is attempting to use the “impure” module expression \(M\) in a “pure” way. This explanation casts the inequality as the result of a principle, rather than an engineering trick, thus more easily incorporating it into a conceptual model.
More generally, treatment of modules as impure computations is both justifiable and clarifies many of their characteristics. Harper [6] encourages us to think of sealing as having a pro forma effect. Signatures are unlike normal types. In a monadic type system, types do not abstract away effects. We can thus infer knowledge from what is not explicitly stated by the type. For example, a term of type int is definitely pure, since the type does not claim to be impure. Module signatures hide as much as they describe: hence, unlike a type, a signature is allowed to hide impurity. Consequently, module types are impure by default, unless explicitly claimed otherwise. This additionally explains the generativity of functors [6], since equations like
\[ \texttt{N = F(M)} \implies \texttt{N.t = F(M).t} \]
rely on some notion of purity [2].
Philosophically, we might choose to see programming language designers as modellers of user desiderata. Hence, models (in this case, the dependently-typed account of modules) are analytic. An analytic model can both be useful and wrong [1]. Rossberg et al.’s [12] story is thus a parable: a reminder that questioning “conventional wisdom” [9] can lead to better analytic models.
Starting Afresh, Properly?
Yet Rossberg et al. only tell a partial story: one of second-class modules, first-order modules, and generative functors. While work has been done to generalise the approach to first-class modules [11], it is unclear how far the technique scales. A canonical approach to models still seems elusive.
Perhaps Rossberg et al. do not go far enough. An alternative perspective is that language designers are not analytic modellers, but synthetic modellers: extracting usable designs from hand-crafted axiomatic systems. A synthetic account of module systems is illustrated by Harper. Modules, rather than types and values, are the atoms of the language. Types are synthesised from modules: a type is nothing but a degenerate structure, with a universe of types a degenerate signature. Thus, everything is a “mode of use” of modules. Encouragingly, this perspective is shared by Rossberg [11], in his analytic account of first-class modules. To me, this convergence of perspectives teases a potential canonical model.
Neither Rossberg et al. nor Harper and Lillibridge suggest that their approach is canonical. However, the trajectory of research suggests one might exist – though potentially in a wholly unexpected, synthetic form.
References
- [1] G. E. P. Box. Science and Statistics. Journal of the American Statistical Association, 71(356), pages 791–799. 1976. doi.org/10.1080/01621459.1976.10480949
- [2] D. Dreyer. Understanding and Evolving the ML Module System. PhD thesis, Carnegie Mellon University. 2005.
- [3] R. Harper. Modules Matter Most. 2011. existentialtype.wordpress.com/2011/04/16/modules-matter-most/
- [4] R. Harper. Introduction to Dependent Types Lectures, Oregon Programming Languages Summer School. 2015.
- [5] R. Harper. Types for Program Modules. 2021. www.youtube.com/watch?v=81BdQ6rdlOY
- [6] R. Harper. Phase Distinctions in Type Theory. 2022. www.youtube.com/watch?v=7DYkyB1Rm3I
- [7] R. Harper and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 123–137. 1994. doi.org/10.1145/174675.176927
- [8] M. Lillibridge. Translucent Sums: A Foundation for Higher-Order Module Systems. PhD thesis, Carnegie Mellon University. 1997.
- [9] D. B. MacQueen. Using dependent types to express modular structure. In Proceedings of the 13th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 277–286. 1986. doi.org/10.1145/512644.512670
- [10] Y. Minsky, A. Madhavapeddy, and J. Hickey. Real world OCaml. 2013. ci.nii.ac.jp/ncid/BB14521330
- [11] A. Rossberg. 1ML – core and modules united (F-ing first-class modules). In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, pages 35–47. 2015. doi.org/10.1145/2784731.2784738
- [12] A. Rossberg, C. V. Russo, and D. Dreyer. F-ing modules. In Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation, pages 89–102. 2010. doi.org/10.1145/1708016.1708028