Type Inference, Principal Typings,and Let-Polymorphism
for First-Class Mixin Modules
Henning Makholm and Joe Wells
Technical University of Denmark and Heriot-Watt University

UsefulLogics,Types,Rewriting, and theirAutomation

ICFP’05 – Tallinn, Estonia – September 27, 2005
Work supported by EU/IST/FET grant 2001-33477 (DART)Type Inference, Principal Typings, and Let-Polymorphism for First-Class Mixin Modules – p.1/17

What is this all about?
The m-calculus:
Variables:
x ::= x | y | z | · · ·Field labels: ` ::= f | g | h | · · ·Terms:
M, N ::= x | M.` | M ⊕ N | {[γ1; . . . ; γk]}
Module items: γ ::= local x = M| export ` . x = M| import ` . x
We recognize variables, field selection, some kind of fancy
sum operator, but what on earth is “{[γ1, . . . , γk]}”?
Is it a record...?
Is it a letrec...?
Is it a closure...?
It is a mixin module!
UsefulLogics,Types,Rewriting, and theirAutomation

Type Inference, Principal Typings, and Let-Polymorphism for First-Class Mixin Modules – p.2/17

Anatomy of a mixin module
The m-calculus:
Variables:
x ::= x | y | z | · · ·Field labels: ` ::= f | g | h | · · ·Terms:
M, N ::= x | M.` | M ⊕ N | {[γ1; . . . ; γk]}
Module items: γ ::= local x = M| export ` . x = M| import ` . x
A mixin module consists of three kinds of items:
A local definition binds an internal name x to anexpression M
An export binds an external label ` to an expression M(while also providing a local definition for x)
An import binds an internal name x to a linking promise
represented by the external label `.
UsefulLogics,Types,Rewriting, and theirAutomation

Type Inference, Principal Typings, and Let-Polymorphism for First-Class Mixin Modules – p.3/17

An example{[ local •d = λx•.x
• − 1;
export odd . o• = λx•.if x• = 0 then false else not(v•(d•(x•)));
import even . v•;export even . v• = λx•.if x• = 0 then true else not(o• (x• − 1));
import odd . •o; ]}Linking uses one operand’s exports to bind the other one’s
imports... and vice versa: Linking is symmetric
Recursion may arise “spontaneously”
Well-known examples of symmetric linking include
C compilation units, but not ML modules
UsefulLogics,Types,Rewriting, and theirAutomation

Type Inference, Principal Typings, and Let-Polymorphism for First-Class Mixin Modules – p.4/17

Other module operations
Field extraction{[ local d = λx.x − 1;export odd . o = λx.if x = 0 then false else not(v(d(x)));export even . v = λx.if x = 0 then true else not(o(x − 1));]}.even(42) ,→∗ true
Field hiding makes exports into locals{[ export f . x = 5;
export g . y = x + 17; }] \\ {f},→ {[ local x = 5;
export g . y = x + 17; }]UsefulLogics,Types,Rewriting, and theirAutomation

Type Inference, Principal Typings, and Let-Polymorphism for First-Class Mixin Modules – p.5/17

Modules as first-class citizens
Modules can be bound to variables and can beimported/exported from other modules
Expressions in module constructions can mention variables
that are bound in an enclosing scope{[local x = 5; export f . _ = {[export g . _ = x + 7]}]}
Constructs from lambda calculus can be simulated directly:(λx.M) =⇒ {[import in . x; export out . _ = M]}
M N =⇒ (M ⊕ {[export in . _ = N]}).out

Records are a restricted case of modules:{[f = 42; g = "foo"]}=⇒ {[export f . _ = 42; export g . _ = "foo"]}In this case, linking becomes record concatenation.
UsefulLogics,Types,Rewriting, and theirAutomation

Type Inference, Principal Typings, and Let-Polymorphism for First-Class Mixin Modules – p.6/17The Martini type system: design goals
Type safety by progress & subject reduction
No extraction of a field that is not exported
No extraction from a module with unsatisfied imports
No linking of two modules that export the same nameNo hiding of names that the module imports
Tractable automatic type inference. (First for mixin modules!)Not trivial: The most straightforward typing rules forlinking lead to an NP-complete typing problem
Principal typings for compositional type inference
Principal types: Given M and Γ , find “best” τ s.t. Γ ` M : τPrincipal typings: Given M, find “best” (Γ, τ) s.t. Γ ` M : τML types have principal types, but not principal typings
To emphasize principal typings, we write M : hΓ ` τi

UsefulLogics,Types,Rewriting, and theirAutomation

Type Inference, Principal Typings, and Let-Polymorphism for First-Class Mixin Modules – p.7/17

Martini types explained by example
Let M = {[ local d = λx.x − 1;export odd . _ = λx.if x = 0 then false
else not(e(d(x)));import even . e; }]Some valid types for M are:{[ |even:int→bool,⇒{odd} ]}{z odd:int→bool} / {even}| {z } | {z }Types of all imports and exports

Imports

Exports{[ even:int→bool, odd:int→bool, k:string / {even} ⇒{odd} ]}|{z}More types than necessary are OK{[ even:int→bool, odd:int→bool, k:string / {even, k}⇒{odd} ]}| {z }Overapproximation here OK{[ |even:int→bool, {zodd:int→bool, r0} / {even, k} ⇒{odd} ]}Any row defining even and odd

UsefulLogics,Types,Rewriting, and theirAutomation{[ even:int→bool, odd:int→bool, r0 / q0 ⇒{odd} ]}whenever the constraint set {q0 ⊇ {even}} is satisfied
Type Inference, Principal Typings, and Let-Polymorphism for First-Class Mixin Modules – p.8/17

Another example (principal) typing
Let N = λx.λy.(x ⊕ y).f + 42
Giving this a principal typing is not trivial:
The input modules x and y may need to exchange values
before one of them can calculate a value for f.
We don’t even know which of x and y will export f.
Exactly one of them must.
Row overapproximation to the rescue!
N has type {[ f:int, r / q1 ⇒s1 ]} → {[ f:int, r / q2 ⇒s2 ]} → int
with constraint set {s = s1 ] s2, {f} ⊆ s, s2 ⊇ q1, s1 ⊇ q2}
Both rows contain “f:int”... meaning if the module exports f, then it has type int

UsefulLogics,Types,Rewriting, and theirAutomation

Constraints ensure that exactly one of s1 and s2 contain fMore constraint to ensure that x’s imports are satisfied byy’s exports, and vice versa
Type Inference, Principal Typings, and Let-Polymorphism for First-Class Mixin Modules – p.9/17

Grammar for Martini types
Label sets:
L ::= {`1, . . . , `k}(k ≥ 0)Type rows:
R ::= r0 | r1 | r2 | · · · | `:τ, R
Import set expressions: Q ::= q0 | q1 | q2 | · · · | L
Export set expressions: S ::= s0 | s1 | s2 | · · · | L | ⊥Types:
τ ::= ’a | ’b | ’c | . . . | {[ R / Q ⇒S ]}Each of the classes R, Q, S, τ has an infinity of variables
The concrete form of Q and S is just a set of field names.
An S can also be ⊥; the type {[ R / Q ⇒⊥ ]} is always void
A row R is a series of field–type bindings, always
ending with a row variable
For all `1 6= `2 we impose the equation(`1:τ1, `2:τ2, R) = (`2:τ2, `1:τ1, R)
UsefulLogics,Types,Rewriting, and their
Automation

There is no syntax for an empty row– a row variable can always be used insteadType Inference, Principal Typings, and Let-Polymorphism for First-Class Mixin Modules – p.10/17

Constraint language
S constraints: cS ::= S = S1 ] S2 | S = S1 \ LQ constraints: cQ ::= Q ⊇ Q1 \ S | Q # L
Constraints:c ::= cS | cQ
Constraint sets: C ::= {c1, . . . , ck}(k ≥ 0)Central principle: Constraints speak about label sets only.
(In particular, about possible instantiations of set variables).
The structure of rows and types is independent ofconstraints.
Sets on a constraint RHS come from operand types.
The set on the LHS is part of the result type.
In S constraints the operands exactly determine the result set.
Q constraints allow the result to overapproximate.
A constraint with ⊥ on its RHS comes from an expression
whose operand can never exist at run-time.
Such a constraint is by definition solved.

UsefulLogics,Types,Rewriting, and theirAutomation

Type Inference, Principal Typings, and Let-Polymorphism for First-Class Mixin Modules – p.11/17

Judgements and rules
Typing judgements have the form M : hΓ ` τ | Ci
An example rule:M : hΓ ` {[ R / Q1 ⇒S1 ]} | Ci
N : hΓ ` {[ R / Q2 ⇒S2 ]} | Ci
C ° {Q ⊇ Q1 \ S2, S = S1 ] S2, Q ⊇ Q2 \ S1}M ⊕ N : hΓ ` {[ R / Q ⇒S ]} | Ci

where C1 ° C2 if all substitutions that solve C1 also solve C2.
The same C is used in the entire derivation.
The concrete form of Q’s and S’s matters only in constraints.

UsefulLogics,Types,Rewriting, and theirAutomation

Type Inference, Principal Typings, and Let-Polymorphism for First-Class Mixin Modules – p.12/17

Type inference for Martini
Phase 1a: Ignore all rule premises of the form C ° {· · ·}Then inference can be done by standard techniques
using first-order unification in the presence of rowsDuring this phase Q’s and S’s are always variables
Set variables may get unified but get no more structure
Fixes the type/row structure of the principal typing
Phase 1b: Let C be union of the right-hand-side of all theignored C ° {· · ·} premisesThis C is the most liberal constraint set that entails all of
the right-hand-sides
Theorem: The typing after Phase 1b is principal
Phase 2: Solve the collected C
In practice most of the three phases will be interleaved(This gives more readable principal typings)

UsefulLogics,Types,
Rewriting, and theirAutomation

Type Inference, Principal Typings, and Let-Polymorphism for First-Class Mixin Modules – p.13/17

Formal properties
Subject reduction holds
If M : h∅ ` τ | Ci for C solvable, then M does not go wrong
C can be checked for solvability in timeO((number of constraints) · (number of different field labels))

Solutions sometimes contain ⊥Type inference and constraint solving takes timeO((length of program) · (number of different field labels) · α(· · ·))Oops! C1 ° C2 is hard to decide. But luckily we don’t have to.

UsefulLogics,Types,Rewriting, and theirAutomation

Type Inference, Principal Typings, and Let-Polymorphism for First-Class Mixin Modules – p.14/17

Reasons to read our paper(beyond wanting to see the formalism behind the previous slides)
How to solve constraints in our systemand how to restrict the solving such as not to lose principality
Extension of Martini with let-polymorphism by theHindley–Milner procedure
A robust proof that ⊥-less typing rules forlinking/concatenation operators make typability NP-hard.
(Even just concatenable records in a first-order language)First written down presentation of an efficient algorithm forrow unification
URL for our online type inference implementation
UsefulLogics,Types,Rewriting, and theirAutomation

Type Inference, Principal Typings, and Let-Polymorphism for First-Class Mixin Modules – p.15/17

Shortcomings and future work
Programming in the large: Not nearly strong enough tosubsume ML modules (yet!)
Needs polymorphism of local bindings in modules
Needs type components of modules
Needs type abstractions for modules
Row pollution: When a module is constructed, the row partof its type will list types of all fields the module may ever belinked with.
Not that bad: The list will be inferred
Can be mitigated by polymorphism or by programmer
annotations.
Perhaps stratifed type inference could also be useful.

UsefulLogics,Types,Rewriting, and their
Automation

Type Inference, Principal Typings, and Let-Polymorphism for First-Class Mixin Modules – p.16/17

The endThank you
Questions?

UsefulLogics,Types,Rewriting, and their
Automation

Type Inference, Principal Typings, and Let-Polymorphism for First-Class Mixin Modules – p.17/17