Modular Type Classes and Implicit Modules

Prerequisites. Direct starred prerequisites: Chapter 11, Chapter 12. No later core chapter depends on this route.

Suppose integer equality is available in two useful forms. The first compares integers literally; the second always returns false. Write their module evidence as $\mathsf{EqInt}$ and $\mathsf{EqNever}$. Now consider the surface program $$\begin{array}{l}\mathsf{module}A=\mathsf{using}\mathsf{EqInt}\mathsf{in}\mathsf{struct}\mathsf{let}fx=\mathsf{eq}(x,x)\mathsf{end},\\ \mathsf{module}B=\mathsf{using}\mathsf{EqNever}\mathsf{in}\mathsf{struct}\mathsf{let}y=A.f3\mathsf{end}.\end{array}$$ There are two plausible elaborations. If the definition of $A.f$ fixes the instance available at its definition, then $$A.f⇝\lambda x:\mathsf{Int}.\mathsf{EqInt}\mathsf{.}\mathsf{eq}(x,x),B.y=\mathsf{true}.$$ If generalization instead exports a class constraint, then $$A.f⇝\mathrm{\Lambda }(X:\mathsf{EQ}).\lambda (x:X.t).X.\mathsf{eq}(x,x),$$ and the call in $B$ may instantiate $X$ with $\mathsf{EqNever}$, giving $B.y=\mathsf{false}$. The two legal elaborations are observably different: the same surface binding has changed from a monomorphic value to an implicitly parameterized one. Local instance scope, polymorphic generalization, and module abstraction cannot be allowed to settle this question independently.

The parenthesized binders above are distinct: $X$ is a module parameter classified by $\mathsf{EQ}$, while $x$ is a term parameter whose type is the selected component $X.t$.

Explicit module passing avoids the ambiguity. Define $$\mathsf{same}(E:\mathsf{EQ}[\mathsf{Int}])xy:=E.\mathsf{eq}xy$$ and write $\mathsf{same}\mathsf{EqInt}33$. This places an evidence argument at every use. The design problem is to retain explicit modular configuration while reconstructing omitted module evidence predictably.

Classes as signatures and instances as modules

Ground types are finite constructor trees $$\tau ::=c({\tau }_1,\dots ,{\tau }_n),$$ where a nullary constructor is written without parentheses. Thus $\mathsf{Int}$, $\mathsf{Bool}$, $\mathsf{List}(\mathsf{Int})$, and $\mathsf{Pair}(\mathsf{Int},\mathsf{Bool})$ are ground types. Their size is $$|c({\tau }_1,\dots ,{\tau }_n)|:=1+\sum _{i=1}^n|{\tau }_i|.$$

Evidence for $K[\tau ]$ is a module $V$ with a transparent component equation $V.t=\tau$. Resolution therefore returns module paths and applications such as $\mathsf{EqList}⟨\mathsf{EqInt}⟩$; uniqueness means syntactic equality of those evidence trees, not observational dictionary coherence.

For example, The type component matters. A module containing an integer comparison but claiming $t=\mathsf{Bool}$ is not approximately suitable evidence; it is ill typed.

Compound evidence is constructed by module functors. The equality functors for products and lists have the interfaces Here ${\Rightarrow }_{\mathsf{mod}}$ describes a module functor interface, not an object language implication. Applying these functors gives the evidence term $$\mathsf{EqList}⟨\mathsf{EqPair}⟨\mathsf{EqInt},\mathsf{EqBool}⟩⟩:\mathsf{EQ}[\mathsf{List}(\mathsf{Pair}(\mathsf{Int},\mathsf{Bool}))].$$ An evidence functor is total and pure. Hence resolving $F⟨V_1,\dots ,V_n⟩$ neither diverges nor creates a fresh abstract type; repeated applications to the same transparent evidence denote the same evidence expression.

The corresponding display functors have interfaces

The decreasing condition rejects $$\mathsf{EqAgain}:\mathsf{EQ}[\alpha ]{\Rightarrow }_{\mathsf{mod}}\mathsf{EQ}[\alpha ].$$ Its result has no constructor layer that is removed by the premise. The module may be extensionally harmless, but unrestricted search can apply it forever. The condition also excludes useful instances whose premises are not structural subcomponents. It is deliberately stronger than the full calculus; a small theorem with visible hypotheses is preferable to a broader algorithm whose termination argument is left implicit.

Availability is not declaration

A repository may contain both $\mathsf{EqInt}$ and $\mathsf{EqNever}$. They conflict only if both are adopted for the same inference scope. We therefore distinguish a repository $\mathcal{R}$ of named, separately checkable modules from the finite lexical subenvironment $\mathrm{\Theta }\subseteq \mathcal{R}$ used by resolution.

The distinction gives three separate operations: Conflating the first two operations recreates the global-instance problem. Conflating the second and third hides configuration inside search.

The opening counterexample also shows why adoption cannot be inserted under an arbitrary expression and then forgotten at generalization. Let $m\in \mathsf{Inner}(S)$ mean that $m$ is an ordinary term or reduced-module phrase of chapter 12, checked at signature $S$, with no $\mathsf{using}$ form. The outer boundary grammar is exactly Only $T$ admits $\mathsf{using}$. The ascription fixes the signature exported across the boundary. In the opening program, the signature of $A$ must therefore choose between $$\mathsf{val}f:\mathsf{Int}\to \mathsf{Bool}\text{and}\mathsf{val}f:\mathrm{\forall }X:\mathsf{EQ}.X.t\to \mathsf{Bool}.$$ The first captures $\mathsf{EqInt}$; the second advertises a module parameter and lets each caller supply it. Scope no longer guesses which interface the programmer intended.

The finite elaboration judgment begins after the exported signature has chosen one of these two types for $A.f$. It inserts evidence for an already explicit class request; it does not decide whether $A.f$ is generalized.

Head-directed resolution

Resolution should construct the omitted module expression and nothing else. The judgment $$\mathrm{\Theta }⊢K[\tau ]{\Downarrow }_{\mathsf{res}}V$$ means that the available declarations construct evidence $V$ for the realized signature $K[\tau ]$. It is generated by two rules.

Evidence typing is the least judgment generated by the corresponding two declaration rules:

These are the evidence judgments used in the resolver theorem; field typing is added only when the evidence is inserted into ordinary terms.

Resolve the pair request first and name its evidence $$V_{\mathsf{pair}}:=\mathsf{EqPair}⟨\mathsf{EqInt},\mathsf{EqBool}⟩.$$ The pair evidence is derived by $$\frac{\begin{array}{c}{\displaystyle \frac{\mathsf{EqInt}\in \mathrm{\Theta }}{\mathrm{\Theta }⊢\mathsf{EQ}[\mathsf{Int}]{\Downarrow }_{\mathsf{res}}\mathsf{EqInt}}}\mathrm{R}-\mathrm{Base}\\ {\displaystyle \frac{\mathsf{EqBool}\in \mathrm{\Theta }}{\mathrm{\Theta }⊢\mathsf{EQ}[\mathsf{Bool}]{\Downarrow }_{\mathsf{res}}\mathsf{EqBool}}}\mathrm{R}-\mathrm{Base}\end{array}}{\mathrm{\Theta }⊢\mathsf{EQ}[\mathsf{Pair}(\mathsf{Int},\mathsf{Bool})]{\Downarrow }_{\mathsf{res}}{V}_{\mathsf{pair}}}\mathrm{R}-\mathrm{Functor}.$$ The outer application then has one premise: $$\frac{\mathrm{\Theta }⊢\mathsf{EQ}[\mathsf{Pair}(\mathsf{Int},\mathsf{Bool})]{\Downarrow }_{\mathsf{res}}{V}_{\mathsf{pair}}}{\mathrm{\Theta }⊢\mathsf{EQ}[\mathsf{List}(\mathsf{Pair}(\mathsf{Int},\mathsf{Bool}))]{\Downarrow }_{\mathsf{res}}\mathsf{EqList}⟨V_{\mathsf{pair}}⟩}\mathrm{R}-\mathrm{Functor}.$$

A naive resolver might enumerate all module expressions and test their signatures. That search rediscovers irrelevant functors, repeats identical subproblems, and diverges in the presence of $\mathsf{EqAgain}$. In ${\mathsf{MTC}}_0$, the result type already determines the only declaration that could finish a derivation. Resolution can therefore follow the pair $(K,c)$ at the root.

${\mathsf{resolve}}_{\mathrm{\Theta }}$ returns transparent module syntax $V:K[\tau ]$; dictionary entailment in chapter 11 instead returns an ordinary target term.

Elaboration inserts module evidence

To elaborate $\mathsf{eq}[\tau ](e_1,e_2)$, resolve $\mathsf{EQ}[\tau ]{\Downarrow }_{\mathsf{res}}V$, elaborate both arguments at $\tau$, and return $V.\mathsf{eq}{e}_1^{\prime }{e}_2^{\prime }$. Consider the ground source fragment with explicit type indices: $$e::=x\mid \lambda x:\tau .e\mid ee\mid \mathsf{eq}[\tau ](e,e)\mid \mathsf{show}[\tau ](e).$$

The target’s ordinary fragment is the simply typed lambda calculus on these ground types. Its module-evidence expressions are $$V::=P\mid F⟨V_1,\dots ,V_m⟩,e^{\prime }::=x\mid c\mid \lambda x:\tau .e^{\prime }\mid e^{\prime }{e}^{\prime }\mid V.f,$$ where $c$ ranges over the ground literals and primitives. The environment $\mathrm{\Theta }$ binds every path and total functor at its realized interface. Write $\overline{K}[\overline{\alpha }]$ for $K_1[{\alpha }_{j_1}],\dots ,K_m[{\alpha }_{j_m}]$. Besides the ordinary lambda rules, target typing has $$\begin{array}{c}\frac{P:K[c]\in \mathrm{\Theta }}{\mathrm{\Gamma };\mathrm{\Theta }⊢P:K[c]}\mathrm{Mod}-\mathrm{Path}\\ \frac{\begin{array}{c}\mathrm{\Theta }(F)=\overline{K}[\overline{\alpha }]{\Rightarrow }_{\mathsf{mod}}K[c(\overline{\alpha })]\\ \mathrm{\Gamma };\mathrm{\Theta }⊢V_r:K_r[{\tau }_{j_r}](1\le r\le m)\end{array}}{\mathrm{\Gamma };\mathrm{\Theta }⊢F⟨V_1,\dots ,V_m⟩:K[c(\overline{\tau })]}\mathrm{Mod}-\mathrm{Functor}.\end{array}$$ and $$\frac{\begin{array}{c}\mathrm{\Gamma };\mathrm{\Theta }⊢V:K[\tau ]\\ f:A(t)\text{ is a field of }K\end{array}}{\mathrm{\Gamma };\mathrm{\Theta }⊢V.f:A(\tau )}\mathrm{Mod}-\mathrm{Field},$$ Thus $F⟨\overline{V}⟩$ has its declared realized result when every $V_i$ has the corresponding realized premise interface. These rules type the finite slice’s module evidence.

Ordinary forms elaborate homomorphically. The two interesting rules are

For example, let $${\tau }_0:=\mathsf{List}(\mathsf{Pair}(\mathsf{Int},\mathsf{Bool})),V_0:=\mathsf{EqList}⟨\mathsf{EqPair}⟨\mathsf{EqInt},\mathsf{EqBool}⟩⟩.$$ The premise $\mathrm{\Theta }⊢\mathsf{EQ}[{\tau }_0]{\Downarrow }_{\mathsf{res}}{V}_0$ and two variable rules give $$x:{\tau }_0,y:{\tau }_0;\mathrm{\Theta }⊢\mathsf{eq}[{\tau }_0](x,y):\mathsf{Bool}⇝V_0.\mathsf{eq}xy.$$ The target records the module expression selected by resolution.

The proposition is preservation, not a theorem that every source program has an elaboration. Missing evidence, rejected overlap, and an unannotated ambiguous type can all prevent a derivation.

Residual constraints and polymorphic evidence

Ground resolution constructs a closed module expression. Type inference must also handle requests containing unknown types. Consider $$\lambda x:\alpha .\mathsf{eq}[\mathsf{Pair}(\mathsf{Int},\alpha )]((0,x),(0,x)).$$ The outer constructor already determines $\mathsf{EqPair}$. The integer premise is solved by $\mathsf{EqInt}$, while the request $\mathsf{EQ}[\alpha ]$ remains. Introduce an evidence variable $X:\mathsf{EQ}[\alpha ]$. The partially constructed evidence is $$\mathsf{EqPair}⟨\mathsf{EqInt},X⟩,$$ and the generalized target is $$\mathrm{\Lambda }\alpha .\lambda X:\mathsf{EQ}[\alpha ].\lambda x:\alpha .(\mathsf{EqPair}⟨\mathsf{EqInt},X⟩).\mathsf{eq}((0,x),(0,x)).$$ The residual constraint is not a failure. It is the interface exported by generalization.

For example, reducing $\mathsf{EQ}[\mathsf{Pair}(\alpha ,\alpha )]$ produces $$(X:\mathsf{EQ}[\alpha ],\mathsf{EqPair}⟨X,X⟩),$$ not two independently generalized parameters.

Here $\mathrm{\Sigma }$ denotes the residual module-evidence context; in lemma 16.11, lowercase $\sigma$ denotes an evidence substitution.

For the request $\mathsf{EQ}[\mathsf{Pair}(\mathsf{Int},\alpha )]$, reduction returns $$(X:\mathsf{EQ}[\alpha ],\mathsf{EqPair}⟨\mathsf{EqInt},X⟩).$$ Substituting any ground evidence $W:\mathsf{EQ}[\tau ]$ for $X$ yields well-typed evidence at $\mathsf{Pair}(\mathsf{Int},\tau )$. It yields exactly the evidence obtained by ground resolution when $W$ is itself the evidence selected by the ground resolver for $\mathsf{EQ}[\tau ]$.

The published modular-type-class calculus

Three forms deserve immediate calculation.

First, $\mathsf{canon}(S)$ requests the canonical module at a concrete class signature $S$. Its class parameters must be transparent, but associated type components may remain abstract. Thus a class can expose the selected carrier while retaining additional type-level information supplied by the instance.

Second, $$\mathsf{overload}\mathsf{eq}\mathsf{from}\mathsf{EQ}$$ elaborates to a constrained polymorphic value whose module parameter supplies the projection $X.\mathsf{eq}$. Instantiating that value finds a canonical module of a transparent realization of $\mathsf{EQ}$ and inserts it as a total-functor argument.

Third, $$\mathsf{using}P\mathsf{in}T$$ first checks that $P$ is usable, including the source calculus’s structural non-overlap test, and only then checks $T$ under $\mathrm{\Theta },P$. The form exists only at the top-module stratum, which is the formal repair for the scope/generalization failure at the beginning of the chapter.

Canonical evidence is not restricted to a named base path. The selected rules admit:

1. singleton modules for transparent type components;

2. componentwise canonical structures;

3. a path $P\in \mathrm{\Theta }$ at its atomic class signature;

4. application of a canonical total functor from $\mathrm{\Theta }$ to canonical argument evidence; and

5. conversion along equivalent signatures.

The fourth clause is the full-calculus analogue of R-Functor.

The inference algorithm does not immediately guess closed evidence for every constraint. It produces a type-and-module substitution $\delta$ and a constraint context $\mathrm{\Sigma }$. Constraint normalization performs canonical backchaining. For example, an equality constraint at $\mathsf{Pair}(\mathsf{Int},\alpha )$ reduces to a residual equality constraint at $\alpha$, with evidence $\mathsf{EqPair}⟨\mathsf{EqInt},X⟩$. This is the higher-order, structural-signature version of definition 16.10.

The expression can leave the intermediate carrier unconstrained. Distinct reader/printer module expressions can then solve the constraints, so the algorithm rejects the ambiguity. Soundness types one returned elaboration; coherence would compare all returned elaborations.

Modular implicits: evidence is a module expression

The examples in this section follow OCaml surface notation: list is postfix and a module functor is applied with parentheses. The formal ${\mathsf{MTC}}_0$ calculus above retains prefix $\mathsf{List}(A)$ and angle brackets $F⟨V⟩$; the notation change does not identify the two resolution systems.

Modular implicits move the implicit parameter into ordinary function syntax. For a module type $S$, a function may have an implicit module parameter $$\{M:S\}\to \tau .$$ An explicit call writes $f\{M\}x$; an omitted argument asks the resolver to construct a module expression. Candidate modules enter the search space through $\mathsf{implicit}\mathsf{module}$, local implicit-module bindings, implicit parameters, and explicitly opened implicit namespaces.

With the call $\mathsf{show}[1,2]$ constrains the missing module $M$ by $M.t=\mathsf{Int}\mathsf{list}$. Trying the functor $\mathsf{ShowList}$ transforms that constraint into $S.t=\mathsf{Int}$, which $\mathsf{ShowInt}$ solves. The evidence is the module expression $$\mathsf{ShowList}(\mathsf{ShowInt}),$$ not merely the name of a global dictionary.

Let $\mathcal{I}$ be the finite, lexically ordered collection of implicit module paths and total implicit-module functors currently in scope. Write $\mathcal{I};\mathrm{\Gamma }⊢S{\Downarrow }_{\mathsf{cand}}\{V_1,\dots ,V_n\}$ for candidate search after inference has generated the type-component equations for an omitted parameter of module type $S$. A module path is a candidate when its signature matches $S$. A functor application $F(V_1,\dots ,V_n)$ is a candidate when its result matches $S$ and each strictly earlier argument request has the unique candidate $V_i$. Reject cycles and nondecreasing self-applications, and quotient the resulting finite set by alpha-equivalence. The omitted-call boundary is $$\frac{\begin{array}{c}\mathcal{I};\mathrm{\Gamma }⊢S{\Downarrow }_{\mathsf{cand}}\{V\}\\ \mathrm{\Gamma }⊢f:\{M:S\}\to {\tau }_1\to {\tau }_2\\ \mathrm{\Gamma }⊢x:{\tau }_1\end{array}}{\mathcal{I};\mathrm{\Gamma }⊢fx⇝f\{V\}x:{\tau }_2}\mathrm{MI}-\mathrm{Call}.$$ Zero candidates is a missing-implicit error; two distinct candidates is an ambiguity error. For the list example the carrier equation first admits $\mathsf{ShowList}(S)$, reduces its premise to $S.t=\mathsf{Int}$, and closes uniquely with $S=\mathsf{ShowInt}$. If both $\mathsf{ShowList}$ and $\mathsf{CompactShowList}$ are eligible, the same calculation produces two candidates and MI-Call is inapplicable.

The decreasing check compares the constraints passed to successive applications of one functor. Thus $$\mathsf{ShowList}(\mathsf{ShowList}(\mathsf{ShowInt}))$$ is allowed when resolving an integer-list-list request: the carrier constraint loses one list constructor at each repeated application. In contrast, $$\mathsf{ShowAgain}(\mathsf{ShowAgain}(\cdots ))$$ with $\mathsf{ShowAgain}(S).t=S.t$ does not decrease and is rejected. Termination is required before uniqueness can be checked; silently ignoring a nonterminating branch could miss a second candidate.

Uniqueness concerns complete module expressions. If the two candidates are then the call is ambiguous even if both modules print some legal string. If two inheritance paths construct extensionally similar modules but are not recognized aliases, they also remain distinct candidates. Resolution is therefore not ordered by a hidden preference rule.

Resolving $\mathsf{SHOW}$ for a list of pairs constructs the nested evidence

"4"
5
[("hello",1); ("world",2)]
5.5

The archived prototype output confirms that this module expression elaborates the sample list [WBY15].

Implicit function types are lexically scoped functions

An implicit function need not denote a canonical class instance or a module. Consider the source term $$\mathsf{let}?:\mathsf{Int}=1\mathsf{in}\mathsf{let}f:\mathsf{Int}?\to \mathsf{Int}=?\mathsf{in}\mathsf{let}?:\mathsf{Int}=2\mathsf{in}f.$$ The body used to define $f$ is checked under a fresh implicit integer parameter, so it elaborates to the identity function. At the final occurrence of $f$, automatic implicit application chooses the innermost integer, namely $2$. The result is $2$. There is no globally canonical $\mathsf{Int}$ evidence, no distinguished type component, and no module expression to synthesize.

SI has ordinary arrows, implicit arrows, polymorphism, explicit variables, and query $?$; both arrows elaborate to ordinary System F arrows [OBL^+18]. Restricted types and full types are $$R::=b\mid X\mid T\to T,T::=R\mid T?\to T\mid \mathrm{\forall }X.T,b::=\mathsf{Int}.$$ Terms include explicit variables and functions, the query $?$, ordinary and implicit let bindings, type abstraction/application, and a stitching annotation. Bidirectional typing simultaneously elaborates into System F. Integer literals and addition elaborate homomorphically and never invoke implicit search.

The source uses one ordered context $\mathrm{\Gamma }$, writing explicit bindings as $x:T$ and implicit bindings as $?y:T$. The tags are part of the context syntax: $x$ ranges over explicit variables and $y$ over implicit variables, so the two membership tests below are disjoint. The judgments $\mathrm{\Gamma }⊢e\Rightarrow T⇝u$ and $\mathrm{\Gamma }⊢e\Leftarrow T⇝u$ respectively synthesize and check while producing a System F term. The type translation $(-{)}^{\ast }$ maps both ordinary and implicit arrows to ordinary arrows and is homomorphic elsewhere. The typing and elaboration rules are:

The checking query in SI-ImpE is therefore a SI-Query synthesis followed by SI-Stitch when its type is restricted. Crucially, SI-Query itself permits any matching implicit binding. Lexical priority is imposed on complete derivations by definition 16.16. Declaratively, SI-AllE may instantiate $\mathrm{\forall }X.T$ with any well-formed $S$. Algorithmically, synthesis creates a fresh metavariable $\alpha$, elaborates the consumer, and solves $\alpha$ when an application or checking judgment next constrains its expected type.

For the opening SI term, write the three implicit variables as $i_1,i_f,i_2$. The definition of $f$ checks as $$?i_1:\mathsf{Int},?i_f:\mathsf{Int}⊢?\Rightarrow \mathsf{Int}⇝i_f,$$ so implicit introduction gives $$f⇝\lambda i_f:\mathsf{Int}.i_f.$$ At the final use, implicit elimination generates a query at $\mathsf{Int}$; the rightmost eligible binding is $i_2$. The complete target therefore contains $$(\lambda i_f:\mathsf{Int}.i_f)i_2{⟶}^{\ast }{i}_2,$$ and the enclosing explicit lets substitute $2$ for $i_2$.

The derivation that selects the earlier binding $i_1$ in the opening shadowing context is not well scoped. If $D_1$ selects $i_1$ and $D_2$ selects the later eligible $i_2$, then $$\mathrm{res}(D_1)=i_1,\mathrm{res}(D_2)=i_2,i_1\text{ lies to the left of }{i}_2.$$ The defining comparison therefore fails for $D_1$ and succeeds for $D_2$.

This calculus answers the section’s question. An implicit function arrow elaborates to an ordinary function arrow, so it is dictionary-like in the weak sense that omitted values become explicit parameters. It differs in what those values mean and how they are found. SI searches lexical values by type and shadowing order. ${\mathsf{MTC}}_0$ and modular type classes construct class modules indexed by a distinguished carrier. Modular implicits search ordinary module expressions constrained by module types and type equations. The target may look like argument passing in all three cases, but the source static disciplines are not interchangeable.

The boundary between the three mechanisms

The chapter has used three different evidence disciplines.

All three elaborate omission into explicit target syntax. That shared last step is not enough to identify their coherence, termination, ambiguity, or abstraction theorems. A theorem transfers only through an explicit translation preserving the hypotheses that make resolution meaningful.

Sources and exact limits.

The modular-type-class development, including its declarative elaboration and inference-soundness theorem, is due to Dreyer, Harper, Chakravarty, and Keller [DHCK07]. Modular implicits and their archived OCaml prototype are due to White, Bour, and Yallop [WBY15]; their paper presents the design and elaboration but not a complete formal inference/coherence metatheory for OCaml. The SI calculus and the exact results in theorem 16.17 are due to Odersky, Blanvillain, Liu, Biboudis, Miller, and Stucki [OBL^+18]. Stable coherent implicits provide a useful neighboring calculus, but its theorems require its own stability and unambiguity conditions and are not silently inherited here [SdSOWM19].