Modules and Abstraction

A large program is not one calculus term — it is many, written by different people at different times, that must fit together without any one of them knowing the others' internals. The language feature that makes this possible is the module system: a way to package definitions behind an interface, hide their representation, and combine them. The ML tradition (Standard ML and OCaml) took modules further than any mainstream language, turning them into a small typed language of their own — structures (implementations), signatures (interfaces), and functors (modules parameterised by other modules).

The theoretical heart of all this is type abstraction: a module can export a type whose identity is public but whose representation is sealed away, so clients can hold values of that type and pass them around, yet cannot inspect or forge them. That is exactly the power of the existential type \exists X.\,T — and the deep result of this lesson is that an abstract type is an existential, and a module is a value of an existential type.

Signatures, structures, functors

Think of a stack of small typed objects, one level up from ordinary values:

Module construct	What it is	Term-level analogue
Structure	a bundle of type + value definitions (an implementation)	a record / a value
Signature	an interface: the types and value-types a structure must provide	a record type
Functor	a function from structures to structures	a (dependent) function

A signature lists type components as well as value components — and that is what ordinary record types cannot do. When a signature writes type t with no definition, it declares an abstract type: implementations must supply some representation, and clients get none. When it writes type t = int, the type is transparent (its identity leaks). The whole art of module design is choosing, component by component, what to reveal.

The diagram shows sealing: a structure implementing a counter as an int is ascribed the signature COUNTER whose t is abstract. After sealing, the outside world sees only the interface arrows — start, bump, read — and the concrete int underneath is invisible.

An abstract type is an existential

Here is the correspondence that unifies modules with the type theory you already know. A structure

signature COUNTER = sig type t (* abstract *) val start : t val bump : t -> t val read : t -> int end

has, as its type, the existential

\mathsf{COUNTER} \;=\; \exists\, t.\; \{\, \mathit{start}\!:\! t,\; \mathit{bump}\!:\! t \to t,\; \mathit{read}\!:\! t \to \mathsf{int} \,\}.

A structure sealed with this signature is exactly a package \mathsf{pack}\,[\mathsf{int},\, r]\,\mathsf{as}\,\exists t.\,T, where the witness type \mathsf{int} is hidden and r is the record of operations. A client that opens the module is an unpack: it gets a fresh, opaque type variable t and the operations over it, but no way to learn that t = \mathsf{int}. This is why abstraction is safe: the type checker literally forgets the representation.

Two sealed implementations of the same signature are observationally interchangeable: no well-typed client can distinguish a counter-as-int from a counter-as-{count:int}.
This is a corollary of parametricity for the hidden type variable — the client is polymorphic in t, so by the abstraction theorem it must behave the same for every choice of representation.

Sealing, in code

We cannot hide types dynamically in TypeScript, but we can model the module discipline: a maker returns a record of operations over an opaque token type, and clients are handed only that interface. Swapping the hidden representation leaves every client working, unchanged. Run it:

// The abstract type `t` is modelled by a branded opaque type: clients can hold it, not inspect it. type Counter = { readonly __t: unique symbol }; interface COUNTER { start: Counter; bump: (c: Counter) => Counter; read: (c: Counter) => number; } // Implementation A: a counter is just an int. const CounterInt: COUNTER = { start: 0 as unknown as Counter, bump: (c) => ((c as unknown as number) + 1) as unknown as Counter, read: (c) => c as unknown as number, }; // Implementation B: a counter is a record { n }. Same signature, different representation. const CounterRec: COUNTER = { start: { n: 0 } as unknown as Counter, bump: (c) => ({ n: (c as unknown as { n: number }).n + 1 }) as unknown as Counter, read: (c) => (c as unknown as { n: number }).n, }; // A client written ONLY against the COUNTER interface — no knowledge of the representation. function useThreeTimes(M: COUNTER): number { let c = M.start; c = M.bump(M.bump(M.bump(c))); return M.read(c); } console.log("via int rep:", useThreeTimes(CounterInt)); // 3 console.log("via rec rep:", useThreeTimes(CounterRec)); // 3 — indistinguishable

Both runs print 3: the client cannot tell the representations apart, which is representation independence made concrete. In a real ML, the as unknown as casts are unnecessary — the module system enforces the opacity for you, statically.

Functors: modules parameterised by modules

A functor is a function from structures to structures — the module-level analogue of \lambda. It is how ML expresses "generic over an implementation": a Set functor takes any structure supplying an ordered element type and produces a set structure for it.

functor MakeSet (Elt : ORDERED) : SET = struct type elem = Elt.t type t = elem list (* representation, hidden by SET *) val empty = [] fun add x s = ... uses Elt.compare ... end

Two subtleties give ML functors their reputation for depth. Sharing constraints let you demand that two argument modules agree on a type (sharing type A.t = B.t), which is needed to combine them soundly. And the generative vs applicative distinction asks whether applying a functor twice to the same argument yields compatible abstract types (applicative, OCaml) or fresh ones each time (generative, SML) — a question about the identity of the existential witness that has no counterpart in first-order type systems.

They rhyme, but they answer different questions. Both bundle operations with hidden state, but the axis of abstraction differs. Objects abstract over the representation of a single value and are built for extension and dynamic dispatch: you can add new implementations (subclasses) easily, but adding a new operation touches every class. Modules/ADTs abstract over a type and are built for a fixed set of operations over many values of that type: adding an operation is a one-line change, but the representation is fixed at the boundary. This is the two horns of the expression problem (Wadler): objects make new cases cheap, ADTs make new functions cheap. ML modules also add something objects lack — functors, true compile-time parameterisation of one module by another's types, which is strictly more expressive than generics because the parameter can itself carry abstract types.

A classic error is to believe that giving a structure a signature automatically hides its types. It does not — it depends on how you ascribe. Transparent ascription (M : SIG in SML) checks that M matches SIG but keeps every type identity visible, so M.t = int still leaks to clients. Only opaque (or "sealed") ascription (M :> SIG) actually makes the abstract types abstract. Mix these up and you will get either a mysterious "types don't match" error (over-sealing something a client needed to see) or, worse, an accidental leak where two modules become interchangeable because a type you meant to hide stayed transparent. The signature says what to hide; the ascription operator decides whether to hide it.