A Type Theoretic Specification of Type Inference
Kenichi Asai

Kyoko Kadowaki

Ochanomizu University, Japan
asai@is.ocha.ac.jp, kado@pllab.is.ocha.ac.jp

Abstract

but not the binding time analysis it depends on. This is unfortunate,especially in the presence of the structurally recursive unification
algorithm (McBride 2003), which could form a basis for the wholedevelopment.
In this paper, we present the complete formalization of type inference for simply-typed λ-calculus, including unification, where
the soundness and completeness properties are internally expressedin the type inference algorithm. The formalization is done in Agda
(Norell 2008), which is based on dependent type theory (MartinLöf 1984). Our formalization of type inference relies on three techniques: McBride’s unification algorithm, generic programming,and a novel parallel relation between two inequalities (i.e., types).
We exploit McBride’s unification algorithm to formalize type
inference, thereby establishing the solid mechanized foundation oftype inference that uses unification. Since we want our formalization to be applicable to various type systems, we extend McBride’s
unification algorithm to work on any data defined generically in thesum-of-product form. We then formalize type inference on top of it
as a function from an untyped term to the corresponding well-typed
term, where both soundness and completeness properties are built
into types.
Since McBride’s unification algorithm keeps track of the number of metavariables, a naive formalization on top of it requires
many calculations on the number of metavariables, disturbing theessence of the underlying type inference algorithm.1 To maintainthe proof simple and clear, we introduce inequalities on the numberof metavariables and the parallel relation that must hold between
two inequalities. The parallel relation not only enables us to avoid
maintaining the exact number of metavariables but also allows us
to prove necessary but easy inequalities only.
The formalization clearly shows the interaction between allocation of new metavariables and substitution, something that was notobserved in the previous formalizations. Although the proof itself
is non-trivial, we can keep the structure of the type inference very
close to type checking thanks to the parallel relation. The resulting
type inference is simple enough to understand without sacrificing
the fine details of the proof including the number of metavariables.
The contributions of this paper are summarized as follows.

This paper presents the complete formalization of type inference
for simply-typed lambda calculus, including unification, and proves
its soundness as well as completeness in the dependently-typed programming language Agda. The formalization clearly shows the interaction between allocation of new metavariables and substitution,
something that was not observed in the previous formalizations. After introducing metavariables generically using the two-level types
approach by Sheard and Pasalic, we extend McBride’s unification
algorithm to work on generic data defined in the sum-of-productform. We then define a type inference function that, given an untyped term, returns either a proof that the term is untypable or a corresponding well-typed term together with the proof that the inferred
type is most general. During the proof development, we introduce aparallel relation between two inequalities, the key relation to keep
the proof simple and clear. As a result, we could summarize thesoundness of the type inference as typing rules that are intuitively
clear but reflect all the details of the type inference in Agda.
General Terms Languages
Keywords Type inference, unification, mechanized proof, Agda,
dependent type, generic programming

1.

Introduction

Internal verification of programs (Altenkirch 1996; Stump 2016)
utilizes types to express various properties on data structures orprograms and enables us to maintain or prove those properties
directly and ingeniously. With internal verification, we can keep
variety of properties, such as the length of vectors, the balanced
property of Braun trees, and even ordering invariants for a genericdata in which most of the proofs are done automatically (McBride2014). In his keynote talk at ICFP 2013, Ulf Norell showed us how
the internal encoding of λ terms leads to a beautiful type checking
algorithm.
However, internal verification has not been used for type inference so far, partly because type inference, unlike type checking, requires unification of metavariables. Although we have various nicetechniques of internal verification, e.g., the automatic assurance oftype soundness by writing a typed interpreter, we have not beenable to use them for type inference, and hence many static analyses
that are often formalized as type inference problems. Thus, one candiscuss correctness of offline partial evaluation (Asai et al. 2014),• We extend the structurally recursive unification algorithm by

McBride (2003) so that it works for arbitrary sum-of-producttype of generic data.
• We formalize type inference including unification for simply-

typed λ-calculus and prove its correctness in Agda.
• We introduce the parallel relation between two inequalities andshow how it simplifies the correctness proof considerably.
• We clarify the interaction between allocation of new metavari-ables and substitution in the type inference.
1 This is reminiscent of the proof with α-equivalence where the freshness

condition disturbs the essence of the proof.

[Copyright notice will appear here once ’preprint’ option is removed.]

1

2020/9/30

types:type environments:
terms:
typing rules:

t
Γ
e

:=
:=
:=

unit | t1 → t2
(empty) | Γ, x : t
x | λx. e1 | e1 e2 | •then define (and prove correct) unification once and for all for any
generic data.
In the generic programming, data is defined in the sum-ofproduct form as a pattern functor and arbitrary large data is constructed by closing the recursive position by a fixed-point operator.
We use a simplified version of Regular (van Noort et al. 2008) as
formulated by Magalhães and Löh (2012). In Regular, a patternfunctor is defined as follows:

Γ(x) = tΓ, x : t2 ` e1 : t1
(TLam)(TVar)
Γ`x:t
Γ ` λx. e1 : t2 → t1
Γ ` e 1 : t2 → t1 Γ ` e 2 : t2
(TApp)(TUnit)Γ ` e1 e2 : t1
Γ ` • : unit

data Code : Set where
U : Code –– unit
I : Code –– recursive position_⊕_ : (F G : Code) → Code –– sum_⊗_ : (F G : Code) → Code –– productFigure 1. Simply-typed λ-calculus with unit

• We formulate the type inference as typing rules that incorpo-

The type Code is the type of pattern functors. The first two constructors, U and I, represent unit and a recursive position. In Agda,
texts after –– up to the end of line are comments. The latter two
constructors are for sum and product. In Agda, underscores show
the position of the arguments. Thus, _⊕_ and _⊗_ are infix operators. We assume that _⊗_ has higher operator precedence than_⊕_. For example, the pattern functor for the simple types becomes as follows:

rate substitution of matevariables explicitly and that precisely
correspond to Agda implementation.
In the next section, we describe the uses of metavariables in type
inference, and introduce metavariables to the generic programming
framework. In Section 3, we extend McBride’s unification algorithm to generic data and introduce the parallel relation. After defining the simply-typed λ-calculus in Agda in Section 4, we show type
inference in Section 5. Related work is in Section 6 and the paper
concludes in Section 7.
In Agda, lexical tokens are separated by spaces, parentheses,
and braces only. All the other characters (including unicode characters) can constitute an identifier. For example, l≤l0 is a single
identifier, while l ≤ l0 (with spaces around ≤) is a predicate (type)stating that l is less than or equal to l0 . Although we try to explain
various features of Agda as we proceed, we assume basic familiarity with Agda. For thorough introduction, see (Norell 2008) for
example.
The complete Agda code is submitted as the anonymous supplementary material for interested reviewers.

2.

TypeF : Code
TypeF = U ⊕ I ⊗ I

where U is for unit and two I’s are the argument and return typesof a function type.
Before constructing an arbitrary large (recursive) data, we relatea pattern functor with an Agda type, by defining the followinginterpretation function:[[_]] : (F : Code) → (A : Set) → Set[[ U ]] A = >[[ I ]] A = A[[ F ⊕ G ]] A = [[ F ]] A ] [[ G ]] A[[ F ⊗ G ]] A = [[ F ]] A × [[ G ]] A

Metavariables, GenericallyGiven a pattern functor F and a type A representing the interpretation of the recursive position, the interpretation function returns acorresponding Agda type. The constructor U is mapped to the Agda
unit type >, which has a single inhabitant tt. The recursive position
I is mapped to the supplied type A. The sum _⊕_ is mapped tothe disjoint sum type ] in Agda, which comes with two injection
functions inj1 and inj2 . Finally, the product _⊗_ is mapped to thenon-dependent product type × in Agda, whose constructor is _,_.
Using the interpretation function, we can now create a recursive
data, following the two-level types approach by Sheard and Pasalic(2004).

When we specify a language, we use metavariables. For example,
Figure 1 defines types, type environments, terms, and typing rules
for the standard simply-typed λ-calculus, extended with unit • oftype unit. In the figure, t, Γ, x, and e (possibly with subscripts)
are metavariables, representing types, type environments, variables,
and terms, respectively.
Metavariables play an important role in type inference. Givena type environment and a term, type inference returns the typeof the term under the type environment, according to the typing
rules. This view of type inference goes without problems for units,variables, and applications. To infer the type of λx. e1 , however, weneed to infer the type of e1 under the type environment extended
with the type of x. But what is the type of x? We don’t know yet. It
will be fixed during the type inference of the body e1 . To represent
the yet unknown type of x, we use a metavariable, meaning that thetype of x can be any type at this moment. During the type inferenceof the body e1 , it will be instantiated to a required type.
The presence of metavariables during type inference means that
we need to somehow support metavariables in the type inference.
One way to do it is to extend the grammar with metavariables. For
example, we can redefine types ast:=data µ (F : Code) (m : N) : Set whereh_i : [[ F ]] (µ F m) → µ F m –– fixed point
hh_ii : (x : Fin m) → µ F m –– metavariable

Given a pattern functor F and a natural number m (having Agda
type N of natural numbers), µ F m represents the type of data
specified by F with up to m metavariables. The first constructor
h_i receives a value of type [[ F ]] (µ F m) to create a value of typeµ F m. Notice that the recursive position of [[ F ]] is filled with µ F
m itself, tying the knot of recursion. By supplying a data of type µ
F m at the recursive position, we can construct an arbitrarily large
recursive data.
Before presenting examples of simple types, we define the following constructor-like functions to avoid writing injection functions:

unit | t1 → t2 | m

where m represents a metavariable. However, this method works
only for this particular type. Since we want to implement type inference not only for the simply-typed λ-calculus but also for various
other languages, we employ generic programming and introduce
metavariables to any generically specified data definition. We can

TUnit : {m : N} → µ TypeF m
TUnit = h inj1 tt i

2

2020/9/30

_⇒_ : {m : N} → (t1 t2 : µ TypeF m) → µ TypeF m
t1 ⇒ t2 = h inj2 (t1 , t2 ) i(hfi : [[ F ]] A → A) → (hhfii : Fin m → A) →([[ G ]] (µ F m) → [[ G ]] A)
fmap U hfi hhfii tt = tt
fmap I hfi hhfii d = cata hfi hhfii d –– apply cata to rec. pos.
fmap (G1 ⊕ G2 ) hfi hhfii (inj1 d) = inj1 (fmap G1 hfi hhfii d)
fmap (G1 ⊕ G2 ) hfi hhfii (inj2 d) = inj2 (fmap G2 hfi hhfii d)
fmap (G1 ⊗ G2 ) hfi hhfii (d1 , d2 ) =(fmap G1 hfi hhfii d1 , fmap G2 hfi hhfii d2 )The parameters in the braces are implicit arguments whose values
are inferred by Agda type checker. Using these functions, we caneasily construct, for example, (unit → unit) → unit:
TypeEx1 : µ TypeF 0
TypeEx1 = (TUnit ⇒ TUnit) ⇒ TUnit

To introduce a metavariable, we use the second constructor
hh_ii of µ F m. Its argument is of type Fin m, which is a typeof finite natural numbers from 0 to m − 1 (constructed by zeroand suc). When m = 0 (as in TypeEx1 ), Fin 0 has no inhabitants
and thus no metavariables can be used. When m is greater than 0,
we can use metavariables. For example, TypeEx2 below uses one
metavariable hh zero ii:

cata : {F : Code} → {m : N} → {A : Set} →(hfi : [[ F ]] A → A) → (hhfii : Fin m → A) → (µ F m → A)
cata {F} hfi hhfii h d i = hfi (fmap F hfi hhfii d)cata {F} hfi hhfii hh x ii = hhfii x

These definitions pass Agda’s termination check, because it is now
evident that the third argument to cata is strictly decreasing. Thiskind of mutually recursive function definitions appears many times
in our development. Note that the new fmap requires two patternfunctors, F and G, because we want to recurse over the patternfunctor (via G) to find the recursive position, but the recursive
position itself has the type that depend on the original functor (µF m).
In this paper, we will often transform metavariables withoutchanging the overall structure of the data. We define the following
function that maps metavariables by instantiating A in the definitionof cata with µ F m0 and hfi with h_i:

TypeEx2 : µ TypeF 1
TypeEx2 = (TUnit ⇒ hh zero ii) ⇒ hh zero ii

We can use more than one metavariable:
TypeEx3 : µ TypeF 3
TypeEx3 = (TUnit ⇒ hh suc (suc zero) ii) ⇒ hh zero ii

In TypeEx3 , two metavariables are used among the allowed three.
We could also use hh suc zero ii in the type if we wanted.
The type µ F m indicates that there is up to m metavariables, notexactly m metavariables. Thus, if a term has type µ F m, the same
term has also type µ F m0 , for any m0 greater than m:

hhcataii : {F : Code} → {m m0 : N} →(hhfii : Fin m → µ F m0 ) → (µ F m → µ F m0 )
hhcataii hhfii t = cata h_i hhfii t

TypeEx4 : µ TypeF 4
TypeEx4 = (TUnit ⇒ hh suc (suc zero) ii) ⇒ hh zero ii

Using hhcataii, we can, for example, define lift≤ that injects a termof type µ F m into the same term of type µ F m0 when m ≤ m0 :Later, we will define a function that inject a term of type µ F m into
the same term of type µ F m0 .
Having defined a generic data, we next define a generic function. We could first define fmap0 that applies f to all the recursive
positions of a given term by descending down the data as follows:

lift≤ : {F : Code} → {m m0 : N} → m ≤ m0 → µ F m → µ F m0
lift≤ m≤m0 t = hhcataii (ń x → hh inject≤ x m≤m0 ii) t

where inject≤ is a function that injects x of type Fin m into thesame x of type Fin m0 given m ≤ m0 . It is important that lift≤ isdefined based on inequality m ≤ m0 and the conclusion of lift≤
does not impose any constraint on the form of the number of
metavariables. One could easily define lift+ that lifts the numberof metavariables by m0 .

fmap0 : (G : Code) → {A B : Set} →(f : A → B) → ([[ G ]] A → [[ G ]] B)
fmap0 U f tt = tt
fmap0 I f d = f d –– apply f to recursive position
fmap0 (G1 ⊕ G2 ) f (inj1 d) = inj1 (fmap0 G1 f d)
fmap0 (G1 ⊕ G2 ) f (inj2 d) = inj2 (fmap0 G2 f d)
fmap0 (G1 ⊗ G2 ) f (d1 , d2 ) = (fmap0 G1 f d1 , fmap0 G2 f d2 )lift+ : {F : Code} → {m : N} →(m0 : N) → µ F m → µ F (m + m0 )lift+ m0 t = hhcataii (ń x → hh inject+ m0 x ii) t

We could then define a generic catamorphic function that folds overa given generic type.

The applicability of this function, however, is severely restricted,
because we can apply this function only when the goal has exactly
the form µ F (m + m0 ) for some m and m0 . Suppose we have agoal of the form µ F (f 0) for some function f and want to proveit by lifting the number of metavariables of a term t of type µ F
m. We cannot use lift+ directly, because µ F (f 0) does not havethe form µ F (m + m0 ). We have to identify that the goal has to beof the form µ F (m + m0 ), prove that µ F (f 0) is actually equalto µ F (m + m0 ) for some m0 , and manually replace the type of t
accordingly (which is painful), before being able to use lift+ at all.
This is in contrast to lift≤, which does not impose such restriction
and which does not require manual replacement of a type of a term.
We can directly apply lift≤ in the above case and we are left with aconstraint m ≤ f 0 which we can prove later. The difference between
these two becomes particularly evident when we implement more
complex functions such as type inference.
In addition to a generic function, we will need a generic predicate to prove properties on generic terms. To define generic predicates, we follow the same path as generic functions, but with predicates instead of sets. The following interpretation function relatesa pattern functor with an Agda predicate, given a predicate P that
holds for the recursive position.

cata0 : {F : Code} → {m : N} → {A : Set} →(hfi : [[ F ]] A → A) → (hhfii : Fin m → A) → (µ F m → A)
cata0 {F} hfi hhfii h d i = hfi (fmap0 F (cata0 hfi hhfii) d)
cata0 {F} hfi hhfii hh x ii = hhfii x

Given a generic data of type µ F m, cata0 hfi hhfii computes a valueof type A by first applying itself to all the recursive positions of dusing fmap0 . The result (of type [[ F ]] A) is then passed to hfi thatdesignates how to handle each case of the pattern functor F. Since
the data can be a metavariable, we supply another function hhfii thatdesignates what to produce for metavariables.
Although the termination of cata0 hfi hhfii t is clear since therecursive call is made by fmap0 only at the recursive positions oft, the Agda termination checker does not infer this fact, because
the recursive call cata0 hfi hhfii textually appears without its thirdargument. To make the termination of cata0 clear, we instantiate
the argument f of fmap0 with the recursive call cata0 hfi hhfii anddefine these two functions mutually recursively:mutualfmap : {F : Code} → (G : Code) → {m : N} → {A : Set} →32020/9/30

[[_]]0 : (F : Code) → {R : Set} → (P : R → Set) → (d : [[ F ]] R) → Set[[ U ]]0 P tt = >[[ I ]]0 P d = P d[[ F ⊕ G ]]0 P (inj1 d) = [[ F ]]0 P d[[ F ⊕ G ]]0 P (inj2 d) = [[ G ]]0 P d[[ F ⊗ G ]]0 P (d1 , d2 ) = [[ F ]]0 P d1 × [[ G ]]0 P d2

We will also use thin, the partial inverse of thick.
 0y(y0 < x)thin x y0 =0
y + 1 (y0 ≥ x)
For any x and y of type Fin (suc m) and y0 of type Fin m, we havethin x y0 = y if and only if thick x y = just y0 . It is useful to define aversion of thick that comes with this property.

We can then define the following two functions mutually recursively.

thick2 : {m : N} → (x y : Fin (suc m)) →x ≡ y ] Σ[ y0 ∈ Fin m ] thin x y0 ≡ ymutualeverywhere : {F : Code} → (G : Code) → {m : N} → (P : µ F m → Set) →In the return type, Σ[ y0 ∈ Fin m ] thin x y0 ≡ y denotes a dependent(hfi : (d : [[ F ]] (µ F m)) → [[ F ]]0 P d → P h d i) →product whose first element is a number y0 and second element(hhfii : (x : Fin m) → P hh x ii) →is a proof for thin x y0 ≡ y. See the accompanying code for the0(d : [[ G ]] (µ F m)) → [[ G ]] P dstraightforward definitions of thick, thin, and thick2 .
everywhere U P hfi hhfii tt = tt
everywhere I P hfi hhfii d = ind P hfi hhfii d –– apply ind to rec. pos.
3.2 Occur Check
everywhere (G1 ⊕ G2 ) P hfi hhfii (inj1 d) = everywhere G1 P hfi hhfii deverywhere (G1 ⊕ G2 ) P hfi hhfii (inj2 d) = everywhere G2 P hfi hhfii dUsing thick, we can define a function check that performs the occur
everywhere (G1 ⊗ G2 ) P hfi hhfii (d1 , d2 ) =check. Since we want to prove both the soundness and complete(everywhere G1 P hfi hhfii d1 , everywhere G2 P hfi hhfii d2 )ness of type inference, the occur check not only returns whether avariable occurs in a data, but also its proof.

ind : {F : Code} → {m : N} → (P : µ F m → Set) →(hfi : (d : [[ F ]] (µ F m)) → [[ F ]]0 P d → P h d i) →(hhfii : (x : Fin m) → P hh x ii) → (t : µ F m) → P t
ind {F} P hfi hhfii h d i = hfi d (everywhere F P hfi hhfii d)
ind {F} P hfi hhfii hh x ii = hhfii x

check : {F : Code} → {m : N} →(x : Fin (suc m)) → (t : µ F (suc m)) →(Σ[ C ∈ Context F (µ F (suc m)) ] plug C hh x ii ≡ t)
] (Σ[ t0 ∈ µ F m ] hhcataii (hh_ii ◦ thin x) t0 ≡ t)

If a metavariable x occurs in a type t, check x t returns a context
that, when filled with the variable, becomes the type t, showingthat x actually occurs in t. The definition of Context and plug arestandard and omitted; we extend (McBride 2003b) to cope withgeneric data. If a metavariable x does not occur in a type t, on theother hand, we can thicken the metavariables in t at x to produce
a type t0 with one less metavariables. The original term t is thenexpressed as thinning t0 at x, ensuring that x does not actually occur
in t.

The second one defines the induction principle that proves that ageneric data t satisfies a predicate P.

3.

First-order Unification, Generically

During type inference, types (possibly containing metavariables)
are unified to satisfy type constraints present in the typing rules.
To implement unification in type theory where all function mustterminate, McBride (2003) presented a unification algorithm that is
structurally recursive and hence is guaranteed to terminate.
3.1

check {F} {m} x t =ind (ń t → (Σ[ fs ∈ Context F (µ F (suc m)) ] plug fs hh x ii ≡ t)
] (Σ[ t0 ∈ µ F m ] cata h_i (hh_ii ◦ thin x) t0 ≡ t))(hchecki F x) (hhcheckii x) t

Thick

McBride’s key observation is that whenever a metavariable is instantiated, the number of (uninstantiated) metavariables reduces by
one. To reduce the number of metavariables, we first define a function thick. It receives two arguments, x and y (of type Fin (sucm)), and checks whether they differ. When they do, it ‘thickens’
the number y at position x. Intuitively speaking, x represents themetavariable to be instantiated (and removed) and y is some othermetavariable. Then, thick x y returns a new y (of type Fin m) after x
is removed. Mathematically, it is defined as follows, where nothing
and just are the two constructors of Agda’s Maybe (option) type.
 just y(y < x)nothing(y = x)thick x y = just (y − 1) (y > x)

The occur check is implemented by ind, using two functions,hchecki and hhcheckii, that take care of the pattern functor case andthe metavariable case, respectively. The former simply traverses thegeneric data recursively to propagate the result of recursive positions to the call site. It is somewhat lengthy but can be straightforwardly defined, following the recursive structure of everywhere.
The real occur check is done in hhcheckii, using thick2 .
hhcheckii : {F : Code} → {m : N} → (x y : Fin (suc m)) →(Σ[ C ∈ Context F (µ F (suc m)) ] plug {F} C hh x ii ≡ hh y ii)] (Σ[ t0 ∈ µ F m ] hhcataii (hh_ii ◦ thin x) t0 ≡ hh y ii)
hhcheckii x y with thick2 x y... | inj1 x≡y = inj1 ([] , (cong hh_ii x≡y)) –– x occurs in y... | inj2 (y0 , thinxy0 ≡y) = inj2 (hh y0 ii , (cong hh_ii thinxy0 ≡y))For example, suppose that TypeEx3 in Section 2 is obtained as aresult of instantiating the metavariable hh suc zero ii (and hence themetavariable hh suc zero ii is not present in TypeEx3 ). Since hh suczero ii is no longer used and is removed, we want to decrease thenumber of metavariables from three to two. To do so, we rename
the metavariable bigger than hh suc zero ii by its predecessor. In
other words, we apply thick hh suc zero ii to all the metavariables
in TypeEx3 . The result becomes as follows.

3.3

Substitution

We next define substitution. Following McBride (2003), we represent substitution as a snoc list.
data AList (F : Code) : (l m : N) → Set whereanil : {m : N} → AList F m m –– empty substitution_asnoc_/_ : {l m : N} → (σ : AList F l m) → (t : µ F l) →(x : Fin (suc l)) → AList F (suc l) m –– maps x to t before σ

TypeEx5 : µ TypeF 2
TypeEx5 = (TUnit ⇒ hh suc zero ii) ⇒ hh zero ii

When a substitution σ is applied to a type t, σ replaces metavariables in t one by one, reducing the number of metavariables int. The type AList F l m represents a substitution that transformsa type with l metavariables to a type with m metavariables. The

Observe that hh zero ii remains the same as in TypeEx3 , but hh suc(suc zero) ii is changed to hh suc zero ii, and both the metavariables
have type Fin 2.

4

2020/9/30

empty substitution anil does not change the number of metavariables, and hence has type AList F m m. On the other hand, σ asnoc
t / x replaces the metavariable x with t, thus reducing the numberof metavariables by one, before applying the rest of the substitution
σ. From the definition of AList, we can easily show that wheneverσ has type AList F l m, l must be equal to or greater than m.
We can append two substitutions, ρ and σ, to obtain ρ ++ σ,which applies σ first, followed by ρ.

σ0

l0
l

m0

l≤l0

σ
m

ρ

l
n

σ

ρ
n

m≤m0
m

Figure 2. Concatenation of two substitutions, σ and ρ. When thenumbers of metavariables match, they can be appended directly (ρ++ σ, left). When new metavariables are allocated between thetwo substitutions, we need lifting of σ (ρ +h para i σ, right, wherepara is a proof term for l≤l0 // m≤m0 and σ 0 is liftAList≤ paraσ).

_++_ : {F : Code} → {l m n : N} →(ρ : AList F m n) → (σ : AList F l m) → AList F l nρ ++ anil = ρρ ++ (σ asnoc t / x) = (ρ ++ σ) asnoc t / x

Observe the numbers of metavariables exhibit transitivity, if weinterpret AList F l m as m ≤ l. See Figure 2 (left).
When we implement type inference, we will need to lift the
number of metavariables of a substitution, too. Suppose we havea data with l metavariables and a substitution σ of type AList F lm that reduces the number of metavariables from l to m. Suppose
further that we want to introduce k new metavariables, resulting
in k + l metavariables in total. To apply σ to the resulting data,
we first need to lift σ so that it can accept k + l metavariables.
Since σ operates on the first l metavariables only, σ should leave
the new k metavariables intact. In other words, after lifting, we needa substitution that reduces the number of metavariables from k + l
to k + m, where the new k metavariables remain the same. We canactually define a function that has such a type:

Introducing another variable with an equality constraint (as we
did for liftAList0 ) is not a good idea, because it does not liberate
us from managing the subtraction formula. What we really want
to do is to introduce inequality constraints for both l and m, while
maintaining the dependency between them. For this purpose, we
introduce the following inductive relation between two inequalities.
data _//_ : {l l0 m m0 : N} → l ≤ l0 → m ≤ m0 → Set where
Refl : {m m0 : N} → (m≤m0 : m ≤ m0 ) → m≤m0 // m≤m0
Step : {l l0 m m0 : N} → {l≤l0 : l ≤ l0 } →{m≤m0 : m ≤ m0 } → l≤l0 // m≤m0 → s≤s l≤l0 // m≤m0

Two inequalities, l≤l0 and m≤m0 where l is greater than or equal tom, are in parallel, written l≤l0 // m≤m0 , when their differences are. m. The first constructor says that an. l = m0 −the same, i.e., l0 −
inequality is in parallel to itself. The second constructor says thatwhen two inequalities are in parallel, we obtain another parallel
inequalities by adding 1 to both sides of the first inequality. The
constructor s≤s adds 1 to both sides of the argument inequality. Ifl≤l0 and m≤m0 are in parallel, we have that l0 is greater than orequal to m0 by the same amount as l and m. Intuitively, l, m, l0 , andm0 form a parallelogram as illustrated in Figure 2 (right).
Using this relation, we can finally define the lifting function for
substitutions that is sufficiently easy to use.

liftAList : {F : Code} → {l m : N} → (k : N) →(σ : AList F l m) → AList F (k + l) (k + m)

However, as we saw for the function lift≤ in Section 2, applicabilityof this function is severely restricted, because we have to not only
specify the number k by ourselves but also adjust the number of
metavariables manually in the return type of the function to be
exactly in the forms k + l and k + m.
It is in general not a good idea to unnecessarily constrain the
return type of a function. McBride (2014, Section 4) made a similar
observation. To avoid the problem, we can introduce new variables
together with constraints they have to satisfy.

liftAList≤ : {F : Code} → {l l0 m m0 : N} →{l≤l0 : l ≤ l0 } → {m≤m0 : m ≤ m0 } → l≤l0 // m≤m0 →(σ : AList F l m) → AList F l0 m0

liftAList0 : {F : Code} → {l l0 m m0 : N} → (k : N) →l0 ≡ k + l → m0 ≡ k + m → (σ : AList F l m) → AList F l0 m0

We can lift a substitution σ from AList F l m to AList F l0 m0 ,when l≤l0 and m≤m0 are in parallel. Notice that the conclusion of
the definition does not impose any restriction on the numbers of
metavariables and that it does not contain any complex formula.
All the necessary constraints are embedded in the parallel relationof two inequalities.
The definition of liftAList≤ in terms of the parallel relation
between two inequalities is one of the technical contributions of
this paper. It not only avoids manual replacement of a type of aterm, but also keeps the necessary constraints on the number of
metavariables minimally. Without the definition of liftAList≤, it
would have been impossible to describe type inference in the formof typing rules (as we show in Section 5) while showing all the finedetails of the number of metavariables.
Using liftAList≤, we can define more flexible version of thesubstitution concatenation that lifts the second substitution (the onethat is applied first) before concatenation, which we use in thesubsequent development.

With this definition, we do not have to adjust the return type of thefunction manually, but we are given separate constraints that we
can satisfy later with the help of Agda type checker.
However, there still remains a problem that we have to specify
the number k explicitly. Since the required number of new metavariables varies depending on which kind of terms we are working
on, the need to explicitly specify the number k disturbs the structure of the proofs with unnecessary calculation of the number of
metavariables. However, the exact number of new metavariables ineach case is not important. We just allocate some metavariables asneeded. Thus, what we really want to express is the inequality.
liftAList≤0 : {F : Code} → {l m m0 : N} → (m≤m0 : m ≤ m0 ) →. m) + l) m0(σ : AList F l m) → AList F ((m0 −Instead of specifying the difference k, we supply an inequalitym ≤ m0 and state that we lift the number of metavariables fromm to m0 . This definition liberates us from keeping the number of
metavariables exactly. In return, however, it requires us to handle a. m) + l, where m0 −. m represents
rather complex formula (m0 −subtraction on natural numbers, i.e., the result becomes 0 if m
is greater than m0 . The formula arises because l and m are notindependent. If m is raised to m0 , l must be raised the amount. m.
exactly the same as m is raised, namely, m0 −_+h_i_ : {F : Code} → {l m l0 m0 n : N} →{l≤l0 : l ≤ l0 } → {m≤m0 : m ≤ m0 } →(ρ : AList F m0 n) → l≤l0 // m≤m0 → (σ : AList F l m) →AList F l0 n
ρ +h para i σ = ρ ++ liftAList≤ para σ

52020/9/30

In this definition, m0 in the type of ρ does not have to be exactly thesame as m in the type of σ, as long as m0 is greater than or equal tom. Within the angle brackets, we specify the parallel relation thatmust hold to connect the two substitutions. Note that the numbers of
metavariables still exhibit transitivity, intertwined with the parallel
relation, as depicted in Figure 2.
3.4(Σ[ k00 ∈ N ] Σ[ m0 ≤k00 ∈ m0 ≤ k00 ] Σ[ para ∈ m≤l00 // m0 ≤k00 ]Σ[ f0 ∈ (Fin k00 → µ F l0 ) ]((x : Fin m) →f (inject≤ x m≤l00 ) ≡ (f0 +h para i0 g) (inject≤ x m≤l00 ))))

There are two subtle points in this definition. First, it includes
many lifting operations to account for possible allocation of new
metavariables. In particular, the number of metavariables of the
input of f and f0 are set in a least restrictive way. Second, and more
importantly, the decomposition of f is considered only for the firstm metavariables, i.e., the metavariables appearing in t1 and t2 . By
restricting the considered case to the first m metavariables only,
we obtain flexibility in choosing f0 . The same technique is used by
Leroy (1992, page 28).
The function mgu is defined using a helper function amgu
written in the accumulator passing style.

Unifier

To apply a substitution to a generic data, we first turn the substitution into a unifier, an Agda function from metavariables to genericdata.
sub : {F : Code} → {m m0 : N} →(σ : AList F m m0 ) → Fin m → µ F m0
sub anil = hh_ii
sub (σ asnoc t / x) = hhcataii (sub σ) ◦ (t for x)

mgu t1 t2 with amgu t1 t2 anil... | inj1 f rewrite hh-ii-id t1 | hh-ii-id t2 = inj1 f... | inj2 (m0 , σ , mgσ) rewrite hh-ii-id t1 | hh-ii-id t2 = inj2 (m0 , σ , mgσ)

It decomposes a substitution, turns each element to an Agda function, and composes the results using the function composition operator ◦. Here, t for x is a function that maps a metavariable y to t if
y is equal to x, and otherwise thickens y.

Here, hh-ii-id asserts that applying an empty unifier cancels out.

_for_ : {F : Code} → {m : N} →(t : µ F m) → (x : Fin (suc m)) → Fin (suc m) → µ F m(t for x) y with thick x y... | nothing = t –– x = y... | just y0 = hh y0 ii –– y is thickened to y0

hh-ii-id : {F : Code} → {m : N} → (t : µ F m) → hhcataii hh_ii t ≡ t

In the following, we do not explain this kind of rewrite rules that areneeded to go through the proof but whose contents are unimportant.
Starting from the empty substitution, amgu accumulates necessary
substitution by traversing over the given data.

Once a substitution is turned into a unifier, we can use hhcataii toapply it to all the metavariables in a data. Since we often want to lift
the number of metavariables before applying a unifier, it is handy
to define the following three functions.

amgu : {F : Code} → {m m0 : N} → (t1 t2 : µ F m) →(ρ : AList F m m0 ) →ununifiable (applySub ρ t1 ) (applySub ρ t2 )] (Σ[ m00 ∈ N ] Σ[ σ ∈ AList F m0 m00 ]mg (applySub ρ t1 ) (applySub ρ t2 ) (sub σ))amgu t1 t2 anil
rewrite hh-ii-id t1 | hh-ii-id t2 = amguAnil t1 t2amgu t1 t2 (ρ asnoc t / x)with amgu (hhcataii (t for x) t1 ) (hhcataii (t for x) t2 ) ρ... | inj1 frewrite fuse (sub ρ) (t for x) t1 | fuse (sub ρ) (t for x) t2= inj1 f... | inj2 (m00 , σ 0 , mgσ 0 )rewrite fuse (sub ρ) (t for x) t1 | fuse (sub ρ) (t for x) t2= inj2 (m00 , σ 0 , mgσ 0 )hhcataii≤ hhfii m≤m00 t = hhcataii hhfii (lift≤ m≤m00 t)
applySub σ t = hhcataii (sub σ) tapplySub≤ σ m≤m00 t = applySub σ (lift≤ m≤m00 t)

3.5

Unification

We are now ready to define unification.
mgu : {F : Code} → {m : N} → (t1 t2 : µ F m) →ununifiable t1 t2] (Σ[ m0 ∈ N ] Σ[ σ ∈ AList F m m0 ] mg t1 t2 (sub σ))

The function mgu takes two data, t1 and t2 , both with m metavariables, and returns either a proof that t1 and t2 are not unifiable ora unifying substitution σ together with the proof that sub σ is themost general unifier for them.
Two data t1 and t2 are ununifiable, when there exists no unifierthat unifies them.

The function amgu is defined by induction on m, or equivalently,
the length of the substitution in the accumulator. When m is positive(i.e., when the substitution has the form σ asnoc t / x), we canreduce the number of metavariables by substituting t for x in t1 andt2 . Note that because of the substitution, the sizes of t1 and t2 canbecome bigger than before. This is where the standard terminationargument fails. We can make a recursive call here, because we keep
track of the number of metavariables that is strictly decreasing.
When m is zero (when the substitution is empty), amgu delegate
the task to amguAnil.

ununifiable : {F : Code} → {m : N} → (t1 t2 : µ F m) → Set
ununifiable {F} {m} t1 t2 =(l0 l00 : N) → (m≤l00 : m ≤ l00 ) → (f0 : Fin l00 → µ F l0 ) →¬ (hhcataii≤ f0 m≤l00 t1 ≡ hhcataii≤ f0 m≤l00 t2 )Note that we consider not only unifiers for m metavariables but
also any unifiers that accept more than m metavariables. We haveto take such unifiers into account, because they arise as the resultof introducing new metavariables during type inference.
A unifier g is the most general unifier for t1 and t2 , if (1) g
unifies t1 and t2 and (2) any unifier f that unifies t1 and t2 can be
represented as the composition of some f0 and possibly lifted g forany x in the first m metavariables.

amguAnil : {F : Code} → {m : N} → (t1 t2 : µ F m) →ununifiable t1 t2] (Σ[ m00 ∈ N ] Σ[ σ ∈ AList F m m00 ] mg t1 t2 (sub σ))amguAnil {F} h d1 i h d2 i with amgu0 F d1 d2 anil... | inj1 f rewrite fmap-id F d1 | fmap-id F d2
= inj1 (ununifiable-hdi d1 d2 f)... | inj2 (m0 , σ 0 , mgσ 0 ) rewrite fmap-id F d1 | fmap-id F d2
= inj2 (m0 , σ 0 , mg-hdi d1 d2 (sub σ 0 ) mgσ 0 )amguAnil h d1 i hh x2 ii with flexRigid x2 d1... | inj1 f = inj1 (ununifiable-sym h d1 i hh x2 ii f)... | inj2 (m0 , σ 0 , mgσ 0 ) =inj2 (m0 , σ 0 , mg-sym h d1 i hh x2 ii (sub σ 0 ) mgσ 0 )amguAnil hh x1 ii h d2 i with flexRigid x1 d2... | inj1 f = inj1 f

mg : {F : Code} → {m m0 : N} → (t1 t2 : µ F m) →(g : Fin m → µ F m0 ) → Set
mg {F} {m} {m0 } t1 t2 g =(hhcataii g t1 ≡ hhcataii g t2 ) ×((l0 l00 : N) → (f : Fin l00 → µ F l0 ) → (m≤l00 : m ≤ l00 ) →(hhcataii≤ f m≤l00 t1 ≡ hhcataii≤ f m≤l00 t2 ) →6

2020/9/30

... | inj2 (m0 , σ 0 , mgσ 0 ) = inj2 (m0 , σ 0 , mgσ 0 )amguAnil {m = m} hh x1 ii hh x2 ii with flexFlex m x1 x2... | (m0 , σ 0 , mgσ 0 ) = inj2 (m0 , σ 0 , mgσ 0 )The second and the third cases require careful proofs, which follows McBride (2003b) but extended to handle generic data. See
accompanying code for details.

When the accumulator is empty, amguAnil dispatches over the
shapes of t1 and t2 . We examine each case starting from the bottom. When both are metavariables (the fourth case), we return asubstitution that unifies the two metavariables using flexFlex.

3.6

Concise Notation for Unification

Once we define the unification function, we do not have to remember all its internal workings. Instead, we pay attention only to how
the number of metavariables changes, in addition to the standard
behavior of unification, i.e., that it produces a unifying substitution. As a preparation for expressing type inference in the form oftyping rules, we introduce a concise notation for unification.
(m) .
(m)
σ[↓m
) = σ[↓m)m0 ](t1
m0 ](t2

flexFlex : {F : Code} → (m : N) → (x1 x2 : Fin m) →(Σ[ m0 ∈ N ] Σ[ σ ∈ AList F m m0 ] mg hh x1 ii hh x2 ii (sub σ))
flexFlex zero () x2
flexFlex (suc m) x1 x2 with thick2 x1 x2... | inj1 x1 ≡x2 rewrite x1 ≡x2 = (suc m , anil , mgAnil hh x2 ii)... | inj2 (x2 0 , thinx1 x2 0 ≡x2 ) rewrite sym thinx1 x2 0 ≡x2 =(m , anil asnoc hh x2 0 ii / x1 , mgFor x1 hh x2 0 ii)

This equation expresses that two terms, t1 and t2 both with m
metavariables, can be unified by the substitution σ[↓mm0 ]. The notation [↓mm0 ] after σ signifies that the substitution reduces the numberof metavariables from m to m0 . The inputs to the equation are t1 ,t2 , and m (written in blue), and the outputs are m0 and σ (written
in red).2 The above notation precisely and concisely captures thetype of mgu including the property the returned substitution satis.
fies: the = sign indicates that the substitution unifies the two input
terms.

When the two metavariables are the same, we return the empty substitution, together with mgAnil hh x2 ii stating that the empty substitution is the most general for the same data. Otherwise, we returna substitution that unifies one of the metavariables to the thickened
version of the other, reducing the number of metavariables by one.
The proof mgFor x1 hh x2 0 ii states that anil asnoc hh x2 0 ii / x1 is
the most general substitution for the two. (See accompanying codefor completeness-related functions, such as amguAnil and mgFor,
that are mostly omitted in the paper due to the lack of space.) We
arbitrarily chose to map x1 to hh x2 0 ii, but we could do the otherway around.
When exactly one of the two data is a metavariable (the second and the third cases), we return a substitution that unifies themetavariable to the other data using flexRigid.

4.

Well-scoped and Well-typed Terms

The input to the type inference is an untyped term. We assume thatthe input term is closed and does not contain any free variables. We
define such terms using de Bruijn index.

flexRigid : {F : Code} → {m : N} → (x : Fin m) → (d : [[ F ]] (µ F m)) →ununifiable {F} hh x ii h d i] (Σ[ m’ ∈ N ] Σ[ σ ∈ AList F m m’ ] mg hh x ii h d i (sub σ))
flexRigid {m = zero} () dflexRigid {m = suc m} x d with check x h d i... | inj1 ([] , ())... | inj1 (f :: fs , eq) = inj1 (occurred f fs x d eq) –– x occurs in h d i... | inj2 (t0 , eq) with mgFor x t0... | mg-t0 forx rewrite eq = inj2 (m , anil asnoc t0 / x , mg-t0 forx)

If the metavariable occurs in the data, there is no unifying substitution. We show there is no unifier using occurred, in a way similar to
McBride (2003b). This is one of the two cases where the unification
fails. Otherwise, it returns a substitution.
Finally, the first case is when both the data are not metavariables. This case is handled by calling amgu0 and lift the result on
d1 and d2 to h d1 i and h d2 i. We do not show the code for amgu0 ,which is written as a straightforward induction similar to everywhere, but only note that it requires us to propagate the results on
subparts up to the whole data along the following line.

data WellScoped (n : N) : Set where
Unit : WellScoped n
Var : (x : Fin n) → WellScoped n
Lam : (s1 : WellScoped (1 + n)) → WellScoped n
App : (s1 s2 : WellScoped n) → WellScoped n

The argument n of WellScoped indicates how many binders theterm is under. The number increases whenever we go into the bodyof Lam. The closedness condition is guaranteed by representing avariable as a number from 0 to n − 1.
The output of the type inference is a typed term. We first fix thesimple types as follows using the pattern functor TypeF defined in
Section 2.
Type : (m : N) → Set
Type m = µ TypeF m

It is a type of simple types that have at most m metavariables.
Since we use de Bruijn index, the type environment is represented as a vector of types:
Cxt : {m : N} → N → Set
Cxt {m} n = Vec (Type m) n

• If one of the subparts is ununifiable, the whole data is ununifi-

where Vec A n is a type of vectors of length n (with the constructors[] and ::) whose elements have type A.
We then define WellTyped Γ t, the type of well-typed terms oftype t under Γ, using the same constructors as the well-scoped
terms. (Agda allows sharing of constructors between different
types. No ambiguity arises because all the Agda terms are explicitly
typed.)

able.
• If all the subparts return the most general unifiers, we canconstruct the most general unifier for the whole data.
These guidelines cover the cases for U, I, and ⊕. For products, weneed some more consideration.
• If the first projection is ununifiable, the whole product is un-data WellTyped {m n : N} (Γ : Cxt n) : Type m → Set where
Unit : WellTyped Γ TUnit
Var : (x : Fin n) → WellTyped Γ (lookup x Γ)
Lam : {t1 : Type m} → (t2 : Type m) →(w1 : WellTyped (t2 :: Γ) t1 ) → WellTyped Γ (t2 ⇒ t1 )unifiable. This case can be easily shown.
• If the second projection is ununifiable, the whole product isununifiable, provided that the first projection returns the mostgeneral unifier. (If the first projection unnecessarily instantiates
metavariables, it could make the second projection ununifiable.)• If both the projections returns the most general unifier, we can

2 We will write which are the inputs and which are the outputs explicitly incompose the most general unifier for the pair.

the main text. However, it is easier to read if the paper is printed in color.

7

2020/9/30

metavariables during type inference of s. Since we already use mmetavariables before the type inference of s begins, m00 must be atleast as big as m. This inequality is returned as the third element.
The second element m0 represents the number of metavariables
when the type inference of s finishes. The fourth element σ is thesubstitution required to infer the type of s. It reduces the numberof metavariables from m00 to m0 . The fifth element t is the inferred
type of s, which has m0 metavariables. The sixth element is the welltyped term w that we want to obtain. Since some metavariables mayneed to be instantiated to type check s, however, w is a well-typed
term of type t not under the original type environment Γ, but Γ after
applying σ. In the type of w, the function applySubCxt≤ applies agiven substitution σ to all the types in Γ after lifting the number of
metavariables of Γ from m to m00 . The seventh element shows thatthe obtained w is not an arbitrary well-typed term but actually thewell-typed version of s. Finally, the last element is the proof thatthe obtained type and substitution are the most general ones for s.
In this paper, we express the soundness parts (i.e., the parts otherthan untypability proofs and generality proofs) of the type inferencefunction infer as the following typing rule.

App : {t1 t2 : Type m} → (w1 : WellTyped Γ (t2 ⇒ t1 )) →(w2 : WellTyped Γ t2 ) → WellTyped Γ t1

where lookup x Γ is the x’th element of Γ. This type embodies thetyping rules of simply-typed λ-calculus. It consists of only welltyped terms.
Given a well-scoped term, the task of type inference is to find acorresponding well-typed term, if it exists. To relate the input andoutput of type inference, we can easily define a relation between awell-typed term and the corresponding well-scoped term obtainedby stripping off the type information.
data erase {m n : N} : {t : Type m} → {Γ : Cxt n}(w : WellTyped Γ t) → (s : WellScoped n) → Set

We define erase as a relation rather than a function, because wesometimes want to guess the shape of the well-typed term corresponding to a well-scoped term.

5.

Type Inference

To formalize type inference, we first specify the properties it should
satisfy. We define untypable Γ s, meaning that s is not typable
under Γ, as follows.

00

00

0

m
(m)
) ` s : t(m )σ[↓mm0 ](↑m Γ

untypable : {m n : N} → (Γ : Cxt {m} n) → (s : WellScoped n) → Set
untypable {m} Γ s =(l00 l0 : N) → (m≤l00 : m ≤ l00 ) → (f0 : Fin l00 → Type l0 ) →(t0 : Type l0 ) → (w0 : WellTyped (applyFunCxt≤ f0 m≤l00 Γ) t0 ) →¬ erase w0 s

The inputs to the type inference are Γ, s, and m (written in blue),
while the outputs are m00 , m0 , σ, and t (written in red). The other
outputs of infer are represented in the judgement as follows. The
00
inequality m≤m00 is implicitly shown as the lifting operator ↑mm
00
applied to Γ, which is possible because m≤m . It lifts the numberof metavariables of all the types in Γ. The well-typed term w
is represented by the whole judgement: under σ-applied Γ, theterm s is well typed and has type t. Finally, the erasure property
is expressed by the fact that the judgement can be regarded asa well-scoped judgement if we remove the type parts. Thus, theabove notation expresses precisely and concisely all the soundness
properties of infer.
The function infer is defined by induction on terms.

We then define mgt σ Γ s t, meaning that σ gives the most general
type t for s under Γ.
mgt : {m m0 m00 n : N} → (σ : AList TypeF m00 m0 ) →(Γ : Cxt {m} n) → (s : WellScoped n) → (t : Type m0 ) → Set
mgt {m} {m0 } {m00 } σ Γ s t =(l000 l0 : N) → (m≤l000 : m ≤ l000 ) →(f0 : Fin l000 → Type l0 ) → (t0 : Type l0 ) →(w0 : WellTyped (applyFunCxt≤ f0 m≤l000 Γ) t0 ) →erase w0 s →Σ[ k00 ∈ N ] Σ[ k000 ∈ N ] Σ[ m0 ≤k00 ∈ m0 ≤ k00 ]Σ[ m00 ≤k000 ∈ m00 ≤ k000 ] Σ[ para ∈ m00 ≤k000 // m0 ≤k00 ]Σ[ m≤k000 ∈ m ≤ k000 ] Σ[ f0 ∈ (Fin k00 → Type l0 ) ](((x : Fin m) →f0 (inject≤ x m≤l000 ) ≡(f0 +h para i0 (sub σ)) (inject≤ x m≤k000 )) ×t0 ≡ applyUnifier≤ f0 m0 ≤k00 t)

infer m Γ Unit = infer-Unit m Γinfer m Γ (Var x) = infer-Var m Γ xinfer m Γ (Lam s1 ) = infer-Lam m Γ s1
infer m Γ (App s1 s2 ) = infer-App m Γ s1 s2

Below, we will examine each case in turn. Figure 3 precisely summarizes all the cases in the form of typing rules.
5.1

The definition is long, but it reads: if there exists a unifier f0 thatgives a type t0 for s under Γ, then f0 and t0 are instantiations of sub
σ and t, respectively. To be more precise, we can find f0 such that

Unit

The type inference for the unit case becomes as follows:
infer-Unit : (m : N) → {n : N} → (Γ : Cxt {m} n) →untypable Γ Unit
] Σ[ m00 ∈ N ] Σ[ m0 ∈ N ] Σ[ m≤m00 ∈ m ≤ m00 ]Σ[ σ ∈ AList TypeF m00 m0 ] Σ[ t ∈ Type m0 ]
Σ[ w ∈ WellTyped (applySubCxt≤ σ m≤m00 Γ) t ](erase w Unit × mgt σ Γ Unit t)infer-Unit m Γ =inj2 (m , m , m≤m , anil , TUnit , Unit , Unit , mg-Unit)• f0 is the composition of sub σ and f0 , possibly with lifting, and• t0 is obtained by applying f0 to t, possibly with lifting.

We are now ready to formalize type inference. The type inference function we are going to construct has the following type.
infer : (m : N) → {n : N} → (Γ : Cxt {m} n) → (s : WellScoped n) →untypable Γ s] Σ[ m00 ∈ N ] Σ[ m0 ∈ N ] Σ[ m≤m00 ∈ m ≤ m00 ]Σ[ σ ∈ AList TypeF m00 m0 ] Σ[ t ∈ Type m0 ]
Σ[ w ∈ WellTyped (applySubCxt≤ σ m≤m00 Γ) t ](erase w s × mgt σ Γ s t)

where m≤m is a proof term for m being (less than or) equal to itself. The type of infer-Unit is obtained by instantiating s in the typeof infer to Unit. Since we need neither allocation of new metavariables nor substitution for the unit case, the numbers of metavariables become both m and the substitution is empty. The returned
type is TUnit. Since Unit is well typed in any type environments, ittrivially has the required type WellTyped (applySubCxt≤ σ m≤mΓ) TUnit, whose erasure is also trivially Unit as required.
Completeness can be easily shown since the empty substitution
unifies two (identical) Units and any unifiers are composition of

Given a type environment Γ that has m metavariables and a wellscope term s, the function infer returns either a proof that s isuntypable under Γ or (roughly) a well-typed term w as a proof thatthe input term s is well typed.
To be more precise, infer returns a tuple of eight elements in thelatter case. The first element m00 represents the number of required

8

2020/9/30

m (m)φ[↓m) ` • : unit(m)m ](↑m Γ
00

Γ(m) (x) = t(m)(IUnit)m (m)φ[↓m) ` x : t(m)m ](↑m Γ000m
1+m (m)σ[↓mΓ ), x : m(1+m) )(1+m) ) ` s1 : t1 (m )m0 ](↑1+m ((↑m
00

00

00

(IVar)

m(1+m) is a new metavariable

00

0

m
(m)
m
(1+m)
σ[↓m
) ` λx. s1 : σ[↓m
) → t1 (m )m0 ](↑m Γ
m0 ](↑1+m m
1+m02

σ3 [↓m0

1+m02

](↑m0

2

3

1+m02

σ3 [↓m0

1+m02

](↑m0

2

3

1+m02

σ3 [↓m0

1+m02

](↑m0

m00

m00

2

1

1

m00

m00

m00

2

1

1

3

1+m000
2

](↑m

m00

0

0

0
0
.
1+m0
1+m0
m00
m00
(1+m02 ))(σ2 [↓m20 ](↑m20 t1 (m1 ) ))) = σ3 [↓m0 2 ](↑m0 2 t2 (m2 ) → m02

000
m001 ≤ m000
2 // m1 ≤ m2
1+m02Γ) = σ3 [↓m0

3

1+m0002σ321 [↓m0

3

2

3

1

0

1+m0002

0` s1 : t1 (m1 ) )))σ2 [↓m20 ](↑m20 (σ1 [↓m10 ](↑m1 Γ(m) ))(m1 ) ) ` s2 : t2 (m2 ) )(1+m2 )
m02
is a new metavariable

σ321 [↓m0m00(σ2 [↓m20 ](↑m20 σ1 [↓m10 ](↑m1 Γ(m) )

2

2

3

m00

(ILam)

1+m02

](↑m0

2

1+m000
2

](↑m

000
0
0
m000
2 ≤ 1 + m2 // m2 ≤ 1 + m2

m00

m00

2

1

m00

m00

(σ2 [↓m20 ](↑m20 (σ1 [↓m10 ](↑m1 Γ)))))
1

1+m02

Γ(m) ) ` s1 s2 : σ3 [↓m0

3

](m02

(1+m02 )(IApp))

Figure 3. Type inference rules
To infer the type of an abstraction λx. s1 , we infer recursively
the type of its body s1 . To do so, however, we need to assign a yet
unknown type to the argument x. For this purpose, we allocate a
new metavariable m(1+m) . The current number m of metavariables
indicates that we have used the metavariables from 0 to m − 1 so
far. Thus, the next available metavariable is m.3
Because we allocate a new variable, the number of metavariables is increased by one. To accommodate it, we lift the number of
metavariables of Γ by one. Now that both ↑1+m
Γ(m) and m(1+m)
mhave 1 + m metavariables, we can form an extended type environment (↑1+m
Γ(m) ), x : m(1+m) . We infer the type of s1 under thismtype environment.
When the type inference of s1 finishes, we obtain the type t1
of s1 and a substitution σ together with a number m00 of required
metavariables to infer t1 and the final number m0 of metavariables.
They together satisfy the judgement in the premise of (ILam).
Because application of a substitution to a type environment iselement wise, we can rewrite the type environment in the premiseof (ILam) as follows.

itself and the empty substitution. It is shown in the omitted codemg-Unit.
This case is summarized as (IUnit) in Figure 3, where φ stands
for the empty substitution.
5.2

Variable

The type inference for the variable case becomes as follows:
infer-Var : (m : N) → {n : N} → (Γ : Cxt {m} n) → (x : Fin n) →untypable Γ (Var x)] Σ[ m00 ∈ N ] Σ[ m0 ∈ N ] Σ[ m≤m00 ∈ m ≤ m00 ]Σ[ σ ∈ AList TypeF m00 m0 ] Σ[ t ∈ Type m0 ]
Σ[ w ∈ WellTyped (applySubCxt≤ σ m≤m00 Γ) t ](erase w (Var x) × mgt σ Γ (Var x) t)
infer-Var m Γ x =inj2 (m , m , m≤m , anil , t , VarX , eq , mg-Var x)
wheret : Type mt = lookup x Γ

Again, we need neither allocation of new metavariables nor substitution. The returned type t is found in the type environment. The
well-typed term VarX (whose definition is omitted) is almost Var
x of type WellTyped Γ t. However, the required type for the welltyped term is WellTyped (applySubCxt≤ anil m≤m Γ) t. Thus,
we need to show that applySubCxt≤ anil m≤m Γ and Γ are thesame, which can be easily proved by induction on Γ.
Completeness is again easy to show (using mg-Var, omitted),
because any unifiers are composition of itself and the empty substitution.
This case is summarized as (IVar) in Figure 3. The required
property can be written in mathematical form as follows:

00

00

00

00

1+m
By fusing the two lifting operations ↑m·) into one ↑m
1+m (↑mm·, it is further rewritten to the following.
00

00

00

00

00

m
(m)
m
(1+m)
σ[↓m
), x : σ[↓m)m0 ](↑m Γ
m0 ](↑1+m m

We can then obtain the conclusion of (ILam) using (TLam).
By transcripting the above scenario, we can define infer-Lam as
follows.
infer-Lam : (m : N) → {n : N} →(Γ : Cxt {m} n) → (s1 : WellScoped (1 + n)) →untypable Γ (Lam s1 )] Σ[ m00 ∈ N ] Σ[ m0 ∈ N ] Σ[ m≤m00 ∈ m ≤ m00 ]Σ[ σ ∈ AList TypeF m00 m0 ] Σ[ t ∈ Type m0 ]
Σ[ w ∈ WellTyped (applySubCxt≤ σ m≤m00 Γ) t ](erase w (Lam s1 ) × mgt σ Γ (Lam s1 ) t)

m (m)
φ[↓m
) = Γ(m)m ](↑m ΓWith this equation, (IVar) becomes identical to (TVar) ensuringthat the obtained term is well typed.
5.3

00

m
1+m (m)
m
(1+m)
σ[↓m
Γ )), x : σ[↓m)m0 ](↑1+m (↑mm0 ](↑1+m m

Abstraction

3 When the current number of metavariables is m, it is always the case that

For the abstraction case, we examine the (ILam) in Figure 3 first,
because it precisely reflects (the soundness part of) the Agda codeand is easier to understand.

m is a new metavariable. Thus, the second premise of (ILam) is redundant.
We keep it for better readability. It does not mean to use a gensym-like
operator here.

9

2020/9/30

The body of infer-Lam starts by allocating a new metavariable hh
fromN m ii, which we call t2 . Here, fromN is a function to turn an
integer m to the same finite natural number m of type Fin (1 + m).

Figure 3 without sacrificing the details to reconstruct mechanizedsoundness proofs.
5.4

infer-Lam m {n} Γ s1
with lett2 : Type (1 + m)
t2 = hh fromN m ii –– new type variableΓ0 : Cxt {1 + m} n
Γ0 = liftCxt 1 Γin infer (1 + m) (t2 :: Γ0 ) s1

Application

For the application case, we again examine the (IApp) in Figure 3
first. To infer the type of s1 s2 , we first infer the type of s1 andobtain a type t1 and a substitution σ1 (the first box in the premiseof (IApp)). We then infer the type of s2 under σ1 Γ to obtain t2
and σ2 (the second box). Roughly speaking, we want to check at
this point that the type of the function part (σ2 t1 ) has the form
t2 → t for some type t. Since we do not know what t will be,
we allocate a new metavariable. Because we have already used m02
metavariables at the end of type inference of s2 , we use m02 as the
new metavariable. Now that we have allocated a new metavariable,t2 (which has m02 metavariables) must be lifted by one to adjust the
number of metavariables. Thus, t2 → t should actually be written
as follows.

We next lift the number of metavariables of Γ by one and call it Γ0 .
We then infer the type of the body s1 in the type environment Γ0extended by t2 . Note that the recursive call to infer is made with mbeing increased by one.
... | inj1 ill-s1 = –– s1 is ill-typed
inj1 (illtyped-Lam Γ s1 ill-s1 )

1+m02

0

t2 (m2 ) → m02↑m 0

If the body s1 is ill typed, the whole term is also ill typed. To
show completeness, the ill-typedness of s1 is propagated to the illtypedness of the whole term (using illtyped-Lam; one would needa clever trick to treat the newly allocated metavariable t2 specially,as shown by Nazareth and Nipkow (1996)).

2(1+m02 )The type of the function part is more complicated. First of all, t1
has m01 metavariables, but the substitution σ2 obtained later expects
a type with m002 metavariables. Thus, we need to lift t1 ’s numberof metavariables from m01 to m002 . Furthermore, after σ2 is applied,
one more metavariable (for t) is allocated. As a whole, σ2 t1 should
actually be written as follows.

... | inj2 (suc m00 , m0 , s≤s m≤m00 , σ , t1 , w1 , eraseW1 ≡S1 , mgσ) =inj2 (suc m00 , m0 , m≤1+m00 , σ , σt2 ⇒ t1 ,LamW1 , eraseLamW1 ≡LamS1 ,mg-Lam s1 t1 m≤m00 σ w1 eraseW1 ≡S1 mgσ)where
σt2 : Type m0
σt2 = applySub≤ σ (s≤s m≤m00 ) t2

1+m02

m00

m00

2

1

0

(σ2 [↓m20 ](↑m20 t1 (m1 ) ))↑m0

2

We can now unify these two types to obtain yet another substitution
σ3 .
Since types of both s1 and s2 are obtained, we then try to use(TApp) to obtain the type of s1 s2 . However, the type environmentsin the two boxes in (IApp) are not the same, because new substitutions are obtained as the type inference proceeds. To restore theirequality, we apply the substitution obtained after the type inference
to each judgement. For the judgement for s2 (the second box), σ3
was obtained afterwards, so we apply σ3 to the judgement for s2 . In
the figure, it is represented by applying σ3 to the box containing thejudgement for s2 . It expresses to apply σ3 to both the type environment and the type in the boxed judgement. As for judgement for s1(the first box), both σ2 and σ3 were obtained afterwards, which areapplied in this order to the judgement for s1 . The two judgements
now share the same environment

If s1 is well typed, we obtain a tuple with the eight elements. During
this type inference, we used metavariables as many as the recursive
call had used, namely, m00 . We have to show that it is greater than(or equal to) m. It can be easily seen from the fact that (1) 1 + m isgreater than m, (2) m00 is greater than or equal to 1 + m as the third
element of the result of the recursive call shows, and the transitivity
law. The type of the abstraction becomes σt2 ⇒ t1 which has m0
metavariables.
The returned well-typed term LamW1 of type
WellTyped (applySubCxt≤ σ m≤m00 Γ) (σt2 ⇒ t1 )is almost Lam σt2 w1 . However, like in the variable case, we haveto adjust its type, because w1 has type1+m02

σ3 [↓m0

WellTyped (applySubCxt≤ σ 1+m≤m00 (liftCxt 1 Γ)) t1

3

1+m02

m00

m00

m00

2

1

1

m00

(σ2 [↓m20 ](↑m20 (σ1 [↓m10 ](↑m1 Γ(m) )))))

](↑m0

2

with s1 having the type

and thus Lam σt2 w1 has type1+m02

σ3 [↓m0

WellTyped (applySubCxt≤ σ 1+m≤m00 (liftCxt 1 Γ)) (σt2 ⇒
t1 )

3

1+m02

](↑m0

2

m00

m00

2

1

0

(σ2 [↓m20 ](↑m20 t1 (m1 ) )))and s2 having the typewhich is different from the required type for LamW1 . We thus haveto show that the two underlined type environments in the above two
types are equal, which can be shown by induction on the structureof Γ and then by using the fusion property of liftings.
We can provide the seventh element eraseLamW1 ≡LamS1 byattaching the Lam constructor to both sides of the recursive result
eraseW1 ≡S1 , where we need to use the equality between the above
two type environments.
Finally, the completeness is shown in mg-Lam that promote thegenerality mgσ of σ for s1 to the generality for Lam s1 .
We can observe that the properties we needed to interpret Fig00
00
1+m
ure 3 (such as ↑m·) can be fused to ↑m
1+m (↑mm ·) must also be
shown in Agda. Put differently, we can reconstruct a proof in Agda,
once we precisely specify the type inference as in Figure 3. To ourknowledge, type inference has not been formalized as concisely as

1+m02

σ3 [↓m0

3

1+m02

](↑m0

2

0

t2 (m2 ) )By the correctness property of σ3 , the type of s1 is equal to1+m02

σ3 [↓m0

3

1+m02

](↑m0

2

0

t2 (m2 ) → m02(1+m02 ))which can be rewritten to1+m02

σ3 [↓m0

3

1+m02

](↑m0

2

1+m02

0

t2 (m2 ) ) → σ3 [↓m0

3

](m02

(1+m02 ))Because the argument part of this type is equal to the type of s2 ,we can now apply (TApp) to obtain the type of s1 s2 :1+m02

σ3 [↓m0

3](m02(1+m02 ))as is also written in the conclusion of (IApp).

10

2020/9/30

Now, what about the substitution? We have three substitutions,
σ1 , σ2 , and σ3 . We want to return one substitution σ321 that combines them all. By carefully inspecting the numbers of metavariables of the three substitutions, σ321 is defined as the last premiseof (IApp) in Figure 3. The relationship of the three substitutions is
depicted in Figure 4.
We started the type inference of s1 s2 with m metavariables.
During the type inference of s1 , the number of metavariables wasraised to m001 , which was then reduced to m01 by σ1 . During thetype inference of s2 , the number of metavariables was raised tom002 , which was then reduced to m02 by σ2 . Finally, we introduced
one more metavariable, raising the number of metavariables to
1 + m02 , which was then reduced to m03 by σ3 . To combine thethree substitutions, we first raise the number of metavariables fromm to some number (written as 1 + m000
2 in (IApp)) that takes all the
introduced metavariables during the type inference of s1 s2 into
account. Then, σ321 reduces it to m03 .
At first sight, it is not immediately clear how to set the number
1 + m000
2 . In fact, if we did not employ the parallel relation ofsubstitutions, we had to devise the number by ourselves. With theparallel relation of substitutions, it is mechanically determined by
m00
the Agda type checker. From σ1 [↓m10 ] and the inequality m01 ≤1
m002 , we can define σ10 in such a way that the substitution commuteswith lifting. (See the small parallelogram in Figure 4.)
m000

m000

m00

m00

2

1

1

1

σ 321
1+m2 000

2

1+m000

1+m02

2

2

=
=
=
=

1+m0

m00

m00

σ2
σ1

m3 0

m2 0

m1 0

m
Figure 4. Relationship between substitutions in the applicationcaseinfer-App : (m : N) → {n : N} →(Γ : Cxt {m} n) → (s1 s2 : WellScoped n) →untypable Γ (App s1 s2 )] Σ[ m00 ∈ N ] Σ[ m0 ∈ N ] Σ[ m≤m00 ∈ m ≤ m00 ]Σ[ σ ∈ AList TypeF m00 m0 ] Σ[ t ∈ Type m0 ]
Σ[ w ∈ WellTyped (applySubCxt≤ σ m≤m00 Γ) t ](erase w (App s1 s2 ) × mgt σ Γ (App s1 s2 ) t)

We first make a recursive call to infer the type of s1 .
infer-App m {n} Γ s1 s2
with infer m Γ s1... | inj1 ill-s1 = –– s1 is ill-typed
inj1 (illtyped-App1 Γ s1 s2 ill-s1 )... | inj2 (m1 00 , m1 0 , m≤m1 00 , σ 1 , t1 , w1 , eraseW1 ≡S1 , mgσ 1 )If it is untypable, we propagate the untypability of s1 to the untypability of App s1 s2 (using illtyped-App1 ). Otherwise, we obtain atuple with the eight elements, in particular, the (most general) type
t1 for s1 and the substitution σ 1 .
We next apply σ 1 to Γ and infer the type of s2 under thesubstituted type environment.
with letσ 1 Γ : Cxt n
σ 1 Γ = applySubCxt≤ σ 1 m≤m1 00 Γ
in infer m1 0 σ 1 Γ s2... | inj1 ill-s2 = –– s2 is ill-typed
inj1 (illtyped-App2 Γ s1 s2 t1 m≤m1 00 σ 1 mgσ 1 ill-s2 )... | inj2 (m2 00 , m2 0 , m1 0 ≤m2 00 , σ 2 , t2 , w2 , eraseW2 ≡S2 , mgσ 2 )m000(σ21 [↓m20 ](·))
2

m00

σ3

m2 00

m1 00

We have provided the concrete value 1 + m000
2 here, but we did
not have to. It can be uniquely determined by the parallel relation
000
0
0
m000
2 ≤ 1 + m2 // m2 ≤ 1 + m2 . In fact, in the Agda program,
we name the number as 1+m2 000 suggesting that it has the value
1 + m000
2 , but it is merely an identifier whose value is deduced from0
the parallel relation. Finally, we can compose σ21
and σ3 to obtain
σ321 .
The deduction of σ321 from σ1 , σ2 , and σ3 is summarized inmathematical form as follows.
1+m0

1+m2 0

σ 21
σ1 0

00
Here, m000
2 is uniquely determined by the parallel relation m1 ≤000
000
m2 // m1 ≤ m2 (one of the premises of (IApp)), which we
00
0interpret as calculating m000
2 (output, red) from m1 and m1 ≤
00000
m2 (inputs, blue). In this case, m2 can be calculated in fact asm001 +m002 −m01 . However, specifying an exact number is not a good
idea, because we would then have to manipulate such a formula allover the places. Rather, we specify only the parallel relation andprove necessary relations as Agda type checker requires. Once weobtain σ10 and m000
2 , we can compose it with σ2 to obtain σ21 .
We apply the same procedure to σ21 and m02 ≤ 1+m02 to define0
σ21. (The big parallelogram in Figure 4.)
1+m000σ 21(1+m2 00 )m2 000σ10 [↓m200 ](↑m200 ·) = ↑m20 (σ1 [↓m10 ](·))

0
σ21[↓1+m20 ](↑m000 2 ·) = ↑m00Again, if it is untypable, we propagate the untypability of s2 to theuntypability of App s1 s2 (using illtyped-App2 , which requires σ 1
to be most general for s1 ). Otherwise, we obtain the (most general)
type t2 for s2 and the substitution σ 2 .
After the type inference of the two subterms, we allocate a newmetavariable and check whether σ 2 t1 unifies with t2 ⇒ t.

m00

σ3 [↓m0 2 ](↑m0 2 (σ2 [↓m20 ](↑m20 (σ1 [↓m10 ](↑m1 Γ(m) )))))
3
2
2
1
1
{definition of σ10 }
000
000
1+m02
1+m02
m00
m
m
m00
σ3 [↓m0 ](↑m0(σ2 [↓m20 ](σ10 [↓m200 ](↑m200 (↑m1 Γ(m) )))))
3
2
2
2
1
{definition of σ21 , lifting fusion}
1+m0
1+m0
m000
m000
σ3 [↓m0 2 ](↑m0 2 (σ21 [↓m20 ](↑m2 Γ(m) )))32
20{definition of σ21
}
000
000
1+m02
1+m
1+m
m000
0
σ3 [↓m0 ](σ21[↓1+m20 ](↑m000 2 (↑m2 Γ(m) )))3
2
2{definition of σ321 , lifting fusion}
1+m0001+m000σ321 [↓m0 2 ](↑m 2 Γ(m) )with lett : Type (suc m2 0 )t = hh fromN m2 0 ii –– new type variable
m2 0 ≤1+m2 0 : m2 0 ≤ suc m2 0
m2 0 ≤1+m2 0 = n≤m+n 1 m2 0
σ 2 t1 : Type m2 0
σ 2 t1 = applySub≤ σ 2 m1 0 ≤m2 00 t1
in mgu (lift≤ m2 0 ≤1+m2 0 σ 2 t1 ) (lift≤ m2 0 ≤1+m2 0 t2 ⇒ t)... | inj1 ill-unify = inj1 (illtyped-unify Γ s1 s2 t1 m≤m1 00 m1 0 ≤m2 00
σ 1 mgσ 1 σ 2 t2 mgσ 2 ill-unify)... | inj2 (m3 0 , σ 3 , mgσ 3 )3

By transcripting the above scenario, we can define infer-App asfollows.

If it does not, we report the untypability of App s1 s2 (using
illtyped-unify, again requiring the two substitutions to be most gen-11

2020/9/30

eral). Otherwise, we obtain the most general unifying substitution
σ3 .
We next obtain the parallel relation.

other difference is that his proof is done using Coq tactics while ourproof specifies the proof term directly, which requires struggles forclearer and simpler proofs.

= let
m2 000 = proj1 (σ→// σ 1 m1 0 ≤m2 00 )m1 00 ≤m2 000 = proj1 (proj2 (σ→// σ 1 m1 0 ≤m2 00 ))m1 00 ≤m2 000 //m1 0 ≤m2 00 = proj2 (proj2 (σ→// σ 1 m1 0 ≤m2 00 ))Formalization of unification. The unification algorithm was firstformalized by Paulson (1985) in LCF. McBride (2003) formalized unification via structural recursion with the observation thatthe number of metavariables reduces as the unification proceeds.
The correctness of the unification algorithm is shown in (McBride
2003b). The unification algorithm in this paper is directly basedon McBride’s algorithm and its correctness proof. We extend
McBride’s work by implementing unification generically for any
data, rather than simple types as used in McBride’s presentation.
Ribeiro and Camarão (2015) formalized unification algorithm in
Coq following the classic textbook algorithm. They use the degreeof constraints, a pair of the number of metavariables and the size oftypes in constraints, as a termination measure.

Given a substitution and an inequality, the function σ→// returns(in a triple) the parallel relation that must hold together with thelifted number of metavariables and the induced inequality. We can
now obtain σ 21 :in letσ 21 : AList TypeF m2 000 m2 0
σ 21 = σ 2 +h m1 00 ≤m2 000 //m1 0 ≤m2 00 i σ 1
m2 0 ≤1+m2 0 : m2 0 ≤ suc m2 0
m2 0 ≤1+m2 0 = n≤m+n 1 m2 0
1+m2 000 = proj1 (σ→// σ 21 m2 0 ≤1+m2 0 )m2 000 ≤1+m2 000 = proj1 (proj2 (σ→// σ 21 m2 0 ≤1+m2 0 ))Metavariables in generic programming. We introduced metavarim2 000 ≤1+m2 000 //m2 0 ≤1+m2 0 = proj2 (proj2 (σ→// σ 21 m2 0 ≤1+m2 0 )) ables into generic programming by adopting the two-level types

presented by Sheard and Pasalic (2004), extended with additional
information on the number of metavariables. Similar approach wastaken by Hinze et al. (2004) to implement typed-indexed data types
in Haskell and van Noort et al. (2008) to implement rewriting rulesthat contain metavariables.

from which we obtain the second parallel relation.
Finally, we return the result of the type inference.
in inj2 (1+m2 000 , m3 0 , m≤1+m2 000 , σ 321 , σ 3 t ,AppW1 W2 , eraseAppW1 W2 ≡AppS1 S2 ,mg-App s1 m≤m1 00 σ 1 t1 w1 eraseW1 ≡S1 mgσ 1
s2 m1 0 ≤m2 00 σ 2 t2 w2 eraseW2 ≡S2 mgσ 2
σ 3 mgσ 3 )where
σ 3 t : Type m3 0
σ 3 t = applySub σ 3 t

Generic programming. The generic programming we adopted isbased on Regular (van Noort et al. 2008) and supports only thesum-of-product type of data and one recursive position. More flexible framework includes PolyP (Jansson and Jeuring 1997) that supports one datatype parameter, Multirec (Rodriguez et al. 2009) that
supports multiple recursive positions, and Indexed functors (Löhand Magalhães 2011) that support both. Magalhães and Löh (2012)
give a clear comparison between these approaches with implementation in Agda. In this paper, we have used the most basic approach.
It is an interesting future work to see if we can support more flexible approaches. We expect it would not be very hard to support a
datatype parameter. As for multiple recursive positions, we would
have to somehow deal with multiple kinds of metavariables, one foreach recursive position, and mutual recursion based on the vectorof numbers of metavariables.

The inequality m≤1+m2 000 can be easily shown from the inequalities obtained during the type inference and the transitivity law. The
returned substitution σ 321 is defined as follows.
σ 321 : AList TypeF 1+m2 000 m3 0
σ 321 = σ 3 +h m2 000 ≤1+m2 000 //m2 0 ≤1+m2 0 i σ 21

The well-typed term AppW1 W2 is again almost App σ 3 σ 2 w1
σ 3 w2 , but we have to adjust their types. In particular, the typeof w1 is based on t1 but it has to be converted to the form t2⇒ t using the correctness property of σ 3 . The situation is similar
for eraseAppW1 W2 ≡AppS1 S2 . See the accompanying code fordetails.
Finally, to show completeness, we exploit (in mg-App) the factthat the three obtained substitutions are all most general ones.

6.

7.

Conclusion

In this paper, we have presented the complete formalization of type
inference, including unification, and proved its soundness as wellas completeness in Agda. We first extended McBride’s unification
algorithm to work with generic data, so that the correctness of unification is established once and for all. We then formalized type
inference as a function from an untyped term to a well-typed term.
The parallel relation between two inequalities was the key to maintaining the number of metavariables easily. The resulting type inference function was summarized as typing rules that are intuitively
clear but reflect all the details of the underlying soundness proof
including the number of metavariables. Thanks to the generic programming, we can extend the input language without reimplementing unification.
As future work, we have already mentioned in the previous section the extension to more expressive generic programming. As alonger-term goal, we would like to formalize various static analyses, which are often specified as type inference problems. For example, Asai et al. (2014) formalized an offline partial evaluation,
but they assumed the input language was already staged. We could
augment their work by providing binding-time analysis before partial evaluation.

Related Work

Formalization of type inference. Type inference has been formalized in various systems. Dubois and Ménissier-Morain (1999),
Naraschewski and Nipkow (1999), and Urban and Nipkow (2009)
formalized the algorithm W (Damas and Milner 1982) in Coq,
Isabelle/HOL, and Nominal Isabelle, respectively. They proved
soundness and completeness of the algorithm W. Their proofs are
more general than ours in that they handle let polymorphism, while
we handle only simply-typed λ-calculus. On the other hand, theirformalizations do not provide the correctness proof of the unification algorithm, but are parameterized over the properties the unification must satisfy. Our formalization includes the correctness of
unification, which clarifies the interaction between the allocation of
new metavariables and substitution.
Garrigue (2015) proved in Coq correctness of type inference forOCaml that includes structural polymorphism and recursion. His
proof is similar to ours in that the number of metavariables is used
to ensure termination. He used it as a termination measure, while
we exploit the structural recursion following McBride (2003). An-

12

2020/9/30

References

Proceedings of the 2009 ACM SIGPLAN International Conference
on Functional Programming (ICFP’09), pp. 233–244 (August 2009).
Sheard, T., and E. Pasalic “Two-level types and parameterized modules,”Journal of Functional Programming, Vol. 14, No. 5, pp. 547–587,
Cambridge University Press (September 2004).
Stump, A. Verified Functional Programming in Agda, New York: Association for Computing Machinery and Morgan & Claypool (2016).
Urban, C. and T. Nipkow “Nominal verification of algorithm W,” In G.
Huet, J.-J. Lévy, and G. Plotkin, editors, From Semantics to Computer
Science, Essays in Honour of Gilles Kahn, pp. 363–382, Cambridge
University Press (2009).

Altenkirch, T. “Integrated Verification in Type Theory,” Lecture notes for acourse at ESSLLI 96, Prague, 32 pages (August 1996).
Asai, K., L. Fennell, P. Thiemann, and Y. Zhang “A type theoretic
specification of partial evaluation,” Proceedings of the 2014 Symposiumon Principles and Practice of Declarative Programming (PPDP’14),
pp. 57–68 (September 2014).
Damas, L. and R. Milner “Principal type-schemes for functional programs,”
Proceedings of the 9th Annual ACM Symposium on Principles ofProgramming Languages, pp. 207–212 (January 1982).
Dubois, C. and V. Ménissier-Morain “Certification of a type inference toolfor ML: Damas-Milner within Coq,” Journal of Automated Reasoning,
Vol. 23, No. 3, pp. 319–346 (November 1999).
Garrigue, J. “A Certified Implementation of ML with Structural Polymorphism and Recursive Types,” Mathematical Structures in Computer
Science, Vol. 25, No. 4, pp. 867–891, Cambridge University Press (May2015).
Hinze, R., J. Jeuring, and A. Löh. “Type-indexed data types,” Science ofComputer Programming, Vol. 51, pp. 117–151, Elsevier (2004).
Jansson, P., and J. Jeuring “PolyP—a polytypic programming language
extension,” Proceedings of the ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, pp. 470–482 (January 1997).
Leroy, X. “Polymorphic typing of an algorithmic language,” Research
Report RR-1778, INRIA, Rocquencourt (October 1992).
Löh, A., and J. P. Magalhães “Generic programming with indexed functors,”
Proceedings of the ACM SIGPLAN Workshop on Generic Programming(WGP’11), pp. 1–12 (September 2011).
Magalhães, J. P. and A. Löh “A formal comparison of approaches todatatype-generic programming,” Proceedings of the Fourth Workshop
on Mathematically Structured Functional Programming (MSFP 2012),
Electronic Proceedings in Theoretical Computer Science 76, pp. 50–67(March 2012).
Martin-Löf, P. Intuitionistic Type Theory, Bibliopolis, Napoli (1984).
McBride, C. “First-order unification by structural recursion,” Journal of
Functional Programming, Vol. 13, No. 6, pp. 1061–1075, Cambridge
University Press (November 2003).
McBride, C. “First-order unification by structural recursion, correctness proof” available from http://www.strictlypositive.org/
foubsr-website/, 8 pages (October 2003b).
McBride, C. “How to keep your neighbours in order,” Proceedings ofthe 2014 ACM SIGPLAN International Conference on Functional
Programming (ICFP’14), pp. 297–309 (September 2014).
Naraschewski, W. and T. Nipkow “Type inference verified: algorithm W
in Isabelle/HOL,” Journal of Automated Reasoning, Vol. 23, No. 3,
pp. 299–318 (November 1999).
Nazareth, D., and T. Nipkow “Formal Verification of Algorithm W: The
Monomorphic Case,” In G. Goos, J. Hartmanis, J. van Leeuwen, J. vonWright, J. Grundy, and J. Harrison, editors. Theorem Proving in Higher
Order Logics (LNCS 1125), pp. 331–345 (August 1996).
van Noort, T., A. Rodriguez Yakushev, S. Holdermans, J. Jeuring, and
B. Heeren “A lightweight approach to datatype-generic rewriting,”
Proceedings of the ACM SIGPLAN Workshop on Generic Programming(WGP’08), pp. 13–24 (September 2008).
Norell, U. “Dependently typed programming in Agda,” In P. Koopman, R.
Plasmeijer, and D. Swierstra, editors, Advanced Functional Programming (LNCS 5832), pp. 230–266 (2009).
Paulson, L. C. “Verifying the unification algorithm in LCF,” Science ofComputer Programming, Vol. 5, No. 2, pp. 143–169, Elsevier NorthHolland (June 1985).
Ribeiro, R., and C. Camarão “A mechanized textbook proof of a typeunification algorithm,” In M. Cornélio, and B. Roscoe, editors, Formal
Methods: Foundations and Applications (LNCS 9526), pp. 127–141(September 2015).
Rodriguez Yakushev, A., S. Holdermans, A. Löh, and J. Jeuring “Generic
programming with fixed points for mutually recursive datatypes,”

13

2020/9/30