The Measure of a Module
WIP
module (n.)
1580s, “allotted measure,” a sense now obsolete, from Middle French module (1540s) or directly from Latin modulus “small measure,” diminutive of modus “measure, manner” (from PIE root \*med- “take appropriate measures”). Sense of “a standard measure to regulate proportions” is from 1620s. Meaning “interchangeable part” is recorded by 1955, via the notion of “length chosen as the basis for the dimensions of parts of a building …
The term, parameter, etymologically, and literally, means a “measure with respect to”.
…
A property is a parameter, or a notatoinal device for exhibiting a parameter.
TODO What is a module?
TODO read
Notes
In OCaml, a module is specified by a sig and implemented as a struct:
module Some_module : sig (* ...type declarations and value specifications... *) end = struct (* ...type declarations and value bindings... *) end
This is all in accord with the ML module system that was developed in the early 80s. The spirit of the ML module system traces back to an effort to “give structured descriptions of theories”, and the theories that are to be described are “algebraic theories” as developed by Lawvere.
In “Modules for Standard ML”, which proposes all of the most important aspects of ML modules, David McQueen wrote:
This proposal is based on the fruits of a long collaboration with Rod Burstall on prototype designs for modules in Hope [MAC81], and on theoretical investigations with Ravi Sethi and Gordon Plotkin [MAC82, MAC84] that were motivated by those designs. The module designs for Hope were in turn influenced by the Clear specification language of Burstall and Goguen [BUR77].
“[BUR77]” refers to Burstall and Goguen’s paper “Putting theories together to make specifications.” The first line reads:
We have been developing a language in which you can give structured descriptions of theories.
Under the section “What we mean by a theory”, they explain
The notion of theory is a loose intuitive one in mathematics. There should be axioms, rules of inference and theorems, but the language in which they are expressed is open to choice. … We have chosen an algebraic notion of theory, due to Lawvere (1963) [references his 1963 thesis Functorial Semantics Of Algebraic Theories (Lawvere 1963)] …
(1047)
Later they give their definition of a theory and an algebra:
A theory is a signature together with a set of equations closed under inference by reflexivity, transitivity and symmetry of equality and by substitution.
…
The interpretations of a theory are algebras, where an algebra is a collection of sets, one for each sort, with a function over these sets assigned to each operator of the theory.
(1048)
A central concern in their effort is to ensure that theories can be composed out of smaller components:
As soon as [theories] get to be interesting they become incomprehensible. We wind up with a large set of equations that no-one can understand and which are almost certainly wrong. So we must build our theories up from small intelligible pieces. For this we need
Their elaboration of the concept of a “theory” and the motives behind that work are of great importance.
To flesh out these definitions, I present (what I believe to be) examples of corresponding language constructs in OCaml:
…
ML modules are composable, nestable, inheritable, and parametric environments.
TODO Modularity and parametricity
Reynolds introduced λ2 in the 1974 paper “Towards a theory of type structure” (Reynolds 1974). In that paper, the innovation explained in the preceding is described as a solution to “the old but neglected problem of polymorphic functions”, but this problem is only given secondary importance. The principle aim of the work is to formalize a theory of representation independence for programs in order to ensure a program can maintain the seam meaning regardless of the internal representation of its primitive types:
We start with the belief that the meaning of syntactically valid program in a “type-correct” language should never depend upon the particular representations used to implement its primitive types.
… this property of reference independence should hold for user-defined types as well as primitive types. The introduction of a user-defined type
tshould partition a program into an “outer” region in whichtbehaves like a primitive type and is manipulated by various primitive operations which are used but not defined, and an “inner” region in which the representation oftis defined in terms of other types, and the primitive operations ontare defined in terms of this representation. We expect that the meaning of such a program will remain unchanged if the inner region is altered by changing the representation of the type and redfining its primitive operations in a consistent manner.
In providing polymorphic functions, we also provide user-defined types. … Suppose we with to represent complex numbers by pairs of reals, and to represent magnitude and the square root of -1 by the expressions
addrep : (real × real) × (real × real) -> (real × real) magnrep : (real × real) -> real irep : (real × real)
This representation can be specified by the expression
(Λcmp. λadd : cmp × cmp -> cmp. λmagn : cmp -> real. λi : cmp. outer) [real × real] (addrep) (magnrep) (irep) .
TODO Relation to Objects
The notion of a module as a theory (a set or collection of sets with operators over them) stands in defiance of joe Armstrong’s differentiation between FP and OOP in terms of weather or not you package functions and data structures together.
Parametric modules, especially when they can be 1st class, enable idioms which are reminiscent of OOP. E.G.:
TODO Example
TODO Clarify theory vs. model.
However, there is at least one critical formal difference – unbounded recursion – and one critical theoretical difference – paramtetric modules let us represent ideal objects as theories vs. whereas OOP uses the concept of objects to…
How does modularity relate to SOLID?
TODO Explain modules as an existential type quantification
TODO Anti-modular cultural tendencies
Several years back, I spent a chunk of time filing in missing pieces of the Rosetta Code project. When I was focused on SML implementations, I discovered a recurring pattern: in many of the tasks I was working on, extraneous criteria had been introduced to the task description, which posed serious challenges to properly modular compositions.
I spent a significant amount of time attempting to discover a technical solution to this obstacle. However, I gradually came to realize that this conflation of tasks was indicative of a more pervasive problem: it was symptomatic of the pervasive bias toward impure and anti-modular design patterns in programming culture.
This bias leads to a deep, culturally-based anti-modularity (and non-composability): the tendency to mix in extraneous, side-effectual processes with simple, potentially pure algorithms, prohibits the use of interesting and useful languages that don’t cater to these questionable practices.
Cultural problems call for cultural solutions, so I proposed correcting this defect. I now realize that this kind of conscious alteration and improvement of the conditions in which we work are at least as vital for the advancement of modular design as are technical solutions. (re: the cultural roots of technical practice, see The Life Cycle of Programming Languages.)
Two tiny actions I took to change the culture: