## Modules Matter Most

When it comes to controlling the complexity of developing and, more importantly, maintaining a large system, the only game in town is modularity.  And as even the strongest proponents of unityped languages have come to accept, modularity is all about types (static types, of course, there being no other kind).  A decomposition of a system into modules consists of an application of the structural principle of substitution (transitivity of entailment, composition of maps) that is fundamental to the very conception of a type system:

$\displaystyle{{\Gamma\vdash M : A \qquad \Gamma,x:A \vdash N:B}\over{\Gamma\vdash [M/x]N:B}}$

In pedestrian terms the type $A$ is the “header file” describing $M$, and $N$ is the new code implementing specification $B$ in terms of an unspecified implementation of the functionality specified by $A$.  The interaction between $M$ and $N$ is mediated entirely by the type $A$; access to the source code of $M$ is denied to the client, precisely so that the dependence between the components is weakened in anticipation of future changes to $M$, or to allow for flexibility in development ($M$ need not even exist for the development of $N$ to proceed, as long as the type $A$ is specified).

To be most useful, it is important that the relationship between $M$ and $A$ be many-to-many, and not many-to-one or one-to-one.  Think of $A$ as the API for a mapping between keys and values.  It is absolutely essential that the language admit that many different modules $M$ be of type $A$, and it is absolutely essential that a given module $M$ satisfy many distinct types $A$, without prior arrangement.  The type $A$ is purely descriptive of the extensional behavior of a module of that type, and cannot be regarded as pinning down any particular implementation of that behavior.  Moreover, a given module may well support a variety of views, for example by “forgetting” certain aspects of it in particular contexts.  For example, one may neglect that an implementation of mapping supports deletion in a setting where only extension and application are required.

This is all pretty basic, but what surprises me is how few languages support it cleanly and simply.  One particularly awkward method is to rely on extra-linguistic “tools” that manipulate build parameters to switch choices of $M$ for a given $N$, quickly resulting in an ad hoc language of its own just to manage the build scripts.  Another technique is to manipulate or restrict inheritance so that some degree of modularity can be simulated, much as one can bang in nails using a pair of pliers.  A common methodology, in fact, attempts to cut down inheritance to provide what we had in ML in the early 1980’s (functors), obviating the intervening decades of maladaptations of bad ideas.

More disappointingly, for me at least, is that even relatively enlightened languages, such as Haskell or F#, fail to support this basic machinery.  In Haskell you have type classes, which are unaccountably popular (perhaps because it’s the first thing many people learn).  There are two fundamental problems with type classes.  The first is that they insist that a type can implement a type class in exactly one way.  For example, according to the philosophy of type classes, the integers can be ordered in precisely one way (the usual ordering), but obviously there are many orderings (say, by divisibility) of interest.  The second is that they confound two separate issues: specifying how a type implements a type class and specifying when such a specification should be used during type inference.  As a consequence, using type classes is, in Greg Morrisett’s term, like steering the Queen Mary: you have to get this hulking mass pointed in the right direction so that the inference mechanism resolves things the way you want it to.  In F# the designers started with the right thing (Caml) and eliminated the very thing that matters the most about ML, it’s module system!  Instead the F# designers added a bunch of object-oriented concepts (for the sake of compatibility with .net and with the mindset of MS developers), and tricked up the language with features that are more readily, and flexibly, provided by the module system.

Why bring this up?  Apart from general grousing, my point is that we had little choice in what language to use in teaching our students.  Modularity matters most, and we must have a language that supports flexible modularity in the form I am describing here.  When we examined our options, which we did very carefully, the only contenders are Standard ML and O’Caml.  We could have gone with either, but were persuaded to use Standard ML, which has worked beautifully for our purposes.  The decisive factor in choosing between the two ML’s was simply that we have a prior code base in Standard ML on which to draw, and there are two implementations of Standard ML that support parallelism (MLton and Poly/ML), albeit neither optimally for our purposes.  Haskell provides better support for parallelism (by undoing its unfortunate commitment to laziness, which results in an unusable cost model for both time and, especially, space), but wasn’t suitable because of its lack of support for modularity.

As I have mentioned, our plan is to re-do the introductory curriculum in Computer Science to modernize it and to place better emphasis on principles rather than current technologies.  One aspect of this is to re-do the standard Data Structures and Algorithms course to eliminate the over-emphasis on ephemeral data structures, and to treat parallel algorithms as the general case that encompasses the increasingly irrelevant case of one processor.  (Yes, this is a technological trend, but it is more importantly a conceptual change that emerges from focusing on language, rather than machine, models of computation.)  What is a data structure?  It’s a signature, or interface, written in the language you’re programming in.  What’s an algorithm?  It’s a structure, or implementation, of that signature.  A signature, such as that for a mapping, can be implemented in various ways, with different cost trade-offs (logarithmic lookup vs. constant lookup, for example).  A given algorithm, such as a balanced tree, can implement many different data structures, such as mappings or sets.  The distinction between a peristent and an ephemeral mapping is a difference of data structure, that is, of signature.  The demands are different, the algorithms are different.  We should be able to support both forms as easily and cleanly as the other, to be able to compare them, and to explain, for example, why the ephemeral case is of limited utility.  It is not too much to ask to be able to write these examples as running code, with a minimum of fuss or bother!

We have for decades struggled with using object-oriented languages, such as Java or C++, to explain these simple ideas, and have consistently failed.  And I can tell those of you who are not plugged into academics at the moment, many of my colleagues world-wide are in the same situation, and are desperate to find a way out.  The awkward methodology, the “design patterns”, the “style guidelines”, all get in the way of teaching the principles.  And even setting that aside, you’re still doing imperative programming on ephemeral data structures.  It just does not work, because it is fundamentally the wrong thing.  Just try to teach, say, binary search tree delete; it’s a horrific mess!  You wind up with absurd “null pointer” nonsense, and a complex mess caused by the methodology, not the problem itself.  Pretty soon you have to resort to “frameworks” and “tools” just to give the students a fighting chance to get anything done at all, distancing them from the essential ideas and giving the impression that programming is painful and ugly, an enormous tragedy.

Our solution is to abandon it entirely, pushing OO techniques to a more advanced level for students who wish to learn them, and concentrating on the basic principles of modularity, parallel and sequential cost analysis, and direct verification of running code at the introductory level.  Dijkstra used to say “beauty is our business”, to which I would add that life is too short, and bright minds too precious, to waste on ugly things.  And if you take this point of view seriously, the best and the brightest are drawn to, rather than repulsed by, the field.  Pace some of my colleagues at a Major Institute of Technology, students absolutely do love to program and do love the beauty of code, provided that the code you ask them to write is, in fact, beautiful.  There is little more dreary than the corporate bureaucracy of OOP, and few things more lovely than the mathematical elegance of FP.

[Update: word-smithing, again]

### 17 Responses to Modules Matter Most

1. dsannella says:

So what do you think about SML-style sharing specifications?

After many years of teaching and using SML modules, and doing SML-like things in my work on specification languages, I have to say that this is one aspect of the SML language design that really doesn’t seem to work very well in practice. It’s just much too hard to get things right, at least if you believe in data abstraction like I do and use opaque ascription a lot. I don’t know a better way to achieve the same end, but there should be one.

• Abstract Type says:

Good question, I will comment on this and other issues in teaching ML in another post to come shortly.

• schoenfinkel says:

The Haskell Report says the newtype is a form of renaming, and also that it makes a new type; this is a direct contradiction, since you can’t rename what doesn’t already have a name. The incoherent remarks, the insistence that the ‘representation’ is the same, and the stated purposes of the newtype declaration suggest other possibilities for interpretation. Since, to paraphrase Kant, I have no use for B in  newtype Backward = B Int  but to supply it to a function, the question is whether in an expression like f (B i) should be thought of simply as applying f to B i , as the syntax suggests and as would be the correct interpretation for a proper data declaration; or whether instead, it should be thought of as going with f, and thus as, so to say, adverbially modifying the action of the rest of the system on things of type Int. The latter is in fact the standard Haskeller’s experience with that sort of newtyping. It is only if this ‘experience’ can be shown incoherent that Morrisett’s remark has any content in this connection. For what is in fact the principal use of type classes, namely in connection with higher-kinded things, it also seems empty, since in fact there aren’t often many choices, e.g. for Functor or Monad instances. (Note further that to speak of modularity, composition, parametrization, etc. in this connection, since the great (*->*) type classes are basically forms in which *everything* hangs together; one is not stuck so to say with the Identity ‘monad’ or the Identity form of ‘applicative’ programming, but this point is too large for this margin). Of course none of this speaks to the intermediate cases, where everyone of course grants modules would be nice, but only to psteckler’s remark. I am learning a lot from these posts, thanks.

• schoenfinkel says:

Pardon incompetent WordPressing, the above remark, belongs below with psteckler’s. For ” (Note further that to speak of modularity, composition, parametrization, etc. in this connection,…” substitute ” (Note further that to speak of modularity, composition, parametrization, etc. in this connection, might be viewed as circular, ….)”

2. psteckler says:

Another excellent post.

I hadn’t before thought about the limitations of type classes you mention. Yes, you might want Int to be an instance of Ord in arbitrarily many ways. Like the Model T, you can choose any color, as long as it’s black.

• schoenfinkel says:

you can choose any color, as long as it’s black

This particular objection has to do with a particular concrete type though, and for that reason seems kind of weak. Getting new class instances is a standard use of the

newtype

keyword, explained a few pages into the average Haskell tutorial:
 newtype Backward = B {b :: Int} deriving Eq instance Ord Backward where (=) on b -- ghci> B 1 < B 0 -- True 

At the other extreme, though, the great type classes, like

Functor

and

 Monad

, attach not to concrete types but to things of kind

 (* -> *)

and when you look into them, it seems there usually aren’t to many ‘colors’ available. How many ways can

[]

or

 Maybe

 Functor

or

 Monad

? One great class in that family,

 Applicative

, does admit more than one list instance — thus the introduction of

 newtype ZipList a = ZipList [a]

in

Control.Applicative

.

I don’t mean to be objecting to the general point of the essay, which most Haskell users accept.

• Abstract Type says:

I know about newtype, of course. But, as the name implies, it’s a new type, it’s not int.

• schoenfinkel says:

Sorry, got my code tags mixed up there.

• schoenfinkel says:

Here’s more or less what I intended, if you care to replace this and the above mess. http://hpaste.org/raw/45786/type

3. gasche says:

And as even the strongest proponents of unityped languages have come to accept, modularity is all about types (static types, of course, there being no other kind).

I don’t agree about that idea. Modularity is about specification: when you write against an interface, what you care about is the specification of the interfaced component. Static types are an approximation of the specification, but they’re not the only one. For example, Racket documentation is expressed in term of dynamic predicates (the documented “type” of a construct will be something like real? -> (or (is-a color) false)). In absence of dependent types or at least refinement types, runtime specifications are usually more expressive than static specifications, even the static approximation is usually reasonable (in particular, parametricity gives a lot of information about the behaviour of a polymorphic function).

It’s true that most languages are converting towards a state where specification is more apparent, and checked by the language when possible : powerful static type systems, (static or dynamic) contract programming, etc. But I don’t think there is any consensus or even evidence that static types are The Right Way to expose the specification of a program. Have the Racket people ever said something like this, or are you considering the existence of Typed Racket as an implicit agreement?

I don’t personally believe in an “all static” world. It’s currently much too difficult to use proof assistants to completely specify programs, and I expect (even with the advance of proof methods) that for pragmatic, non-critical purposes, there will always be a dynamic part in specification enforcement.

Of course, if the specification is statically available (even if partially-dynamically checked), you can reason about it as you reason with static types, eg. your typing derivation is still relevant (only, parts of A will be statically admitted, and checked at runtime, or maybe A won’t capture all the modular information about the signature and there will still be “this function is associatve” comments in the signature code). But the insistence on static checking is, I think, misguided.

I also think you’re unfair to type classes. You’re right that they are not completely satisfying as a modularity tool, but your presentation make them sound bad in all aspects, which is certainly not true. The limitation of only having one instance per type may be a strong one, but it allows for a level of impliciteness that is just nice. There is a reason why, for example, monads are relatively nice to use in Haskell, while using monads represented as modules in a SML/OCaml programs is a real pain.
It’s a fact that type-classes are widely adopted and used in the Haskell circles, while modules/functors are only used for relatively coarse-gained modularity in the ML community. It should tell you something useful about those two features: they’re something that current modules miss (or maybe a trade-off between flexibility and implicitness that plays against modules for “modularity in the small”), and it’s dishonest and rude to explain the adoption difference by “people don’t know any better”.

More generally, I really enjoy reading your posts, but I’m a bit irritated by the constant attacks on non-ML languages. I think everyone understood by now that you don’t like OOP, and you have exposed fairly valid points for it, maybe you don’t need to add another stab in each new post. Adversarial style can be a good thing, but it should not be abused.

• Abstract Type says:

You seem to overlook that dynamic methods are a mode of use of static methods, as described in an earlier post. Any dynamic technique can be just as readily implemented in a static language, but not the other way around. “All static” includes “dynamic”, so there can be no opposition.

I’ve already published a paper on how to integrate the best features of type classes into a language with modules. Modules matter more, and you can get type classes as a minor special case, but not vice versa.

No insult intended in saying that someone doesn’t know any better; that’s why I teach.

4. egon says:

I have some trouble understanding the concept of “…given module M satisfy many distinct types A, without prior arrangement.”

Does this mean when I have a module M, I would be able to use it with header A or header A’ describing different way of using M?

For example I have a module M that has two stage initialization (M.create, M.init). Header A describes this two stage initialization (A.create, A.init) but header A’ describes only one stage initialization (A’.create). How would it be possible to do this without prior arrangement, ie without knowing A’? I mean, to properly use M through A’ you would have to know A’.

Usual approach to this would be to make a mapping from W : M -> M’ that satisfies A’ and make an accessor for the internal M that can be used with A as well. Essentially W is a wrapper for M and you could possibly use either W(M) or M depending on the need. But this is already a prior arrangement dependent on A’.

Maybe you can provide an example (with code) of this kind of many-to-many mapping between M and A?

• Abstract Type says:

I’m targeting pre-declared matching relationships, which do not scale. You don’t even know what signatures to specify, because they need not even exist when the structure is defined.

• pelotom says:

@egon: Using Haskell as an example, “without prior arrangement” means I can declare a data structure M to be an instance of a type class A without the authors of M being aware of it. Java, on the other hand, requires the author of a particular class (implementation) to anticipate the interfaces it belongs to a priori.

• egon says:

So essentially writing N is like writing a bridge for an interface (in Design Pattern terms)? This just means you need to write N by using the interface A… and I still fail to see the difficulty in that.

I mean can you point me to a concrete example where this is easy in SML and hard in OOP?

a small side note… :)

One particularly awkward method is to rely on extra-linguistic “tools” that manipulate build parameters to switch choices of M for a given N…, just as a comparison, what would you need to do in SML to switch the basis library, as I’m not that familiar with SML?

5. johnwcowan says:

So what’s to complain about? You have ML, go ahead and teach it. All your argument amounts to is, Païens ont tort et Chrétiens ont droit. But to oppose my postulates to yours:

Modules are about name control and only secondarily, if at all, about types.

F# is what it is: a .NET language first, ML second. If the F# developers wanted an implementation of ML on .NET, they could have had one, perhaps by modifying the SML implementation on the JVM, which interfaces with other JVM code only at the far end of a convoluted stick.

Beauty is in the eye of the beholder, and programming, like teaching, is primarily a job (I say this as a programmer who’s the son of two teachers).

Anyway, *plonk*.

• K. Crary says:

Modules are about name control and only secondarily, if at all, about types.

Focusing on name control gives you a cheap, inferior sort of modularity. Modules are (or should be) about abstraction not mere namespaces. What you want from your module system is to know that you can reimplement an abstraction independent of the rest of the system. The fact is, the mathematics of abstraction is shown by Reynolds’s abstraction theorem (a.k.a parametricity theorem) to be inextricably tied to types.

Follow