Type Inference, Principal Typings, and Let-Polymorphism
for First-Class Mixin Modules ∗Henning Makholm

J. B. Wells

Technical University of Denmark †http://henning.makholm.net/

Heriot-Watt University
http://www.macs.hw.ac.uk/∼jbw/

Abstract

1. Introduction

A mixin module is a programming abstraction that simultaneously
generalizes λ-abstractions, records, and mutually recursive definitions. Although various mixin module type systems have been developed, no one has investigated principal typings or developed
type inference for first-class mixin modules, nor has anyone added
Milner’s let-polymorphism to such a system.
This paper proves that typability is NP-complete for the naive
approach followed by previous mixin module type systems. Because a λ-calculus extended with record concatenation is a simple
restriction of our mixin module calculus, we also prove the folk belief that typability is NP-complete for the naive early type systems
for record concatenation.
To allow feasible type inference, we present Martini, a new
system of simple types for mixin modules with principal typings.
Martini is conceptually simple, with no subtyping and a clean andbalanced separation between unification-based type inference with
type and row variables and constraint solving for safety of linking
and field extraction. We have implemented a type inference algorithm and we prove its complexity to be O(n2 ), or O(n) given a
fixed bound on the number of field labels.1 To prove the complexity, we need to present an algorithm for row unification that may
have been implemented by others, but which we could not findwritten down anywhere. Because Martini has principal typings, we
successfully extend it with Milner’s let-polymorphism.

The goal of this work is to produce a type system for first-classmixin modules that would have principal typings and thus support
compositional type analysis.
As a programming tool, first-class mixin modules are aimed not
only at programming-in-the-large issues such as generic modules
and dynamic linking, but also at programming-in-the-small issues,
because they combine the features of λ-abstractions (first-class
functions), records, environments with mutually recursive definitions, and namespaces [31]. A mixin module consists of named
components; some are exports that the module defines for othermodules, some are imports to be supplied by other modules, andsome are locals, i.e., private to the module. Once all imports are
satisfied by linking modules, the exports can be extracted.
Linking is symmetric: when A and B are linked together, A’s exports can satisfy B’s imports and vice versa. For example, consider
the following two modules, where N(g, i) stands for some expression containing the identifiers g and i and so forth for O, P, Q:

Categories and Subject Descriptors D.3.3 [Programming Languages]: Language Constructs and Features—Data types and structures; modules, packages; polymorphism
General Terms Design, theory, algorithms
Keywords Type systems, mixin modules, record concatenation,
row unification, polymorphism∗ Supported by EC FP5/IST/FET grant IST-2001-33477 “DART”, and Sun
Microsystems equipment grant EDUD-7826-990410-US.
† Work done while at Heriot-Watt University.
1 Technically, there is also a factor of α(n), but α(n) ≤ 4 for n < 1010100 (a“googolplex”).

Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior specific permission and/or a fee.
ICFP’05 September 26–28, 2005, Tallinn, Estonia.
c 2005 ACM 1-59593-064-7/05/0009. . . $5.00.
Copyright °A = {[export f = N(g, i); import g, h; local i = O(h)]}B = {[import f; export g = P(f, i); local i = Q]}
Linking A and B produces this combined module:A ⊕ B = {[export f = N(g, j), g = P(f, k); import h;local j = O(h), k = Q]}
Because the local definitions of i in A and B are independent,
they (or at least one) must be renamed in A ⊕ B to avoid conflicts.
Also note that f and g in the linked module are mutually recursive,
though no recursion is apparent in A or B alone.
This behavior is like compilation unit linking in C (and indeed,most languages) and is quite different from the asymmetric linking of the ML family’s structures and functors. However, unlike C“modules”, the mixin modules we investigate are first-class, i.e.,they can be stored in data structures, passed as arguments, returned
as results, nested using variables that are in scope, etc., and which
modules are linked may depend on arbitrary run-time computations. In fact, modern programs in C and other languages do dynamically link modules at run-time (sometimes entire libraries thatare also loaded at run-time). However, this is generally outside thelanguage definitions and the type systems do not prevent linking
failures due to missing or multiple definitions for a name. We focus
instead on a strongly typed situation with better static guarantees.
Type analysis is compositional when each program fragment’s
analysis result does not depend on its lexical context. Compositionality simplifies type inference algorithms and helps with issues like
separate compilation and accurate type error reporting. The main
problem in compositional type inference for mixin modules is ensuring that the type system contains principal typings for expressions like λxy.x ⊕ y, which links two unknown modules. In this ex-ample, the type system must not allow modules given as x and y toboth export the same name. But to be compositional, we must analyze λxy.x ⊕ y without any knowledge about its eventual arguments.
The problem for mixin modules is similar to compositional
analysis of calculi with record concatenation. Records are the special case of mixin modules with no imports and no internal recursion, and record concatenation is just a special case of linking mixin
modules. The fundamental problem in analyzing record concatenation turns out to be similar to that for linking mixin modules, although mixin modules have more complications. Record concatenation has been intensively investigated as a potentially useful programming feature and also as one possible way to model objectoriented multiple inheritance. (Note that type inference for record
concatenation is much harder than single-field record extension.)
Our approach to types for mixin modules is inspired in some respects by previous work on type inference for record concatenation.
However, we could not build directly on a type system for record
concatenation, because the most successful such systems use subtyping polymorphism. For technical reasons, we find this undesirable for mixin modules; for example, we would need different typerows for a module’s imports and exports, which is problematic in
our favored family of mixin module calculi where the externallyvisible names of imports and exports use the same namespace.
Thus, while our type system Martini for mixin modules has
some features in common with record concatenation systems, italso exhibits interesting properties of its own which become apparent when it is restricted to work with a λ-calculus with records.
The restriction, which we call Bowtie, does not type as many terms
as some previous systems, but it has some other advantages, among
which is a fast and conceptually simple type inference algorithm,
which runs in almost linear time. In contrast, among record concatenation type inference algorithms with complexity analyses, thenext best runs in cubic time [19].
Along the way to our main goal, we prove that the most obvious
straightforward systems of simple types for mixin modules andrecord concatenation have NP-complete typability problems.
Martini (and its restriction Bowtie) has principal typings [29],which is a precondition for compositional analysis and is alsoneeded for adding Milner’s let-polymorphism. Principal typings
should not be confused with the weaker notion of principal types
which is usually all that remains after let-polymorphyism is added.
Martini is a simple type system that does not yet include polymorphism, which is needed for a serious strongly typed language.
We present the simply typed version Martini first, because the machinery of polymorphism would obscure the novel features that
handle mixin module linking. Sect. 7 shows how to extend Martinito Martini∀ that has Milner’s let-polymorphism, as used in ML andother languages. This ought to be enough to support programmingin-the-small. For programming-in-the-large, further work is neededto add to Martini encapsulation and parameterization capabilities
like those of the ML module language.
Our type inference implementation for Martini can be found at
hURL:http://www.macs.hw.ac.uk/DART/software/Martini/i as a
web application and as source code.

2. Notation
These notations are fairly standard: A function f is a set ofpairs, where we write each pair in the form “a 7→ b”, such that{(a 7→ b), (a 7→ c)} ⊆ f implies b = c. In this section, let f and grange over functions and let A and B range over sets. The domainof f is Dom f = { x | (x 7→ y) ∈ f }. The range of f is Rng f = { y |(x 7→ y) ∈ f }. The inverse of f is f −1 = { x 7→ y | (y 7→ x) ∈ f }.
The expression f (A) is { f (a) | a ∈ A ∩ Dom f } if A ∈/ Dom f .
Composition is given by ( f ◦ g)(x) = f (g(x)). P (A) is the set of

See Section 2 for some essential notation used here, such as· , fin→ , ¢, # , et cetera.
Variables:
x ::= x | y | z | · · ·Field labels: ` ::= f0 | f1 | f2 | · · ·Label sets:
L ∈ Pfin ( ` )→ xExternal parts: E ∈ ` fin
injInternal parts: I ∈ x fin→ M
Values:V ::= {[E;I]}
Terms:
M, N ::= V | x | M ⊕ N | M.` | M \\ L
To be closer to the notation in earlier module calculi, we allow
writing E functions as “`1 . x1 , . . . , `n . xn ” instead of “{`1 7→
x1 , . . . , `n 7→ xn }” and I functions as “y1 = N1 , . . . , yk = Nk ”
instead of “{y1 7→ N1 , . . . , yk 7→ Nk }”.
M ,→ M 0
RC1
M ⊕ N ,→ M 0 ⊕ N
M ,→ N
RCdot
M.` ,→ N.`

N ,→ N 0
RC2
M ⊕ N ,→ M ⊕ N 0
M ,→ N
RChideM \\ L ,→ N \\ L

FV(Rng I1 ) # X 2
X1 # X2FV(Rng I2 ) # X 1
where X i = Rng Ei ∪ (Dom Ii \ Rng E) for i = 1, 2
RLink{[E ¢ E1 ;I1 ]} ⊕ {[E ¢ E2 ;I2 ]} ,→ {[E ¢ E1 ¢ E2 ;I1 ¢ I2 ]}Rng E ⊆ Dom I
S = { x 7→ {[f . x;I]}.f | x ∈ Dom I }RExtract{[E;I]}.` ,→ [S ](I(E(`)))

Dom E1 # L
Dom E2 ⊆ L
Rng E2 ⊆ Dom I
RHide{[E1 ¢ E2 ;I]} \\ L ,→ {[E1 ;I]}
Figure 1. Syntax and semantics of the m-calculus
all subsets of A. The set difference A \ B is { a ∈ A | a 6∈ B }. The
disjoint union A ] B is A ∪ B if A ∩ B = ∅, and undefined otherwise.
These notations are less common: For any metavariable symbol
X, X is the set that X ranges over. Pfin (A) is the set of all finite
subsets of A. The statement A # B abbreviates A ∩ B = ∅. The
expression A fin→ B is the set of all finite functions f ⊆ A × B, andA fin→B is the set of all injective functions in A fin→B. The expression
injf ¢ g means f ∪ g if Dom f # Dom g, and is undefined otherwise.
If X is a set of syntactic entities that can contain (concrete)variables in the set x ⊂ X , then any (partial or total) function ffrom x to X can be used as a substitution. The application of f to
an entier X is defined in the usual way by recursive descent throughX, replacing each variable x by f (x) whenever x ∈ Dom f andrenaming bound variables in X as needed to avoid name capture.
We identify syntactic entities modulo renaming of bound variables.
We sometimes enclose f in square brackets (like [ f ]) in order
to emphasize that it is being used as a substitution. This happens inparticular when f is given by listing its elements, in which case weomit the set braces and write just [x1 7→ X1 , . . . , xn 7→ Xn ].

3. The m-calculus of mixin modules
Our goal is to create a type system with compositional type inference for the simple mixin module calculus defined in Figure 1,
called the m-calculus. Its syntax is essentially isomorphic to that of

the m-calculus of Wells and Vestergaard [31]. The key differenceis a simplified call-by-name semantics, because the more sophisticated semantics (and equational theory) of the m-calculus are irrelevant for the typing issues this paper investigates. Hirschowitz etal. [13] give a similar calculus with a call-by-value semantics. The
m-calculus is in a family of mixin module calculi where imports
and exports share a single namespace; an alternative family withseparate import and export namespaces starts from CMS [4].
The basic construct is a mixin module, written {[E;I]}, whereE (the external part) maps field labels to variables and I (theinternal part) maps variables to terms. The module expression{[`1 . x1 , . . . , `n . xn ; y1 = N1 , . . . , yk = Nk ]} binds all of the variables x1 to xn and y1 to yk within¡S the Ni ’s. Thus
¢ the free variablesof {[E;I]} are FV({[E;I]}) = N∈Rng I FV(N) \ (Rng E ∪ Dom I)
and all other cases of FV(M) just collect free variables componentwise. Each bound name x falls in one of three classes:• (` . x) ∈ E is an import with external name ` and internalname x iff there is no (x = N) ∈ I. When the module is linked
with a module that has an export with name `, references to x in
the Ni ’s become bound to the exported expression.
• (` . x) ∈ E together with (x = N) ∈ I is an export. The exported
expression N can be used from outside via the field extraction
operation M.`, but only once all imports have been satisfied via
linking. Then N will be evaluated in the context of the otherdefinitions in I. The exported term N can satisfy imports of thename ` by other modules via linking. The internal name x can be
mentioned in all of the Ni ’s, and the defined value can thereby
be directly or indirectly recursive.
• (x = N) ∈ I is a local iff there is no (` . x) ∈ E. Local definitions
can be used in all of the Ni ’s. They can be directly or indirectly
recursive, but are not observable outside their containing module except by being referred to by an export.
Field labels (i.e., external names) are fixed, but bound variables(i.e., internal names) are subject to α-conversion (which must keepthem distinct from other bound variables of the same module) andthe actual names of the bound variables are not visible outside themodule expression. We identify α-equivalent terms.
The fundamental mixin operation is linking, written M1 ⊕ M2 .
Its reduction rule RLink is intuitively simple; linking two modules puts their internal parts side by side (choosing appropriate αvariants to avoid wrong name captures), and joins their external
parts. The rule divides each of the two incoming external parts into
a common part E and a separate part Ei . The separate parts are untouched by the linking. The linking happens in the common part E,
containing the labels mentioned by both operands; such labels cannot be in E1 and E2 , because then E1 ¢ E2 would be undefinedon the right-hand side (RHS) of the rule RLink. A label occurring in E maps to the same internal name in both operands; thisis always possible by α-conversion. No label can be exported byboth operands; otherwise I1 ¢ I2 would be undefined on the RHS of
RLink. A label exported by one module and imported by the otheris forced by the common E to have the same internal name (variable) in both operands, so importing variable references in one Ii
can become bound to definitions from the other after the linking.
The premises of RLink ensure that wrong name captures do
not occur. X i is the set of internal names in operand i that do
not participate in the link. The names in X i will be bound on
both sides post-linking, so they must be disjoint from the otherside’s internal names and free variables. For example, the linking{[f . x, g . y; y = x]} ⊕ {[h . z; x = 13, z = x − 6]} (where the common E is empty) does not proceed with the shown α-variants of theoperands because of the premise X 1 # X 2 where both sets contain x.
Without this premise, the result would be a module that (wrongly)
exported 13 as f. To avoid this, the rule forces us to first α-convert
one or both of the x’s. Another example needing α-conversion is{[f . x; x = 42]} ⊕ {[g . y; y = x]} where the x on the left must be
α-renamed to avoid wrongly capturing the (free) x on the right.
The field extraction rule RExtract extracts the export with thegiven label while unfolding into the field body the implicit letrecof the module M to achieve call-by-name semantics. The hiding
operator M \\ L removes exported fields if they exist in the operand.
A hidden export turns into a local because the internal part I is kept
unchanged. If none of the fields in L are exported or imported thehiding is simply a no-op.
It is a run-time error to try to link two modules that both export
the same label `, as well as to try to extract a field from a modulethat does not export it or has imports, or to try to hide an import.
Our task is designing a type system that prevents these errors while
also allowing compositional type inference.
3.1 Syntactic sugar for mixin modules and records
The representation of a mixin module as separate E and I parts isformally convenient in that it allows our type and reduction rules tobe stated relatively compactly. However, it is not very intuitive for
actual programming, so our implementation also supports a morereadable notation (which we have used already in the example in
the introduction):
Values:V ::= · · · | {[γ1 ; . . . ; γk ]}Module groups: γ ::= import `1 . x1 , . . . , `k . xk
| export `1 . x1 = M1 , . . . , `k . xk = Mk
| local x1 = M1 , . . . , xk = Mk
The construct {[γ1 ; . . . ; γk ]} is sugar for{[[γ1 ]E ¢ · · · ¢ [γ k ]E ;[γ1 ]I ¢ · · · ¢ [γ k ]I ]},where[import `1 . x1 , . . . , `k . xk ]E = { `i 7→ xi | 1 ≤ i ≤ k }[export `1 . x1 = M1 , . . . , `k . xk = Mk ]E = { `i 7→ xi | 1 ≤ i ≤ k }[local x1 = M1 , . . . , xk = Mk ]E = ∅[import `1 . x1 , . . . , `k . xk ]I = ∅[export `1 . x1 = M1 , . . . , `k . xk = Mk ]I = { xi 7→ Mi | 1 ≤ i ≤ k }[local x1 = M1 , . . . , xk = Mk ]I = { xi 7→ Mi | 1 ≤ i ≤ k }and where it is required that Rng [γi ]E # Dom [γ j ]I for i 6= j.
(Note that syntactic correctness of the result follows from implicit
constraints imposed by the definition of ¢ and the fact that eachmixin external part E is a bijection.) For additional compactness,“` . x” in import and export groups can be written as just “`” if x
and ` are textually identical (even though they belong to different
namespaces).
We further define a fourth form of module group (distinguishedby its lack of keyword):
γ ::= · · · | `1 = M1 , . . . , `k = Mk ,which is syntactic sugar for “export `1 .y1 = M1 , . . . , `k .yk = Mk ”,
where the yi ’s are chosen fresh. This allows modules that haveneither imports nor local definitions nor internal references to theirown exports to be written with a record-like syntax.
For example, the record-like expression {[f = 5, g = true]}abbreviates {[export f . x = 5, g . y = true]}, which in turn abbreviates {[f . x, g . y; x = 5, y = true]}, which finally abbreviates{[{f 7→ x, g 7→ y};{x 7→ 5, y 7→ true}]}.
3.2 Encoding of the λ-calculus
The reader may wonder how interesting the m-calculus is giventhat its only data constructor is the mixin module. It is natural
to assume that one would need an additional language layer for
manipulating mixin modules programatically. However, this turns
out to be unneeded, because we can encode the λ-calculus using
only mixin constructions. A function λx.M can be represented as

Rows:Σ ∈ ` fin→ τTypes:
τ ::= ’a | ’b | ’c | . . . | {[ Σ / L ]}Environments: Γ ∈ x fin→ τTypings:
T ::= hΓ ` τ i

x : hΓ ` Γ (x)iDom Γ = Rng E ∪ Dom I
I(x) : hΓ0 ¢ Γ ` Γ (x)i for all x ∈ Dom I
L = E −1 (Dom I)(Γ ◦ E) = Σ{[E;I]} : hΓ0 ` {[ Σ / L ]}i

M : hΓ ` {[ Σ / L ]}i
L = Dom ΣM.` : hΓ ` Σ(`)i
L1 # L2
M : hΓ ` {[ Σ ¢ Σ1 / L 1 ]}i
N : hΓ ` {[ Σ ¢ Σ2 / L 2 ]}i
M ⊕ N : hΓ ` {[ Σ ¢ Σ1 ¢ Σ2 / L 1 ∪ L 2 ]}i

M : hΓ ` {[ Σ1 ¢ Σ2 / L ]}i
Dom Σ1 # L 0
Dom Σ2 ⊆ (L 0 ∩ L )M \\ L 0 : hΓ ` {[ Σ1 / (L \ L 0 ) }] i
Figure 2. Riviera: Naive simple types for the m-calculus{[import arg . x; export res . y = M]}, and an application N M as
(N ⊕ {[export arg . y = M]}).res, where arg (argument) and res(result) are globally fixed labels and in both cases we choose y ∈/FV(M). It is easy to see that an application of RLink followed by anumber of RExtract will simulate a β-reduction in the λ-calculus.
This is not a new result [31, 4], but is essential for understanding
how the m-calculus can be used. We will freely use this translation
as syntactic sugar in examples and constructions.
Let λ⊕ denote the fragment of m-calculus that can be written
using only the constructions from the following grammar, some ofwhich use the syntactic sugar for λ-calculus and records:
M ::= λx.M | M N | {[`1 = M1 , . . . , `k = Mk ]} | M1 ⊕ M2 | M.`
We will use λ⊕ when comparing Martini with earlier record concatenation type systems.

4. Riviera: Naive simple types for mixin modules
A natural first attempt at defining a (Curry-style) simple type system for the m-calculus is the naive type system called Riviera
shown in Figure 2. Following [29], we write typing judgements as“M : hΓ ` τ i” rather than using the older convention of “Γ ` M : τ ”.
A Riviera type has the shape {[ Σ / L ]} where L ⊆ Dom Σ, anddenotes a module that exports every label in L and imports every
label in (Dom Σ) \ L , with the types of the exports and imports
given by the row Σ. (In the context of Riviera, a row is just a
finite map from labels to types. Later in our type system Martiniin Section 5 we will consider partially unknown rows, which willuse different metavariables.) Of course, we could equally well havewritten {[Σ1 ⇒ Σ2 ]} where Σ1 and Σ2 partition the field types into
imports and exports, but the {[ Σ / L ]} syntax makes the typing rules
more compact (and we do not intend to actually use Riviera as we
will prove it has unfeasible type inference).
An expression written with the syntactic sugar λx.M defined in
Section 3.2 will always have a type that can be written {[ {arg 7→
τ1 , res 7→ τ2 } / {res} ]}. We will abbreviate such a type τ1 → τ2 .
4.1

Typability in Riviera is NP-hardRiviera can be proven sound (i.e., programs it accepts do not “gowrong”), but that about exhausts its nice formal properties. In

particular, even though it is only at the level of simple types, type
inference is provably hard.
Theorem 4.1. Typability2 for Riviera is NP-complete.
We define the construction that proves this in several stages.
Let M B N abbreviate (λx.N) M, and let M ∼ N abbreviate(λx.(x M) B (x N)) (λy.y), where for both we choose x ∈/ FV(M N).
Lemma 4.2. M B N : hΓ ` τ i iff there exists a type τ 0 such thatboth M : hΓ ` τ 0 i and N : hΓ ` τ i.
Lemma 4.3. M ∼ N : T if and only if M : T and N : T .
Call canonical the following two fixed types: Off = {[ ∅ / ∅ ]}and On = {[ {a 7→¡ {[ ∅ / ∅ ]}} / {a} ]}. Let Nand(x¢ 1 , . . . , xn ) abbreviate λy1 . . . λyn . (y1 ⊕ x1 ).a ⊕ · · · ⊕ (yn ⊕ xn ).a .b.
Lemma 4.4. In an environment that maps each xi to a canonicaltype, Nand(x1 , . . . , xn ) has a type iff the type of some xi is Off.
Let P(x, y) = Nand(x, y) B (x ⊕ y) ∼ (y ⊕ x) ∼ {[a = {[∅]}]}.
Lemma 4.5. P(x, y) has a type exactly in environments where oneof x and y has type Off and the other has type On.
We will be reducing from Boolean formula satisfiability, so leta countable set of Boolean variables P be given, and select a fixed
correspondence that assigns a unique m-calculus variable vP toeach Boolean variable. An environment naturally corresponds toa Boolean valuation for those P such that it assigns vP either typeOn or Off. The corresponding valuation makes P true if vP has typeOn and false if vP has type Off.
Now define a translation from formulae to terms by[P] = λt.λf.P(t, f) B vP ∼ t[¬A ] = λt.λf.[A ] f t[A ∨ B ] = λt.λf.λt1 .λf1 .λt2 .λf2 .
P(t, f) B [A ] t1 f1 B [B ] t2 f2 B
Nand(t1 , f) B Nand(t2 , f) B Nand(t, f1 , f2 )[A ∧ B ] = [¬(¬A ∨ ¬B )]Lemma 4.6. [A ] has a type exactly in environments that correspond to valuations for A ’s variables. The types of [A ] in such anenvironment have the shape On → Off → τ if A is true under thecorresponding valuation and Off → On → τ if A is false. (Theremay be one or more τ ’s that can appear in a valid type for [A ].)Proof. By a straightforward induction over the structure of A .
Proof of Theorem 4.1. It is clear that typability is in NP; given an
oracle which tells for each variable which fields its type imports
and exports, type inference is like for the simply typed λ-calculus.
For NP-hardness, we reduce from satisfiability of arbitrary
Boolean formulae. A formula A is satisfiable exactly if the term
MA = [A ] t f B Nand(f) is Riviera-typable. It follows from Lemma 4.6 that any typing for MA implies a satisfying truth assignment
for A . Conversely, any satisfying truth assignment corresponds toan environment Γ such that [A ] : hΓ ` On → Off → τ i for someτ . From there one easily gets MA : hΓ , t : On, f : Off ` τ i.
4.2 Asymmetric variants
In a calculus with asymmetric linking, M ⊕ N succeeds even when
M and N both define some label `, in which case the result will use
the definition from N. One can construct a Riviera-like type system
RivieraA for such a calculus by replacing the ⊕ typing rule with:
2 Typability means deciding for a given term M whether there exists a typing
T such that M : T . Note that specifying the Γ part of T would not make theproblem easier: one can just abstract over M’s free variables and set Γ = ∅.

Dom Σ11 = L 1 ∩ L 2
M : hΓ ` {[ Σ ¢ Σ1 ¢ Σ11 / L 1 ]}i
N : hΓ ` {[ Σ ¢ Σ2 / L 2 ]}i
M ⊕ N : hΓ ` {[ Σ ¢ Σ1 ¢ Σ2 / L 1 ∪ L 2 ]}i
Another possible variant of linking allows asymmetric linking,but requires that a field that is defined in both linked modules
must have the same type even though at run-time one of them is
discarded. This gives rise to a Riviera variant with this linking rule:M : hΓ ` {[ Σ ¢ Σ1 / L 1 ]}i
N : hΓ ` {[ Σ ¢ Σ2 / L 2 ]}i
M ⊕ N : hΓ ` {[ Σ ¢ Σ1 ¢ Σ2 / L 1 ∪ L 2 ]}i
We call this variant join-like, and name it RivieraJ , because thetype behavior of this rule is identical to the type-level behavior of
the join operator on in relational algebras [15, 25]. It is not common
for modules or records (an exception is the Church-style calculusof [32]), but we mention it to highlight the similarities between
type problems in relational calculi and in calculi with concatenationand linking. Further, the simplest variation of our system Martini(introduced later in Section 5) which allows overwriting linking
would have a join-like typing rule.
Theorem 4.7. Typability for RivieraA and RivieraJ is NP-complete.
The proof for Theorem 4.1 has been constructed to work verbatim for RivieraA and RivieraJ . (This does make it more complex,
however. Simpler constructions for Riviera and RivieraA can befound in the long version of this paper [14]).
4.3

Other calculi

Riviera is very similar to Typed CMS as defined by Ancona andZucca [4], except that Typed CMS is a Church-style system withmandatory type annotations in terms. There are also minor differences, such that the fact the CMS has different namespaces forimport and export labels, and uses a special “freeze” operator toconnect imports with exports. However, the proof of Theorem 4.1
does not use imports at all, except in the syntactic sugar for translating λ abstractions. If one uses the λ translation for CMS (definedin [4]), our proof directly yields NP-completeness of typability in
the Curry-style variant of Typed CMS (i.e., Typed CMS with type
annotations removed), a previously unknown result.
We believe our proof of NP-completeness of typability can also
be adapted to the implicitly typed systems CMSv [12], MM [13]and Mix [11], although we have not checked this formally.
If one restricts RivieraA to (asymmetric) λ⊕ , one gets a typesystem equivalent to Wand’s type system for record concatenation [28]. Because the proof of Theorem 4.1 uses only the λ⊕ fragment of the m-calculus, we get as a bonus result a direct proof of
the folk belief that typability in Wand’s system is NP-hard.
4.4

Discussion

NP-completeness may not sound bad when one compares it to thefamiliar result that typability for the Hindley/Milner type system
is DEXPTIME-complete. However, it should be kept in mind that
Riviera is a simply typed system where polymorphism has yet tobe added. Thus the proper comparison would be the simply typed
λ-calculus, where typability is almost linear (i.e., O(n α(n))).
Our result suggests that type inference for mixin modules is
hard independently of the details of the calculus. A feasible typesystem for mixin modules (or record concatenation) must introduce
complications that are not aimed solely at strengthening the typesystem itself (in the sense of enlarging the set of typable programs)
but serve to make type inference a tractable problem.
A related result was achieved by Palsberg and Zhao [16], whoprove NP-completeness of typability for a typed object calculus with symmetric record concatenation and subtyping. It is notclear to us whether this proof can be easily adapted to recordconcatenation type systems without subtyping. Vansummeren [25]proved NP-completenes of typability in various fragments of anaively typed relational algebra. Ohori and Buneman [15] proved
NP-completeness of typability in a lambda calculus with primitive
sets of records and join operator. Their system is defined in termsof constraints, but appears to be equivalent in expressive power toa RivieraJ -like type system.

5. Martini: A better type system for mixin
modulesFigure 3 show our type system Martini for the m-calculus. It is designed to simultaneously reach two goals in addition to the usual
basic safety. (1) It should have feasible type inference. (2) It shouldhave principal typings [29], which are needed to express intermediate results in a compositional inference algorithm using Martini’s
own type language. Also, principal typings allow adding Milner’s
let-polymorphism (as we do in Section 7).
A mixin module type in Martini has the shape {[ R / Q ⇒S ]},where Q represents the set of import labels and S represents theset of export labels. The row R gives the type of both inputs andoutputs, like Σ in Riviera; however a Martini row may define types
for fields that the module neither imports nor exports.
For example, given obvious extensions with integers and booleans, the term M = {[f . x, g . y; x = y > 5]} has the typing h∅ `{[ f:bool, g:int, r / {g} ⇒{f} ]} | ∅i (r is a row variable whoserole will be described shortly). This is also a typing for N = {[f . x;
x = true]}, even though N does not import g — it is allowed for a
Q to overapproximate the true set of imports. This allows constructions such as if · · · then M else N to be typed without requiring adummy import of g in N.
In Riviera it was essentially an arbitrary choice to use a single
row for imports as well as exports. In contrast, the same decisionin Martini is essential for our type inference strategy. In order tofacilitate type inference with principal typings, the three parts R, Q
and S of a mixin type {[ R / Q⇒S ]} have a more elaborate internal
structure than the monolithic Σ and L of Riviera — in particular,
each part can be a variable.
Wand [26] introduced row variables for manipulating partial
knowledge about mappings from field labels to types. Using thesame row variable at the end of different row expressions can
express that the two rows agree at some but not all labels, as
happens in the rule THide. Adding more fields to the row partof a module type does not change the type’s meaning if the set
expression part stays the same. Therefore Martini needs no syntax
for an “empty row”; a row variable can always be used for this.
Typings now contain constraint sets, which assert relations between label sets that are not known yet. As a concrete example, theterm {[import f . x, g . y; h = x ⊕ y]} has the Martini typing* +
f:{[ r / q1⇒s1 ]},s3 = s1 ] s2,/ {f, g}⇒{h} ]} q3 ⊇ q1 \ s2, .
` {[ g:{[ r / q2⇒s2 ]},h:{[ r / q3⇒s3 ]}, r0q3 ⊇ q2 \ s1
The recurrence of r in all three field types means that if one of theimports contains a field ` at all, its type must be the same as that
expected for ` in the result. The constraint s3 = s1 ] s2 says thatevery field defined in the result must be defined in exactly one of
the arguments. This particular typing is not principal; Martini also
allows the term to have the type {[ · · · / {f, g, k}⇒{h} ]} even though
it does not import k. A principal typing for the term would have{[ · · · / q⇒{h} ]} as its type part and an extra constraint q ⊇ {f, g}.
Martini’s strategy for escaping the NP-hardness of Riviera is toconsider the constraint s3 = s1 ] s2 “good” for as long as we haveno information about s1 or s2, regardless of whether information

Type variables:
α ::= ’a | ’b | ’c | . . .
Row variables:r ::= r0 | r1 | r2 | · · ·Import set variables:
q ::= q0 | q1 | q2 | · · ·Export set variables:s ::= s0 | s1 | s2 | · · ·Type rows:
R ::= r | `:τ , R
Import set expressions: Q ::= q | L
Export set expressions: S ::= s | L | ⊥Types:
τ ::= α | {[ R / Q⇒S ]}Environments: Γ ∈ x fin→ τConstraints:
c ::= S = S1 ] S2 | S = S1 \ L| Q ⊇ Q1 \ S | Q # L
Const. sets:
C ∈ Pfin ( c )Typings:
T ::= hΓ ` τ | Ci

We forbid as ill-formed rows that define any label ` more than once and we consider types (etc.) modulo this row structure equation:(`1 :τ1 , `2 :τ2 , R) = (`2 :τ2 , `1 :τ1 , R)
when `1 6= `2→ τ , let Σ • R abbreviate `1 :τ1 , . . . , `n :τn , R.
For Σ = {`1 7→ τ1 , . . . , `n 7→ τn } ∈ ` fin
Let S1 = S2 , Q1 ⊇ Q2 , and Q ⊆ S abbreviate the constraints S1 = S2 ] ∅, Q1 ⊇ Q2 \ ∅, and ∅ ⊇ Q \ S, respectively.
We allow omitting the set braces around concrete environments and constraint sets in typings.
Let T range over type substitutions, which are functions that map q to Q , s to S , r to R , and α to τ , such that only finitely
many variables do not map to themselves. Type substitutions are extended componentwise to map each of the classes Q , S , R , τ ,Γ , c , C , and T to itself.
A constraint c is solved, written ° c, iff either c is a true statement of set theory (L = L 1 ] L 2 is true iff L = L 1 ∪ L 2 and L 1 # L 2 )or c contains ⊥ to the right of the relation sign (that is, to the right of =, ∈, or ⊇).
Let °C abbreviate ∀c ∈ C : ° c, and let C1 ° C2 abbreviate ∀T : ° T (C1 ) ⇒ ° T (C2 ).
Write τ1 ≈ τ2 iff τ1 and τ2 are identical except for import and export set expressions.
Let C ° τ1 = τ2 abbreviate τ1 ≈ τ2 ∧ ∀T : ° T (C) ⇒ T (τ1 ) = T (τ2 ) .
Let C ° Γ1 = Γ2 mean that Dom Γ1 = Dom Γ2 and C ° Γ1 (x) = Γ2 (x) for x ∈ Dom Γ1 .
Dom Γ = Rng E ∪ Dom I
I(x) : hΓ0 ¢ Γ ` Γ (x) | Ci for all x ∈ Dom I
L = E −1 (Dom I)
L 0 = Dom E \ L
C ° {Q ⊇ L 0 , S = L }TMixin{[E;I]} : hΓ0 ` {[ (Γ ◦ E) • R / Q⇒S ]} | Ci

C ° Γ (x) = τTVarx : hΓ ` τ | Ci

M : hΓ ` {[ R / Q1 ⇒S1 ]} | Ci
N : hΓ ` {[ R / Q2 ⇒S2 ]} | Ci
C ° {Q ⊇ Q1 \ S2 , S = S1 ] S2 , Q ⊇ Q2 \ S1 }TLink
M ⊕ N : hΓ ` {[ R / Q⇒S ]} | Ci
Dom Σ1 = Dom Σ2 = L

M : hΓ ` {[ `:τ , R / ∅ ⇒S ]} | Ci
C ° {{`} ⊆ S}
TExtractM.` : hΓ ` τ | Ci

M : hΓ ` {[ Σ1 • R / Q⇒S1 ]} | Ci
M \\ L : hΓ ` {[ Σ2 • R / Q⇒S2 ]} | Ci

C ° {Q # L , S2 = S1 \ L }THide

Figure 3. Our type system Martini for the m-calculus
about s3 shows up later. Thus, e.g., λx.(x ⊕ x).f is typable in Martini even though there is no value that it can safely be applied to.
This is still sound, as Martini will reject attempts to actually call it.
Thus, Martini does not reject some nonsensical (but dynamicallysafe) programs as type errors, but also escapes NP-hardness oftypability. Theorem 4.1 depends on being able to ask the typesystem: “Can any possible call to this function be proved errorfree?”. Martini refuses to answer until we refine the question to“Will this particular call be error-free?”.
The term λx.(x ⊕ x).f has a principal typing with the shapeh∅ ` {[ arg:{[ f:’a, r / q ⇒s ]}, res:’a, r0 / q0 ⇒{res} ]} | s1 =s ] s, {f} ⊆ s1, . . .i. This typing is “good” because we can solve its
constraint set by substituting the special set expression ⊥ for eachof s and s1. This is the role of ⊥; it allows a constraint to be solved
as long as we have no evidence that a use of the linking or field
extraction operation that the constraint corresponds to will actually
go wrong at run-time. Principal typings never need to contain ⊥.
Effectively, {[ R / Q ⇒⊥ ]} is a type that describes no values at all.
An expression with such a type must be either dead (its result will
never be used, perhaps because its evaluation diverges) or sleeping(its result will not be used unless the program is put into a larger

context). Martini accepts mistakes in dead or sleeping code that are
hard to check for until a concrete calling context is provided, but it
still rejects mistakes that are easy to find in dead or sleeping code.
Now return to the typing for {[import f . x, g . y; h = x ⊕ y]}and consider its triple occurrence of r. Because r appears in thearguments as well as in the result, Martini can begin to resolve
their connection before enough information to solve the constraint
arrives. This lets some internal errors in sleeping code be caught
early and also gives more readable principal typings by expressing more relations between types without constraints. However,some strength is sacrificed: Each module type must contain the field
types of any module it may be linked with. (The programmer need
not write them as they will be inferred.) Thus Martini will reject,for example, λx.{[a = x ⊕ {[f = 5]}, b = x ⊕ {[f = true]}]}, because
the type of x must predict a single type for f in all of its descendants. One way to mitigate this row pollution problem is to use
let-polymorphism (Section 7) instead of λ to bind x, to allow polymorphism in the type of f. Another is to insert dummy hiding operators: λx.{[a = x \\ {f} ⊕ {[f = 5]}, b = x \\ {f} ⊕ {[f = true]}]} is typable. Since this solution depends on guessing which fields will bedefined by the other operand to ⊕, it cannot be applied fully automatically; it can be considered a programmer-supplied typing hint.
5.1

Soundness

Proving type soundness for Martini proceeds as usual, except forthe details of handling constraint sets.
Lemma 5.1 (weakening). Assume M : hΓ ` τ | Ci. For any C0 ° C
and Γ 0 ⊇ Γ it holds that M : hΓ 0 ` τ | C0 i.
A constraint set C is solvable iff ° T (C) for some substitution
T . A typing is called solvable iff its constraint set component is.
Lemma 5.2. Assume C ° τ1 = τ2 and C ° Γ1 = Γ2 . Then M : hΓ1 `τ1 | Ci implies M : hΓ2 ` τ2 | Ci.
Lemma 5.3 (substitution). If M : T , then M : T (T ).
Assume M : hΓ ¢ {x 7→ τ 0 } `Lemma 5.4 (term substitution).
τ | Ci and N : h∅ ` τ 0 | Ci. Then [x 7→ N]M : hΓ ` τ | Ci.

Theorem 5.5 (subject reduction). If M ,→ N and M : h∅ ` τ | Ci
for solvable C, then N : h∅ ` τ | Ci.
Theorem 5.6 (progress). If M : h∅ ` τ | Ci for solvable C, theneither M is a value or M ,→ N for some N.
Theorem 5.7 (type soundness). Programs (closed terms) withsolvable typings do not get stuck.
5.2

Testing constraint set solvability

To make Thm. 5.7 useful, this section develops an algorithm toidentify solvable constraint sets.
Define the relation C ☞ T by:
1. ∀C, s, L 1 , L 2 : C ∪ {s = L 1 ] L 2 } ☞ [s 7→ (L 1 ∪ L 2 )] if L 1 # L 2 ,2. ∀C, s, L 1 , L 2 : C ∪ {s = L 1 \ L 2 } ☞ [s 7→ (L 1 \ L 2 )].
Lemma 5.8. If C ☞ T , then C is solvable if and only if T (C)is.
Lemma 5.9. Assume that there is no T such that C ☞ T , and let T 0
map every export set variable in C to ⊥ (and every other variable
to itself). Then C is solvable if and only if T 0 (C) is.
Proof. The “if” direction is obvious. For “only if”, assume that
C is solved by some T 1 . We claim that T 1 also solves T 0 (C).
For otherwise there would be a c ∈ C such that T 1 (c) is solved
but T 1 (T 0 (c)) is not. Their only difference is that T 1 (T 0 (c)) may
contain ⊥ in a place where T 1 (c) has another (input) set expression.
The only place ⊥ can appear without solving T 1 (T 0 (c)) is to the leftof “=”, so c must have the form s = L 1 \ L 2 or s = L 1 ] L 2 (where in
the latter case L 1 and L 2 must be disjoint, because T 1 (c) is solved).
But in either of these two cases we could find a T such that C ☞ T ,contradicting the assumption.
For any constraint set C and any ` that occurs in C, let QC` be
the least subset of q such that
1. When (q ⊇ L 1 \ L 2 ) ∈ C with ` ∈ (L 1 \ L 2 ), then q ∈ QC` , and
2. When (q2 ⊇ q1 \ L ) ∈ C with ` 6∈ L , then q1 ∈ QC` ⇒ q2 ∈ QC` .
Computing QC` for a given C and ` is a simple O(n) graph reachability problem. The intended intuition is that QC` is “the set of q’s
that ` can reach according to C” and { ` | q ∈ QC` } is a lower boundon the possible values of q in all ground solutions of C. Let C ☛ T
hold when T (q) = { ` | q ∈ QC` } for all q mentioned in C and T
maps all other variables to themselves.
Lemma 5.10. If C ☛ T and C is solvable and free of export set
variables, then T (C) is solved.

Proof. Because C is assumed solvable, any constraint in C that does
not contain at least one q variable must be solved already, and cantherefore be ignored. Constraints of the form Q2 ⊇ Q1 \ ⊥ are also
solved, so the only constraints we need to consider are those of theforms Q2 ⊇ Q1 \ L and Q # L .
Given an arbitrary T 0 that solves C, whenever q ∈ QC` it must
hold that ` ∈ T 0 (q); this follows directly from the inductive construction of QC` . Also, if we let T `0 (q) be T 0 (q) \ {`} for q 6∈ QC`
and T 0 (q) otherwise, then T `0 still solves C — it would contradict
the construction of QC` if this change caused an unsolved constraint
to appear. Now, if any solution to C exists at all, then T is also asolution, because an arbitrary solution can be transformed into T
label for label by the preceding remarks.
Theorem 5.11. Constraint sets can be tested for solvability in timeO(nm), where n is the number of constraints and m is the numberof distinct labels in the constraints.
Proof. The testing procedure consists of first rewriting as much as
possible by Lemma 5.8, and then eliminating the remaining export
set variables by Lemma 5.9. The constraint set now contains only q
variables, and solvability can therefore be decided by Lemma 5.10.
Complexity bound: In the Lemma 5.8 phase, each constraint
is processed at most four times: Once to see if it can be rewritten
immediately, up to twice when set variables on its left-hand side are
instantiated, and once to check whether T (c) is solved. If L ’s are
represented as bit vectors, each visit of the constraint takes O(m)time. Lemma 5.9 can obviously be completed in time O(n). For
Lemma 5.10, the QC` ’s and T can be straightforwardly constructed
in time O(mn); checking ° T (C) takes O(mn) time.
5.3 Type inference
Define the relation v between typings by: hΓ1 ` τ1 | C1 i v
hΓ2 ` τ2 | C2 i iff there exists a type substitution T and Γ20 ⊆ Γ2such that C2 ° Γ20 = T (Γ1 ) and C2 ° τ2 = T (τ1 ) and C2 ° T (C1 ).
Lemma 5.12. If M : T1 and T1 v T2 , then M : T2 .
Let T ≤ T 0 (T is “at least as precise as” T 0 ) mean M : T ⇒ M : T 0
for all M. A typing T is principal [29] for M iff M : T and
M : T 0 ⇒ T ≤ T 0 for all T 0 . A typing T is syntactically principal
for M iff M : T and M : T 0 ⇒ T v T 0 for all T 0 . Because T v T 0
implies T ≤ T 0 , a syntactically principal typing for M is principal.
The definitions directly imply that if T1 v T2 and T2 is solvable,
then T1 is also solvable. Therefore a syntactically principal typing
for a term M is solvable unless M has no solvable typings at all.
Theorem 5.13. The algorithm TYPEINF defined in Figure 4 computes a syntactically principal typing for every typable term. The
algorithm runs in time O(nm α(n)) where n is the size of the analyzed term and m is the number of distinct field labels in it.
As a corollary, Martini has principal typings.
Before we prove the theorem, here are some high-level remarks
about the algorithm. In our description it consists of two phases.
The COLLECT phase processes the input term to collect type equations and constraints; the RUNIFY phase solves the type equations
by a unification algorithm extended to deal with rows. The collected constraints are not touched (except for the side effects of theunification step); they appear directly in the principal typing. Implementations will usually perform the two phases in parallel as
co-processes, and check constraint solvability using Thm. 5.11 afterward; we leave such refinements to the reader’s imagination.
The recursive syntax-directed COLLECT phase takes two inputs: a term M and a type environment Γ that maps all of
M’s free variables to distinct type variables. It produces a triple
COLLECT(M, Γ ) = (W, τ ,C), where W is a set of type equations

COLLECT(x, Γ ) = (∅, Γ (x), ∅)COLLECT({[E;I]}, Γ ) =let X = Rng E ∪ Dom I ;let L = E −1 (Dom I) and L 0 = Dom E \ L ;let r, q, s, and αx for each x ∈ X be fresh;let Γ 0 (x) be αx for x ∈ X , and Γ (x) otherwise;0let (Wx , τx ,Cx ) = COLLECT(I(x),¡¢Γ ) for all x ∈ Dom I;
S
let W = x∈Dom I Wx ∪ {τx = αx } ;let Σ = { ` 7→ Γ 0 (E(`))S| ` ∈ Dom E }in (W, {[ Σ • r / q⇒s ]}, x∈Dom I Cx ∪ {q ⊇ L 0 , s = L }).
COLLECT(M1 ⊕ M2 , Γ ) =let r, q, q1 , q2 , s, s1 , and s2 be fresh;let (Wi , τi ,Ci ) = COLLECT(Mi , Γ ) for i ∈ {1, 2};
let C = C1 ∪C2 ∪ {q ⊇ q1 \ s2 , s = s1 ] s2 , q ⊇ q2 \ s1 };let W = W1 ∪W2 ∪ {τ1 = {[ r / q1 ⇒s1 ]}, τ2 = {[ r / q2 ⇒s2 ]}}in (W, {[ r / q⇒s ]},C).
COLLECT(M.`, Γ ) =let α, r, s be fresh;let (W, τ ,C) = COLLECT(M, Γ )in (W ∪ {τ = {[ `:α, r / ∅ ⇒s ]}}, α,C ∪ {{`} ⊆ s}).
COLLECT(M \\ L , Γ ) =let r, q, s0 , s, and α` and α`0 for each ` ∈ L be fresh;let Σ0 = { ` 7→ α`0 | ` ∈ L } and Σ = { ` 7→ α` | ` ∈ L };let (W, τ ,C) = COLLECT(N, Γ );let W 0 = W ∪ {τ = {[ Σ0 • r / q⇒s0 ]}}in (W 0 , {[ Σ • r / q⇒s ]},C ∪ {q # L , s = s0 \ L }).
TYPEINF(M) =let Γ map each free variable of M to a fresh type variable;let (W, τ ,C) = COLLECT(M, Γ );let T = RUNIFY(W )in hT (Γ ) ` T (τ ) | T (C)i.

ing the type variable name Γ (x) from the name of x. However, thisdoes not work in practice, where type variables are represented byheap-allocated union-find elements to facilitate unification.
A unifier for a type equation set W is a type substitution T suchthat every equation in T (W ) is an identity (remembering that types
are already identified modulo the row structure equation).
Lemma 5.15. Assume that (W, τ ,C) = COLLECT(M, Γ ) whereΓ maps each free variable in M to a unique type variable. Let
T = hΓ ` τ | Ci. For each unifier T for W , it holds that M : T (T ).
Conversely, whenever M : T 0 , it holds that there is a unifier T for
W such that T (T ) v T 0 .
Lemma 5.16. COLLECT(M, Γ ) can be computed in time linear
in the size of M.
Proof. The only parts of the computation for which this is not
obviously the case are lookups and additions in Γ . If we represent
Γ as a trie, the operations are all linear in the length of the variable
name, so the total time spent here is linear in the size of M.4
A most general unifier (MGU) for W is a unifier T for W suchthat every other unifier for W can be written as T 0 ◦ T for some T .
The second phase of type inference computes an MGU of the final
equation set W . Section 6 will construct a function RUNIFY suchthat RUNIFY(W ) computes one of the MGUs of W , if it has any,in time O(nm α(n)), where n is the size of W and m is the numberof distinct field labels mentioned in W .
Proof of Thm. 5.13. The correctness of the result of TYPINF follows from Lemma 5.15 and the property that RUNIFY computes
most general unifiers.
According to Lemma 5.16, the COLLECT phase completes intime O(n), so the size of W is O(n) too. Therefore, the computation(and, implicitly, application) of MGU(W ) can be completed in timeO(nm α(n)) — a detailed argument for this will be given in Section
6. Thus the entire computation has complexity O(nm α(n)).
5.4 Incremental constraint simplification

Figure 4. The definition of the type inference algorithm. The subalgorithm RUNIFY(W ) will be defined in Section 6.
(of the form τ1 = τ2 ), τ is a type expression, and C is a constraint set. Note that the input Γ is only used to map term variables
to type variables (not arbitrary types) and it is never changed by
COLLECT, although the equations in the produced W may giverise to substitutions for the type variables in Dom Γ later.
R EMARK 5.14. In a strictly compositional inference algorithm, thetype environment Γ should be an output instead of an input. However, computing the principal environment for any subexpression
bottom-up will incur possibly large reconciliation costs when theprincipal environments for two sibling expressions meet each other,and would therefore destroy the advertised O(nm α(n)) complexity.
The best type inference solution that we could find that produced
Γ only as output had complexity O(n log n + nm α(n)) (which isworse when m is small), but even that depended (as our current
algorithm does) on a mutable union-find data structure shared by
all the subcomputations.3 One possible solution could be to startby α-renaming all variables away from each other and then deriv3 Incidentally, this suggests that a consistently compositional type inference algorithm cannot achieve the folklore O(n α(n)) behavior on programs
where the number of free variables in a subexpression may be large. However, that is not a real problem; the main point of compositional inference isthat the analysis can be broken at any point in the expression tree, but there
is no obligation to actually break the analysis at every point.

Superficially, it seems that we have solved type analysis for Martini. To analyze a term, one computes its principal typing (Thm. 5.13)
and then checks whether its constraint part is solvable (Thm. 5.11).
Each step is efficient and relatively simple. So are we happy?
Not entirely. Postponing constraint solving until the end has
practical and theoretical disadvantages. One problem is that theconstraint parts of the inferred typings can grow quite large, because they can track each module operation in the term, even thosethat are irrelevant for observable behavior. For example, the term({[f = 5]} ⊕ {[]}).f gets the inferred typing h∅ ` int | s = {f}, {f} ⊆si rather than the more concise h∅ ` int | ∅i — which, incidentally, is also syntactically principal for it.
Instead, we want to interleave the constraint solving (Section
5.2) with other type inference steps. But we must be a little careful;if we blindly applied the entire constraint solving procedure from
4 A reader of early drafts of this explanation complained that this assumes

that variable names are represented with a fixed finite alphabet in the input,
whereas the rest of our complexity analysis assumes a constant-cost RAM
with a word length that expands with the input size such that all partsof the input can be addressed. The reader complained that it was not fair
not to allow the representation of variable names to take advantage of thisincreasing word length, and that the complexity bounds ought to include alogarithmic factor to take account of this. We disagree with this objection;
we believe it is a common convention in complexity theory to measure the“size of the input” in bits even when one is working with a cost model
where internal operations can work with larger pieces of data at once. Thismeans we are measuring our algorithm the same way other algorithms in
the literature are measured, so comparisons will be meaningful.

Section 5.2, a simple term such as x.f would get its original principal typing hx : {[ f:’a, r / q⇒s ]} ` ’a | {f} ⊆ s, ∅ ⊇ qi rewritten
to hx : {[ f:’a, r / ∅⇒⊥ ]} ` ’a | ∅i which is far from principal. To
preserve principality we must make sure that whenever we rewrite
T to T 0 it holds that T v T 0 and T 0 v T , in which case we say it issafe to rewrite T to T 0 . In this section we identify some rewritings
that are safe.
First, constraints that are already solved can be dropped:
Lemma 5.17. Let T = hΓ ` τ | Ci and T 0 = hΓ ` τ | { c ∈ C |¬ ° c }i. Then it is safe to rewrite T to T 0 .
Second, it is safe to perform the ⊥-less solving of s variables
described by Lemma 5.8:
Lemma 5.18. Let T = hΓ ` τ | Ci and assume C ☞ T . Then it issafe to rewrite T to T (T ).
The construction in Lemma 5.9 is not safe. The one in Lemma
5.10 is only partially safe; C ☛ T sets all q’s to a lower bound on
the possible values of q. We should only use this lower bound whenthat entails no restriction on set variables that are visible in thetype and environment parts of the typing. We should also exclude
variables where the lower bound cannot yet be computed because
the S part of a Q ⊇ Q \ S constraint is still a variable.
Lemma 5.19. Let T = hΓ ` τ | Ci, and let Q be the least subsetof q such that
1. If q appears anywhere in Γ or τ , then q ∈ Q.
2. If (q ⊇ Q \ s) ∈ C, then q ∈ Q.
3. If (q ⊇ q0 \ L ) ∈ C then q0 ∈ Q ⇒ q ∈ Q.
Let C ☛ T , and let T 0 (q) be T (q) when q 6∈ Q and q otherwise.
Then it is safe to rewrite T to T 0 (T ).
As a simple example of incremental constraint simplification,
consider the term (x ⊕ {[f . y, h . z;y = z]}).g. Its inferred but not
simplified typing is hx : {[ f:’a, g:’b, h:’a, r / q ⇒s ]} ` ’b | Ci
where
½
¾
q1 ⊇ {h}, s1 = {f}, ∅ ⊇ q1 \ s,C=
s2 = s ] s1, ∅ ⊇ q \ s1, {g} ⊆ s2
We first reduce for s variables by Lemma 5.8. The only reductionin this case is C ☞ [s1 7→ {f}]; after this we have the same typing
but with constraint set¾½
q1 ⊇ {h}, {f} = {f}, ∅ ⊇ q1 \ s,C0 =s2 = s ] {f}, ∅ ⊇ q \ {f}, {g} ⊆ s2
0

We now compute the various QC` ’s and get C0 ☛ [q 7→ ∅, q1 7→{h}]. In Lemma 5.19, Q is {q} (as q appears in the type assumption
for x), so we apply just the substitution [q1 7→ {h}] to get¾½{h} ⊇ {h}, {f} = {f}, ∅ ⊇ {h} \ s,C00 =s2 = s ] {f}, ∅ ⊇ q \ {f}, {g} ⊆ s2
After dropping solved constraints and using abbreviations for theunsolved ones, we get the simplified typing¿µ¶À
f:’a, g:’b,{h} ⊆ s, s2 = s ] {f},x : {[/ q⇒s ]} ` ’bh:’a, rq ⊆ {f}, {g} ⊆ s2
5.5

Discussion

Martini allows compositional type inference for mixin modules
without type annotations. Previous typed mixin module calculi[7, 4, 1, 12, 13] have not considered type inference, and several
expect full type annotations for difficult operations. Because of
the row pollution problem, Martini sometimes fails to type someterms unless the programmer switches to let-polymorphism (notalways possible) or inserts dummy hiding operations. In contrast,
previous mixin module systems tend to need full type annotations

for these problem terms. Also, as Section 4.4 points out, the naive
approach of previous type systems leads to unfeasible NP-complete
typability in the absence of full type annotations.
Some previous mixin calculi have features not supported by
the m-calculus or Martini. Duggan and Sourelis [5] allow different
cases of a function that operates by pattern matching to come fromdifferent modules. Ancona et al. [2] allow extracting an export froma mixin module with imports, if the types prove that the export does
not depend on the imports.
If we restrict Martini to the λ⊕ fragment of the m-calculus that
we defined in Section 3.2, we can derive a type system for the λcalculus with record concatenation. We call this system Bowtie; itarises by adding a primitive type constructor → for function types
and then fixing the Q part of all remaining record types to ∅.
Our entire development for Martini, including the type inference algorithm and its complexity analysis, carries over to Bowtie
without change (except that of course constraint solving for q variables can be omitted).
Bowtie is not the first type system for a λ-calculus with record
concatenation that supports type inference, but to the best of ourknowledge there are no previous systems with a published typeinference complexity bound as low as O(nm α(n)). One system
by Rémy [21] can probably be implemented within this bound;
unfortunately the types in this system are excessively inflexible andit can not reasonably be used for programming. A series of systems
have been defined by Pottier [17, 18, 19], but the only one of thesethat has a complexity analysis [19] has complexity O(n3 m log m),which is significantly more than Bowtie’s O(nm α(n)).
Previous type systems for record concatenation include work by
Wand [27, 28], Harper and Pierce [8, 9], Rémy [21, 23], Zwanenburg [32], Pottier [17, 18, 19], and Palsberg and Zhao [16]. Rémy’s
system in [23] is the earliest to tolerate type “errors” in dead andsleeping code. The Bot concept in Pottier’s system in [17] is very
similar to the “⊥” in Bowtie (and Martini).

6. Row unification
In this section we describe an efficient algorithm for computing
most general unifiers modulo the row structure equation (`1 :τ1 ,`2 :τ2 , R) = (`2 :τ2 , `1 :τ1 , R). This is used in our type inference
procedure, but we also believe it has some general interest. Thisrow unification problem has a standard algorithm (see for example [20]), but a direct implementation of this is too slow to fit within
the O(nm α(n)) complexity we need. The more efficient procedure
we define here may have been independently developed by many
implementers, but appears never to have been written down explicitly. We think it deserves to be recorded.
The key idea is to handle an entire row equation (`1 :τ1 ,. . . , `k :τk , r) = (`01 :τ10 , . . . , `0k0 :τk0 0 , r0 ) in a single step. Whenever`i = `0j , a unification of τi = τ 0j must be scheduled; labels that appear only on one side must have corresponding entries added tothe end of the list of the other side. The standard algorithm uses upto Ω(m2 ) label commutation steps to bring the elements on eitherside of the equation into the same order. This corresponds to linear
searches through the two row expressions; with a monolithic solution we are free to use more efficient data structures such a searchtrees or arrays for this purpose.
The only point where our algorithm differs from an implementation of the standard algorithm for row unification is in steps (b)and (c) of the RECUNIF operation in Figure 6. We describe the algorithm at a more concrete level than most unification descriptionsin the literature. It is usual for such description to allow wholesale
manipulation of type terms and substitutions; but working at thatlevel would reduce our complexity analysis to pure handwaving.

6.1

Data representation

During row unification (and type inference in general) labels will
be represented as small integers between 1 and m, the numberof distinct labels in the program. This allows representing labelindexed maps as arrays. In the original input labels are usuallystrings that must be interned to small integers before type inference;
this can be done in a linear-time pass over the program using a trie
recording indexes for already-seen labels.
In the algorithm type expressions are represented as a directed acyclic graph of pointer-linked memory blocks. We use themetavariable X for pointers to nodes in the type graph. Each node
has a sort from the set {TYPE, ROW, QSET, SSET}, corresponding to the syntactic categories τ , R , Q and S , respectively.
The sorts need not be explicitly present in the graph at run-time,
but it is useful to imagine that they are. Each node also has a contents which is either VAR or ξ(X1 , . . . , Xn ) where ξ is one of thefollowing type constructors:5• {[ · / ·⇒· ]} with kind ROW × QSET × SSET → TYPE.
• `:·, ·, for any `, with kind TYPE × ROW → ROW.
• ⊥ with kind SSET.
• L , for any L , with kind SSET or QSET.

When the contents of a node X is ξ(X1 , . . . , Xn ), the number andsorts of nodes X1 through Xn , as well as the sort of X itself, must be
as specified by the kind of ξ.
A node with contents VAR represents a type (or row or set)variable of the appropriate sort. Each such variable is represented
by exactly one node; we can thus identify the variable with the nodeand do not need explicit names for type variables until and unless
we want to output the inferred type textually.
The nodes in the type graph are elements of a union-find data
structure, which provides the following four primitives: EQUAL(X1 , X2 ) tests whether X1 and X2 refer to the same node. READ(X)produces the contents of node X. FUSE(X1 , X2 , ζ) creates a single
node with contents ζ and destructively redirects all existing references to either X1 or X2 such that they now refer to the new node.
(The unification algorithm only performs this operation when X1
and X2 have the same sort, so the sort of the new node is unambiguous.) Finally, one may CREATE a new node with a given sortand contents. It is well known that k operations in the union-findstructure can be done in total time at most O(k α(k)), where α is anextremely slow-growing function.6
6.2

Consistent graphs

The exposed nodes of the type graph are all nodes of sort ROW
that are mentioned in the contents of a node whose sort is not ROW.
That is, the only ROW nodes that are not exposed are those thatare linked to either not at all or only from ROW nodes. The stateof the algorithm is consistent iff there exists a function ψ ∈ X →Pfin ( ` ) such that ψ(X) = ∅ for all exposed nodes X, and wheneverREAD(X) = `:X 0 , X 00 it holds that ψ(X 00 ) = ψ(X) ] {`} (and ψ(X)can be undefined if X is not of sort ROW). Consistency meansthat each row variable always appears after the same set of labels(although they may appear in different orders).
It is an invariant of the algorithm that its state is consistent. This
ensures that we will not have to worry about creating ill-formedrows that define the same label twice; the map ψ in the definition
5 For other type systems than Martini it is easy to add more type constructors, for example “→” of kind TYPE → TYPE → TYPE. The only fixedpart of the signature is the constructors for ROW which must be exactly“`:·, ·” and nothing else.
6 A possible definition is: α(k) is the least i ≥ 1 such that A(i, 4) > log k,where A is a variant of Ackermann’s function [24].

1. For each type, row or set variable β in W , CREATE a nodewith the appropriate sort and contents VAR. Let θ be themap from each β to its corresponding node.
2. Replace each (τ , τ 0 ) in W with the pair (BUILDθ (τ ),BUILDθ (τ 0 )).
3. Do steps (4)-(10) for as long as W is not empty. Go to step(11) when W becomes empty.
4. Select an equation (X, X 0 ) from W and remove it from W .
5. If EQUAL(X, X 0 ), then discard the pair and start over fromstep (3).
6. If READ(X) = VAR, then execute FUSE(X, X 0 ,READ(X 0 )), and start over from step (3).
If READ(X 0 ) = VAR, then execute FUSE(X, X 0 ,READ(X)), and start over from step (3).
7. Set ξ(X1 , . . . , Xk ) = READ(X) and set ξ 0 (X10 , . . . , Xk00 ) =READ(X 0 ). (This step will not be reached unless the contents of the two nodes have this form.)
8. If ξ 6= ξ 0 , then the unification problem is intrinsically unsolvable. Report failure and terminate the algorithm. (Martini has only one constructor of sort TYPE, but this canhappen for SSET and QSET.)
9. Execute FUSE(X, X 0 , ξ(X1 , . . . , Xk )).
10. Execute RECUNIF(Xi , Xi0 ), defined below, for 1 ≤ i ≤ k,and start over from step (3).
11. (This step is reached when W becomes empty.) Searchfor cycles in the type graph, for example by a depth-firsttraversal looking for back edges. If any are found, thenstop and report failure.
12. If this step is reached, then the unification has succeeded.
Return the substitution { READOUT(θ(β)) | β ∈ Dom θ }.
Figure 5. Definition of the unification algorithm RUNIFY(W )corresponds to the kinding discipline of [20, pp. 647ff]. In particular, the initial state produced by the caller must be consistent or thealgorithm will not work. Fortunately, it is easy see that the equation sets produced by the COLLECT procedure of Section 5.3 will
naturlly be represented by consistent graphs. (Each recursive invocation of COLLECT constructs an isolated component of the graphthat is initially connected to other components solely through theunification queue W , which has no influence on consistency.)
6.3 The algorithm
The unification algorithm is defined in Figures 5 and 6. The algorithm keeps a queue W of waiting equalities, represented as pairs(X1 , X2 ). It is an invariant that when (X1 , X2 ) ∈ W , then X1 and X2
must have the same sort, which must not be ROW. In step (4), thestrategy for picking an equation to remove is not important; theusual recursive unification algorithm corresponds to a LIFO queuethat coincides with the implementation language’s call stack.
Step (11) implements the occurs check, which is usually described as being part of step (6), but the latter is executed too often
to afford doing it there if we want almost-linear complexity. If (contrary to most real-world type checkers that want to report errors to
the user in a readable way) we are not interested in knowing why
the unification failed, it suffices to check the type graph for cycles
once after the unification queue becomes empty.
Notice that part (b) and (c) of RECUNIF is the only place in thealgorithm that specifically concerns rows. All other steps appear
unchanged in the well-known first order unification algorithm.
Theorem 6.1. The RUNIFY algorithm produces a most generalunifier whenever its input has any unifier. If the input does not havea unifier it will terminate with a failure report.

This is the RECUNIF(X, X 0 ) procedure used in step (10) of
RUNIFY:a. If the sort of X and X 0 is not ROW, just add (X, X 0 ) to W
and return.
b. (If this step is reached, both of X and X 0 are exposed
ROW nodes.) Let (ϕ, X0 ) = GETROW(X) and (ϕ0 , X00 ) =GETROW(X 0 ). For each ` ∈ (Dom ϕ ∪ Dom ϕ0 ) (in somearbitrary order), do
1. If ` ∈ (Dom ϕ ∩ Dom ϕ0 ), add (ϕ(`), ϕ0 (`)) to W .
2. Otherwise, if ` ∈ Dom ϕ: CREATE a new node X10
with sort ROW and contents VAR. Then execute
FUSE(X00 , X00 , (`:ϕ(`), X10 )), and set X00 := X10 .
3. Otherwise, if ` ∈ Dom ϕ0 : CREATE a new node X1
with sort ROW and contents VAR. Then execute
FUSE(X0 , X0 , (`:ϕ0 (`), X1 )), and set X0 := X1 .
c. Execute FUSE(X0 , X00 , VAR) and return.
BUILDθ (t) is a side-effecting function from type terms t tonode names, parameterized by a map θ from variables to X :BUILDθ (β) = θ(β).
BUILDθ (ξ(t1 , . . . ,tn )) =let Xi = BUILDθ (ti ) for 1 ≤ i ≤ n
in CREATE a node with contents ξ(X1 , . . . , Xm )and return its name.
GETROW(X) is defined when X is a node of sort ROW andthe unification graph is consistent:
GETROW(X) =case READ(X) of `:X 0 , X 00 ⇒ let (ϕ, X 000 ) = GETROW(X 00 )in ({` 7→ X 0 } ¢ ϕ, X 000 )| VAR⇒ (∅, X)READOUT maps a node name in an acyclic graph to a type
term. It depends on a fixed injective mapping κ from node
names to variables of appropriate sorts.
READOUT(X) =case READ(X) of
ξ(X1 , . . . , Xn ) ⇒ ξ(READOUT(X1 ), . . . , READOUT(Xn ))| VAR⇒ κ(X)
Figure 6. Helper definitions for RUNIFY
Theorem 6.2. The RUNIFY algorithm, except for the final READOUT operations, runs in time O(nm α(n)), where n is the total sizeof the input and m is the number of different field labels mentioned
in it.
Proof. Let N be the largest number of operands of any type constructor; this is assumed to be a constant. When ϕ’s are represented
as arrays, each GETROW operation uses at most O(m) time plus
m union-find operations. Each RECUNIF operation uses at mostO(m) time plus 4m + 1 union-find operations. It may add up to mpairs to W . The total number of RECUNIF operations is at mostNn, because step (10) is always done together with (9), which decreases by one the number of non-ROW nodes (which are nevercreated after step (2)). Therefore, at most Nnm pairs are added to
the O(n) initial pairs in W during the algorithm. Steps (1)–(10) of
the main algorithm are executed at most O(Nnm) + O(n) = O(nm)times. Each execution spends constant time plus a constant number of union-find operations outside RECUNIF. Step (11) uses a

Terms:
M, N ::= · · · | let x = N in M
Generalized t-vars: β ::= s | q | r | α
Variable sets:
B ∈ Pfin ( β )Type schemes:
σ ::= ∀B.hτ |Ci→ τ ∪ σEnvironments:Γ ∈ x fin
let x = N in M ,→ [x 7→ N]MRLetΓ (x) = ∀B.hτ |Ci∀β 6∈ B : T (β) = β
TPoly
x : hΓ ` T (τ ) | T (C) ∪C0 i
N : hΓ ` τ | Ci
B = FTV(τ ,C) \ FTV(Γ )M : hΓ ¢ {x 7→ ∀B.hτ |Ci} ` τ 0 | C0 i
TLet
let x = N in M : hΓ ` τ 0 | C0 i
Figure 7. Adding Hindley/Milner polymorphism to Martini tomake Martini∀ . Things not defined here are in Figure 3.

constant number of union-find operations for each graph edge. The
number of edges is bounded by the number of operations alreadyperformed (each edge must have been added at some time), so because step (11) happens only once, it can at most increase the number of operations performed by a constant factor.
In total, O(nm) + O(Nn(4m + 1)) = O(nm) union-find operations are executed. The work except for these is also O(nm), so
the total time complexity of the unification algorithm is O(nm) +O(O(nm) α(O(nm))) = O(nm α(n)), as required.

7. Let-polymorphism
Because Martini has principal typings, we can add to it Milner’s letpolymorphism to get a type system Martini∀ that is to Martini what
the Hindley/Milner (HM) type system (used by languages like ML)
is to the simply typed λ-calculus. Figure 7 shows the completely
conventional additions that do this. Note that type schemes have aconstraint component, as is often done in HM extensions involving
constraints.
We know that the additional rules in Figure 7 correctly implement let-polymorphism, because Martini∀ types the same programs as would be typed by Martini extended with the single ruleN : hΓ ` τ | Ci
[x 7→ N]M : hΓ ` τ 0 | C0 i
let x = N in M : hΓ ` τ 0 | C0 i
which deliberately ignores τ and C and is well known to correctly characterize the power of Milner’s let-polymorphism. Principal types relative to a given Γ in Martini∀ can be computed by
the obvious extension of the standard algorithm W or one of its
variants. Interleaved constraint simplification yields ground principal types. Note that, as usual for systems extended with Milner’s
let-polymorphism, Martini∀ has only the weaker principal types,
not principal typings.
Note that let-polymorphism is not enough for ML-style modules. Entire mixin modules can be polymorphic, but not individual
module components, unlike ML structures and functors, which also
have features addressing type abstraction and the diamond importproblem such as type components in structures and type sharing
specifications. More work is needed to add such features to Martini.

8. Conclusion
8.1

Summary of contributions

This paper makes these novel contributions:
1. Section 4 proves that typability is NP-complete for Riviera, thestraightforward system of simple types for the m-calculus, acalculus of first-class mixin modules with symmetric linking.
Riviera roughly corresponds to previous mixin module typesystems. We point out that the expense comes from the typesystem checking constraints from dead or sleeping code.
2. Because our NP-completeness proof (1) works for the restriction of Riviera to the λ⊕ subset of the m-calculus and (2) is insensitive to whether linking is symmetric or asymmetric (overriding), we have also proven that type inference is NP-complete
for Wand’s type system for the λ-calculus with record concatenation [28]. The only similar previous NP-completeness result
is by Palsberg and Zhao [16] for a more complicated systemwith subtyping.
3. Section 5 develops Martini, a system of simple types for the mcalculus. Martini is conceptually simple, with no subtyping anda clean and balanced separation between (1) traditional simple
types with type and row variables for determining field typesand (2) constraints for safety of linking and field extraction.
4. Section 5 also develops type inference for Martini, and provesthat Martini has principal typings [29]. Martini is the first
type system for first-class mixin modules with a type inference
algorithm. Its time complexity is O(nm α(n)), where the input
has size n and m distinct field labels, and α(n) is negligible.
5. By restricting Martini to the λ⊕ subset of the m-calculus, weachieve type inference for a λ-calculus with symmetric record
concatenation with the same complexity, better than the previously best published complexity for any type inference algorithm for record concatenation. (Some previous type inference
algorithms for record concatenation without published complexity analyses may have comparable complexities.)
6. Section 6 presents an efficient implementation of row unification with a rigorous complexity analysis.
7. We have implemented inference of principal typings for Martini; our implementation can be downloaded or used on-line athURL:http://www.macs.hw.ac.uk/DART/software/Martini/i.
8. Section 7 shows how to extend Martini with Milner’s letpolymorphism to make Martini∀ , which we believe is the firstpolymorphic type system for first-class mixin modules.
8.2

Acknowledgements

We are grateful to Davide Ancona, Sonia Fagorzi, and Elena Zucca
for discussions during a visit by us to Genova which led directly tothis work. We thank François Pottier and James Cheney for enlightening electronic discussions of the complexity of row unification,
and Elena Zucca, Tom Hirschowitz, Gérard Boudol, and anonymous referees for helpful comments.

References[1] D. Ancona, S. Fagorzi, E. Moggi, E. Zucca. Mixin modules andcomputational effects. In Proc. 30th Int’l Coll. Automata, Languages, andProgramming, vol. 2719 of LNCS. Springer-Verlag, 2003.
[2] D. Ancona, S. Fagorzi, E. Zucca. A calculus with lazy module
operators. In IFIP TC1 3rd Int’l Conf. Theoret. Comput. Sci. (TCS ’04).
Kluwer Academic Publishers, 2004.
[3] D. Ancona, E. Zucca. A primitive calculus for module systems. In
Proc. Int’l Conf. Principles & Practice Declarative Programming, vol.
1702 of LNCS. Springer-Verlag, 1999.
[4] D. Ancona, E. Zucca. A calculus of module systems. J. Funct.
Programming, 12(2), 2002. Extended version of [3].

[5] D. Duggan, C. Sourelis. Mixin modules. In Proc. 1996 Int’l Conf.
Functional Programming. ACM Press, 1996.
[6] Programming Languages & Systems, 9th European Symp. Programming, vol. 1782 of LNCS. Springer-Verlag, 2000.
[7] M. Flatt, M. Felleisen. Units: Cool modules for HOT languages. In
Proc. ACM SIGPLAN ’98 Conf. Prog. Lang. Design & Impl., 1998.
[8] R. Harper, B. C. Pierce. A record calculus based on symmetricconcatenation. Technical Report CMU-CS-90-157R, Carnegie Mellon
Univ., 1991.
[9] R. Harper, B. C. Pierce. A record calculus based on symmetricconcatenation. In Conf. Rec. 18th Ann. ACM Symp. Princ. of Prog. Langs.,
1991.
[10] T. Hirschowitz. Mixin Modules, Modules, and Extended Recursion ina Call-by-Value Setting. PhD thesis, Université Paris 7, 2003.
[11] T. Hirschowitz. Rigid mixin modules. In Seventh International
Symposium on Functional and Logic Programming (FLOPS 2004), 2004.
[12] T. Hirschowitz, X. Leroy. Mixin modules in a call-by-value setting. In
Programming Languages & Systems, 11th European Symp. Programming,
vol. 2305 of LNCS. Springer-Verlag, 2002.
[13] T. Hirschowitz, X. Leroy, J. B. Wells. Call-by-value mixin modules:
Reduction semantics, side effects, types. In Programming Languages &Systems, 13th European Symp. Programming, vol. 2986 of LNCS. SpringerVerlag, 2004. More details can be found in [10].
[14] H. Makholm, J. B. Wells. Type inference, principal typings, and letpolymorphism for first-class mixin modules. Technical report, Heriot-Watt
Univ., School of Math. & Comput. Sci., 2005.
[15] A. Ohori, P. Buneman. Type inference in a database programming
language. In Proc. 1988 ACM Conf. LISP Funct. Program., Snowbird,Utah, U.S.A., 1988.
[16] J. Palsberg, T. Zhao. Type inference for record concatenation andsubtyping. Inform. & Comput., 189, 2004.
[17] F. Pottier. A 3-part type inference engine. In ESOP ’00 [6].
[18] F. Pottier. A versatile constraint-based type inference system. Nordic
Journal of Computing, 7(4), 2000.
[19] F. Pottier. A constraint-based presentation and generalization of rows.
In Proc. 18th Ann. IEEE Symp. Logic in Comput. Sci., 2003.
[20] F. Pottier, D. Rémy. The essence of ML type inference. In B. C. Pierce,ed., Advanced Topics in Types and Programming Languages, chapter 10.
MIT Press, Cambridge, Massachusetts, 2005.
[21] D. Rémy. Typing record concatenation for free. In Conf. Rec. 19th
Ann. ACM Symp. Princ. of Prog. Langs., 1992. A later version is [22].
[22] D. Rémy. Typing record concatenation for free. In C. A. Gunter,
J. C. Mitchell, eds., Theoretical Aspects Of Object-Oriented Programming:
Types, Semantics and Language Design. MIT Press, 1993.
[23] D. Rémy. A case study of typechecking with constrained types:
Typing record concatenation. Presented at the workshop on Advances in
Types for Computer Science at the Newton Institute, Cambridge, UK, 1995.
[24] R. E. Tarjan. Efficiency of a good but not linear set union algorithm.
J. ACM, 22(2), 1975.
[25] S. Vansummeren. On the complexity of deciding typability in therelational algebra. Acta Informatica, 200X. To appear.
[26] M. Wand. Complete type inference for simple objects. In Proc. 2nd
Ann. Symp. Logic in Comput. Sci., 1987. A corrigendum appeared at LICS
1988.
[27] M. Wand. Type inference for record concatenation and multiple
inheritance. In Proc. 4th Ann. Symp. Logic in Comput. Sci., Pacific Grove,
CA, U.S.A., 1989. IEEE Comput. Soc. Press.
[28] M. Wand. Type inference for record concatenation and multiple
inheritance. Inform. & Comput., 93, 1991.
[29] J. B. Wells. The essence of principal typings. In Proc. 29th Int’l Coll.
Automata, Languages, and Programming, vol. 2380 of LNCS. SpringerVerlag, 2002.
[30] J. B. Wells, R. Vestergaard. Confluent equational reasoning for linking
with first-class primitive modules (long version). A short version is [31].
Full paper, 3 appendices of proofs, 1999.
[31] J. B. Wells, R. Vestergaard. Equational reasoning for linking with
first-class primitive modules. In ESOP ’00 [6]. A long version is [30].
[32] J. Zwanenburg. A type system for record concatenation and subtyping.
In K. Bruce, G. Longo, eds., Third Workshop on Foundations of Object
Oriented Languages (FOOL 3), Rutgers Univ., NJ, USA, 1996.