Applicative and Generative Functors in Modular Type Checking

A functor is a function from structures to structures, and the type checker’s problem is deciding when two structures produced by functors have the same type. The answer is not forced by the definition of a functor; it is a design choice with visible consequences for how programs compose. The two coherent choices are called applicative and generative, and the difference shows up in a single question: given a functor F and a structure S, are the abstract types in F(S) and in a second application F(S) the same type?

The problem functors create

Suppose a module signature declares an abstract type and a functor produces a structure satisfying that signature:

signature ORDERED = sig
  type t
  val compare : t * t -> order
end

signature SET = sig
  type elem
  type set
  val empty : set
  val insert : elem * set -> set
  val member : elem * set -> bool
end

functor MakeSet (O : ORDERED) :> SET where type elem = O.t = struct
  type elem = O.t
  type set = elem list
  val empty = []
  fun insert (x, s) = x :: s
  fun member (x, s) = List.exists (fn y => O.compare (x, y) = EQUAL) s
end

The where type clause is what ties the result’s elem to the argument’s t; the :> is an opaque ascription, so set stays abstract to clients while elem remains equal to O.t.

Opaque sealing is what makes set abstract outside the functor: clients can hold values of type set and call the operations, but cannot inspect the representation. Inside, set is a list; outside, it is a type with no structure. This is the module system’s version of the encapsulation discussed in what private fields actually hide, with the important difference that the abstraction is enforced by the type checker rather than by a naming convention.

Now apply the functor twice to the same argument structure:

structure A = MakeSet(IntOrder)
structure B = MakeSet(IntOrder)

If the application is generative, each application creates a fresh abstract type, so A.set and B.set are distinct and a value of one cannot be passed to the other’s operations. If it is applicative, the abstract type is determined by the functor’s identity and the argument’s identity, so A.set and B.set are equal, and values move freely between them.

Generative semantics is the simple one to specify: a functor application is a value-level computation that allocates a type, exactly as a function call allocates a record. It is also the semantics of Standard ML, where each functor application generates new type names. The cost is that a program cannot factor its use of a functor across modules without either threading a single application’s result through every client or accepting that two independently created sets are incompatible.

Applicative semantics and path equality

Applicative semantics replaces allocation with a rule about paths. The type of an abstract type component is identified by the path through which it is reached: the functor’s name plus the argument’s path. Two applications of MakeSet to the same structure path yield the same type, and two applications to structurally equal but distinct paths do not. In OCaml this is expressed by strengthening: a module’s signature is strengthened with equations naming the module’s own path, so IntOrder.t remains equal to itself when reached through different routes, and a functor’s result type refers to the formal parameter’s type rather than to a newly allocated one.

The practical benefit is composition. A program can build a set of integers in one module and a map keyed by integers in another, both from the same IntOrder, and pass an integer-typed key between them without a coercion. Applicative semantics makes the module system behave like a partial evaluator over type-level identities: the same inputs produce the same outputs, and the type checker can see it.

The practical cost is that applicative semantics requires the type checker to decide equality of paths, and paths are not always canonical. A structure can be reached through an alias, through a functor result, or through a signature ascription that hides the path. Implementations therefore need a notion of type identity that is stable under aliasing but not under substitution, and the details of strengthening are where module systems become subtle. In OCaml an applicative functor applied to two structures that are separately defined but have identical contents yields two unrelated types, because the paths differ; sharing requires one path, which is usually achieved by defining the argument once and referring to it by name.

A further consequence: an applicative functor whose result contains mutable state behaves badly in exactly this case. If two applications share the same abstract type, it is natural to assume they also share the same values of that type, but the two structures are separate at run time, each with its own empty set. Sharing the type while duplicating the state is sound — the type only says which operations accept the value — but it can surprise programmers who read type equality as object identity. For this reason a module that holds a store and wants a type unique per instance is a poor fit for applicative functors and a natural fit for generative ones: each SML application really does produce a distinct structure, so a type that was meant to be unique per application is unique per application.

Generative functors as an escape hatch

Because applicative semantics is not always what a module wants, languages that default to it offer an explicit generative form. In OCaml, a functor written with an empty parameter, functor () -> ..., is generative: every application creates a fresh abstract type, and the type checker does not attempt to relate the results. The syntax makes the allocation visible at the definition site, so a reader can tell from the functor’s header whether two applications will be compatible.

The design reason for the empty parameter is that generativity is a property of the application, not of the argument. Writing F() reads as a value construction, which is what it is: a fresh type and a fresh store. The alternative — a separate keyword or an attribute on the functor — would either change the meaning of existing functor definitions or require a second class of functor in the grammar. The empty parameter reuses the existing application form and gives generativity a place in the type syntax.

Standard ML has no applicative mode, so the same effect is achieved differently: a functor application inside a structure is evaluated once, and the resulting structure is passed around, so a program that needs one shared type simply applies the functor once at the top level and refers to that structure everywhere. The discipline is manual rather than enforced by the type system.

Sealing, sharing, and the direction of information flow

A signature ascription can be transparent or opaque, and the choice interacts with both semantics.

A transparent ascription, written in Standard ML as : SIG on a structure whose signature is already known, or in OCaml as : SIG where the signature’s type equations are retained, keeps the type equalities visible. A client that knows the representation can rely on it. An opaque ascription, Standard ML’s :> SIG, hides the representation. In Standard ML the resulting type is abstract in the strongest sense: no type outside the structure is equal to it, so the only way for a client to obtain or use a value of that type is through the operations the signature declares. In OCaml the hidden type still has a path-derived identity, so a second ascription with the same signature can produce a type that the checker considers equal; the equality does not, however, expose the representation or let the client construct values outside the module’s operations.

Sharing constraints express the opposite direction. A signature can require that two of its abstract types be equal, or that a type in one parameter equal a type in another:

functor Pair (A : ORDERED) (B : ORDERED
  sharing type A.t = B.t) = struct ... end

The constraint is checked at application time, and it is what allows a functor to require that its two arguments agree on a key type without naming that type in advance. Without sharing, the functor could only be written for a fixed type, which defeats the point of parameterising over it. OCaml expresses the same requirement with with type constraints on the result signature and with module type constraints in the parameter, which achieves the same effect through a different syntax.

The interaction with applicative semantics is the delicate part. If a functor’s result type is determined by the paths of its arguments, then a sharing constraint between two arguments changes which paths are equal, and therefore changes the result type. Implementations must propagate the equation through the functor’s body, and a type checker that strengthens too eagerly will report equalities the programmer did not intend, while one that strengthens too little will reject programs that should typecheck. This is the practical reason module systems are hard to implement well, and why the formal treatments of the subject spend most of their length on the equational theory rather than on the syntax.

What the choice costs a program

Applicative semantics makes modules compositional: a library can expose a functor and clients can instantiate it repeatedly without losing type compatibility. It makes type checking more expensive, because equality now depends on paths and on the equations introduced by ascription, and it makes some programs inexpressible without an explicit generative escape.

Generative semantics makes type checking local: each application is a fresh name, and equality is syntactic. It makes composition harder, because a program that wants one shared type must arrange for one application, and it ties type identity to the number of times an application is evaluated rather than to the paths involved.

Neither is a superset of the other. A language can offer both, as OCaml does, and let the programmer choose per functor. The choice is recorded in the functor’s type, so it composes: a functor that takes another functor as an argument must be written against one semantics or the other, and the two cannot be mixed freely without a wrapper. That is the same shape of trade-off as the one described in method resolution order in multiple inheritance: a global rule that makes composition predictable, at the cost of forbidding some hierarchies that a local rule would allow.