module systems

In this episode I discuss the paper "Modula-2 and Oberon" by Niklaus Wirth.  Modula-2 introduced (it seems from the paper) the idea of having modules with explicit import and import lists -- something we saw at the start of our look at module systems with Haskell's module system.  I note some interesting historical points raised by the paper.

Last episode we discussed how functors can describe a single level of a datatype.  In this episode, we discuss how to put these functors back together into a datatype, using disjoint unions of functors and a fixed-point datatype.  The latter expresses the idea that inductive data is built in any finite number of layers, where each layer is described by the functor for the datatype.

This episode continues the discussion of Swierstra's paper "Datatypes à la Carte", explaining how we can decompose a datatype into the application of a fixed-point type constructor and then a functor.  The functor itself can be assembled from other functors for pieces of the datatype.  This makes modular datatypes possible.

In a 2013 journal article titled "A Scalable Module System", Florian Rabe and Michael Kohlhase propose a module system called MMT (Modules for Mathematical Theories) for structuring mathematical knowledge.  The paper has a very interesting general discussion of module systems, from programming languages but also other areas like algebraic specification and theorem proving.  The system is based on a rather small set of concepts which subsume those of, for example, Standard ML's module system.  Thought-provoking!

I look back at the module systems we considered so far (Haskell's, Standard ML's, and Agda's), and consider a few points that are on my mind about these.  I also mention a few other languages' module systems (Clojure, Java 9).  I also ponder names and namespace management.

Agda's module system (beautifully described here) could be seen as intermediate between Haskell's and Standard ML's.  It supports nested parametrized modules with information hiding, but does not go all the way to higher-order functors (as in Standard ML).

SML has arguably the most complicated/powerful module system of any existing programming language.  It is a luxury RV to Haskell's camper van.  I take a high-level look, following a very nice paper by Xavier Leroy, titled "A modular module system".

I briefly survey the main features of Haskell's module system, and reflect a bit on its design.

I start Chapter 13 (in Season 2) of the podcast, on module systems.  Almost all programming languages I know include some kind of scheme for modules, packages, namespaces, or something like this.  I discuss the high-level ideas of namespace management and type abstraction, two main use cases for module systems.  Subsequent episodes will discuss module systems (from papers or documentation) of various languages.