Higher-Order Dynamic Pattern Unification for Dependent Types and Records

Andreas Abel^{1} and Brigitte Pientka^{2}

1 Department of Computer Science and Engineering Gothenburg University

                            andreas.abel@gu.se

2 School of Computer Science, McGill University, Montreal, Canada

                          bpientka@cs.mcgill.ca

Abstract. While higher-order pattern unification for the λ^{Π}-calculus is decidable and unique unifiers exists, we face several challenges in practice: 1) the pattern fragment itself is too restrictive for many applications; this is typically addressed by solving sub-problems which satisfy the pattern restriction eagerly but delay solving sub-problems which are non-patterns until we have accumulated more information. This leads to a dynamic pattern unification algorithm. 2) Many systems implement λ^{ΠΣ} calculus and hence the known pattern unification algorithms for λ^{Π} are too restrictive. In this paper, we present a constraint-based unification algorithm for λ^{ΠΣ}-calculus which solves a richer class of patterns than currently possible; in particular it takes into account type isomorphisms to translate unification problems containing Σ-types into problems only involving Πtypes. We prove correctness of our algorithm and discuss its application.

1 Introduction

Higher-order unification is a key operation in logical frameworks, dependentlytyped programming systems, or proof assistants supporting higher-order logic. It plays a central role in type inference and reconstruction algorithms, in the execution of programs in higher-order logic programming languages, and in reasoning about the totality of functions defined by pattern-matching clauses.

\underline{2}

While full higher-order unification is undecidable [8], Miller [10] identified a decidable fragment of higher-order unification problems, called the pattern fragment. A pattern is a unification problem where all meta-variables (or logic variables) occurring in a term are applied to some distinct bound variables. For example, the problem λx y z. X x y = λx y z. x (suc y) falls into the pattern fragment, because the meta-variable X is applied to distinct bound variables x and y; the pattern condition allows us to solve the problem by a simple abstraction X = λx y. x (suc y). This is not possible for non-patterns; examples for non-pattern problems which have no unique most general unifier can be obtain by changing the left hand side of the previous problem to λx y z. X x x y (non-linearity), λx y z. X (Y x) y (X applied to another meta-variable) or λx y z. X x (suc y) (X applied to non-variable term).

In practice we face several challenges: First, the pattern fragment is too restrictive for many applications. Systems such as Twelf [13], Beluga [15], and Delphin [16] solve eagerly sub-problems which fall into the pattern fragment and delay sub-problems outside the pattern fragment until more information has been gathered which in turn simplifies the delayed sub-problems. The metatheory justifying the correctness of such a strategy is largely unexplored and complex (an exception is the work by Reed [17]).

Second, we often want to consider richer calculi beyond the λ^{Π}-calculus. In Beluga and Twelf for example we use Σ-types to group assumptions together. In Agda [12] we support Σ-types in form of records with associated η-equality in its general form. Yet, little work has been done on extending the pattern fragment to handle also Σ-types. The following terms may be seen as equivalent: (a) λy_{1}.λy_{2}. X (y_{1}, y_{2}), (b) λy. X (fst y) (snd y) and (c) λy_{1}.λy_{2}. X y_{1} y_{2}. Only the last term falls within the pattern fragment as originally described by Miller. However, the other two terms can be transformed such that they also fall into the pattern fragment: for term (a), we replace X with λy. X′ (fst y) (snd y); for term (b), we unfold y which stands for a pair and replace y with (y_{1}, y_{2}).

In this paper, we describe a higher-order unification algorithm for the λ^{ΠΣ} calculus; our algorithm handles lazily η-expansion and we translate terms into the pure pattern fragment where a meta-variable is applied to distinct bound variables. The key insight is to take into account type isomorphisms for Σ, the dependently typed pairs: Πz:(Σx:A.B).C is isomorphic to Πx:A.Πy:B.[(x, y)/z]C, and a function f:Πx:A.Σy:B.C can be translated into two functions f_{1} : Πx:A.B and f_{2} : Πx:A.[f_{1} x/y]C. These transformations allow us to handle a richer class of dependently-typed patterns than previously considered.

Following Nanevski et al. [11] and Pientka [14], our description takes advantage of modelling meta-variables as closures; instead of directly considering a meta-variable X at function type Πx:A.B which is applied to x, we describe them as contextual objects, i.e., objects of type B in a context x:A, which are associated with a delayed substitution for the local context x:A.^{3} This allows us to give a high-level description and analysis following Dowek et al. [3], but not resorting to explicit substitutions; more importantly, it provides a logical grounding for some of the techniques such as “pre-cooking” and handles a richer calculus including Σ-types. Our work also avoids some of the other shortcomings; as pointed out by Reed [17], the algorithm sketched in Dowek et al. [3] fails to terminate on some inputs. We give a clear specification of the pruning which eliminates bound variable dependencies for the dependently typed case and show correctness of the unification algorithms in three steps: 1) we show that it terminates, 2) we show that the transformations in our unification algorithm preserve types, and 3) that each transition neither destroys nor creates (additional) solutions.

3 We write x:A for a vector x_{1}:A_{1}, … x_{n}:A_{n}.

2. λ^{ΠΣ}-CALCULUS  3

Our work is to our knowledge the first comprehensive description of constraintbased higher-order pattern unification for the λ^{ΠΣ} calculus. It builds on and extends prior work by Reed [17] to handle Σ-types. Previously, Elliot [5] described unification for Σ-types in a Huet-style unification algorithm. While it is typically straightforward to incorporate η-expansions and lowering for metavariables of Σ-type [19,12] , there is little work on extending the notion of Miller patterns to be able to handle meta-variables which are applied to projections of bound variables. Fettig and Löchner [6] describe a higher-order pattern unification algorithm with finite products in the simply typed lambda-calculus. Their approach does not directly exploit isomorphisms on types, but some of the ideas have a similar goal: for example abstractions λx. fst x is translated into λ(x_{1}, x_{2}). fst (x_{1} , x_{2}) which in turn normalizes to λ(x_{1}, x_{2}).x_{1} to eliminate projections. Duggan [4] also explores extended higher-order patterns for products in the simply-typed setting; he generalizes Miller’s pattern restriction for the simply-typed lambda-calculus by allowing repeated occurrences of variables to appear as arguments to meta-variables, provided such variables are prefixed by distinct sequences of projections.

Our work has been already tested in practice. Some of the ideas described in this paper are incorporated into the implementation of the dependently-typed language Agda and Beluge. Agda has dependently typed records, a generalization of Σ-types. In Beluga, Σ-types occur in a restricted form, i.e., only variable declarations in contexts can be of Σ-type and there is no nesting of Σ-types.

This is the extended version of a published conference paper [1].

2 λ^{ΠΣ}-calculus

In this paper, we are considering an extension of the λ^{ΠΣ}-calculus with metavariables. Its grammar is mostly straightforward. We use x, y, z for bound variables to distinguish them from meta-variables u, v, and w.

Sorts  s ::= type | kind
Atomic types  P, Q ::= a M
Types  A, B, C, D ::= P | Πx:A.B | Σx:A.B
Kinds  κ ::= type | Πx:A.κ
(Rigid) heads  H ::= a | c | x
Projections  π ::= fst | snd
Evaluation contexts  E ::= • | E N | π E
Neutral terms  R ::= E[H] | E[u[σ]]
Normal terms  M, N ::= R | λx.M | (M , N)
Substitutions  σ, τ ::= · | σ, M
Variable substitutions  ρ, ξ ::= · | ρ, x
Contexts  Ψ, Φ, Γ ::= · | Ψ, x:A
Meta substitutions  θ, η ::= · | θ, Ψ̂.M/u
Meta contexts  Δ ::= · | Δ, u:A[Ψ]

Meta-variables are characterized as a closure u[σ] which is the use of the metavariable u under the suspended explicit substitution σ. The term λx y z. X x y with the meta-variable X which has type Πx:A.Πy:B.C is represented in our calculus as λx y z. u[x, y] where u has type C[x:A, y:B] and [x, y] is a substitution with domain x:A, y:B and the range x, y, z. Instead of an abstraction, we can directly replace u with a contextual object x, y. x (suc y). In general, a contextual object Ψ̂. M is a term M whose free variables have to be contained in

the variable list Ψ̂ . (In the example, Ψ̂ = x, y and M = x (suc y).) The use of contextual objects eliminates the need to craft a λ-prefix for the instantiation of meta-variables, avoids spurious reductions, and provides simple justifications for techniques such as lowering (see Section 3.2). In general, meta-variable u of contextual type A[Ψ] stands for a contextual object Ψ̂.M where Ψ̂ is the domain of Ψ, i. e., the list of variables declared in Ψ in the correct order. The use of the prefix Ψ̂ allows us to rename the free variables occurring in M if necessary. Our grammar and our subsequent typing rules enforce that objects are β-normal.

A signature Σ is a collection of declarations, which take one of the forms: a : κ (type family declaration) or c : A (constructor declaration). Because variable substitutions ρ play a special role in the formulation of our unification algorithm, we recognize them as a subclass of general substitutions σ.

Weakening substitutions wk_{Φ} , which are a special case of variable substitutions, are defined recursively by wk_{·} = (·) and wk_{Φ,x:A} = (wk_{Φ}, x). The subscript Φ is dropped when unambiguous. Incidentially, wk_{Φ} = Φ̂, but conceptually, one is a substitution and one a list of binders, thus, we keep them separate. If and only if Φ is a sub-context of Ψ modulo η-equality, then wk_{Φ} is a well-formed substitution in Ψ, i.e., Ψ ⊢ wk_{Φ} : Φ holds (see Fig. 1).

We write E[M] for plugging term M into the hole • of evaluation context E. This will be useful when describing the unification algorithm, since we often need to have access to the head of a neutral term. In the λ^{Π}-calculus, this is often achieved using the spine notation [2] simply writing H M_{1} … M_{n}. Evaluation contexts are the proper generalization of spines to projections (see also [19] for a similar generalization in the linear setting).

Occurrences and free variables. If α, β are syntactic entities such as evaluation contexts, terms, or substitutions, α, β ::= E | R | M | σ, we write α{β} if β is a part of α. If we subsequently write α{β′} then we mean to replaceme the indicated occurrence of β by β′. We say an occurrence is rigid if it is not part of a delayed substitution σ of a meta-variable, otherwise it is termed flexible. For instance, in c (u[y_{1}]) (x_{1} x_{2}) (λz. z x_{3} v[y_{2}, w[y_{3}]]) there are rigid occurrences of x_{1..3} and flexible occurrences of y_{1..3}. The meta-variables u, v appear in a rigid and w in a flexible position. A rigid occurrence is strong if it is not in the evaluation context of a free variable. In our example, only x_{2} does not occur strongly rigidly. Following Reed [17] we indicate rigid occurrences by α{β}^{rig}

and strongly rigid occurrences by α{β}^{srig} .

Flexible variable occurrences can vanish by instantiation of meta-variables, rigid ones not. In our example, y_{1} will disappear by the substitution y_{1}.c′/u.

Rigid variables might disappear by instantiation of other free variables and subsequent normalization. For instance, x_{2} disappears when we substitute λx_{2}.c′ for x_{1}. However, strongly rigid ones will only disappear when they are instantiated themselves, not through other variable instantiations.

We denote the set of free variables of α by FV(α) and the set of free meta

variables by FMV(α) . A superscript ^{rig} indicates to count only the rigid variables.

Typing. We rely on a bi-directional type system to guarantee that well-typed terms are in β-normal form (Fig. 1). The typing rules are divided into rules which check that an object has a given type (⇐ judgments) and rules which synthesize a type for a given object (⇒ judgments). We have record types Σx:A. B but no record kinds Σx:A. κ. Our typing rules ensure that terms are in β-normal form, but they need not be η-long. The judgment A =_{η} C (rules omitted) compares A and C modulo η, i.e., modulo R = λx. R x (x ∉ FV(R)) and R = (fst R , snd R).

Hereditary substitution and meta substitution. For α a well-typed entity in context Ψ and Δ; Φ ⊢ σ : Ψ a well-formed substitution, we facilitate a simultaneous substitution operation [σ]_{Ψ} α that substitutes the terms in σ for the variables as listed by Ψ in α and produces a β-normal result. Such an operation exists for well-typed terms, since λ^{ΠΣ} is normalizing. A naive implementation just substitutes and then normalizes. A refined implementation, called hereditary substitution [20], proceeds by resolving created redexes on the fly through new substitutions. Both Agda and Beluga use that strategy, as well as other theoretical investigations of logical frameworks. Single hereditary substitution [N/x]_{A}α is conceived as a special case of simultaneous substitution. The type annotation A and the typing information in Ψ allow hereditary substitution to be defined by structural recursion; if no ambiguity arises, we may omit indices Ψ and A from substitutions.

The meta-substitution operation, i. e., substitution of meta variables by con-

textual objects, is written as [[Ψ̂.M/u]]N and the simultaneous meta substitu-

tion is written as [[θ]]N . Both operations restore β-normality. In the particular

case when we apply Ψ̂.M/u to u[σ], we first substitute Ψ̂.M for u in σ to obtain σ′. Subsequently, we continue to apply σ′ to M hereditarily to obtain M′.

Detailed definitions of hereditary substitution and meta substitution can be found in the appendices A and B.

3 Constraint-based unification

We define the unification algorithm using rewrite rules which solve constraints incrementally. Constraints K and sets of constraints K are defined as follows:

\underline{6}

Neutral terms/types Δ; Ψ ⊢ R ⇒ A (Δ and Ψ fixed)
{Σ(a) = κ \atop Δ; Ψ ⊢ a ⇒ κ} {Σ(c) = A \atop Δ; Ψ ⊢ c ⇒ A} {Ψ(x) = A \atop Δ; Ψ ⊢ x ⇒ A} \begin{matrix}u:A[Φ] ∈ Δ & Δ; Ψ ⊢ σ ⇐ Φ \\ Δ; Ψ ⊢ u[σ] ⇒ [σ]_{Φ}A \end{matrix}

\begin{matrix}Δ; Ψ ⊢ R ⇒ Πx:A.B & Δ; Ψ ⊢ M ⇐ A \\ Δ; Ψ ⊢ R M ⇒ [M/x]_{A}B \end{matrix}

{Δ; Ψ ⊢ R ⇒ Σx:A.B \atop Δ; Ψ ⊢ fst R ⇒ A} {Δ; Ψ ⊢ R ⇒ Σx:A.B \atop Δ; Ψ ⊢ snd R ⇒ [fst R/x]_{A}B}
Normal terms Δ; Ψ ⊢ M ⇐ A (Δ fixed)

\begin{matrix}Δ; Ψ ⊢ R ⇒ A & A =_{η} C \\ Δ; Ψ ⊢ R ⇐ C \end{matrix}

{Δ; Ψ, x:A ⊢ M ⇐ B \atop Δ; Ψ ⊢ λx.M ⇐ Πx:A.B} \begin{matrix}Δ; Ψ ⊢ M ⇐ A & Δ; Ψ ⊢ N ⇐ [M/x]_{A}B \\ Δ; Ψ ⊢ (M , N) ⇐ Σx:A.B \end{matrix}
Substitutions Δ; Ψ ⊢ σ ⇐ Ψ′ (Δ and Ψ fixed)
Δ; Ψ ⊢ · ⇐ · \begin{matrix}Δ; Ψ ⊢ σ ⇐ Ψ′ & Δ; Ψ ⊢ M ⇐ [σ]_{Ψ′}A \\ Δ; Ψ ⊢ σ, M ⇐ Ψ′, x:A \end{matrix}
LF types and kinds Δ; Ψ ⊢ A ⇐ s (Δ fixed)
Δ; Ψ ⊢ P ⇒ type
Δ; Ψ ⊢ P ⇐ type

Δ; Ψ ⊢ A ⇐ type Δ; Ψ, x:A ⊢ B ⇐ type
Δ; Ψ ⊢ Σx:A.B ⇐ type
Δ; Ψ ⊢ type ⇐ kind  \begin{matrix}Δ; Ψ ⊢ A ⇐ type & Δ; Ψ, x:A ⊢ B ⇐ s \\ Δ; Ψ ⊢ Πx:A.B ⇐ s \end{matrix}
LF typing contexts Δ ⊢ Ψ ctx (Δ fixed)
\overline{Δ ⊢ · ctx} \frac{Δ ⊢ Ψ ctx Δ; Ψ ⊢ A ⇐ type}{Δ ⊢ Ψ, x:A ctx}
Meta substitutions Δ ⊢ θ ⇐ Δ′ (Δ fixed)

for all u:A[Φ] ∈ Δ′ and Φ̂.M/u ∈ θ : Δ; [[θ]]Φ ⊢ M ⇐ [[θ]]A

Δ ⊢ θ ⇐ Δ′
Meta contexts ⊢ Δ mctx

for all u:A[Ψ] ∈ Δ : Δ ⊢ Ψ ctx Δ; Ψ ⊢ A ⇐ type

⊢ Δ mctx

Fig. 1. Typing rules for LF with meta-variables DRAFT July 4, 2017—12 : 53

Constraint K ::= ⊤ | ⊥  Trivial constraint and inconsistency.
| Ψ ⊢ M = N : C Unify term M with N.
| Ψ | R:A ⊢ E = E′ Unify evaluation context E with E′.
| Ψ ⊢ u ← M : C  Solution for u found.
C. sets  K ::= K | K ∧ K  (modulo laws of conjunction).

Our basic constraints are of the form Ψ ⊢ M = N : C. The type annotation Ψ ⊢ C serves two purposes: First, we need to types to direct any hereditary substitutions we employ during constraint solving. Secondly, the type annotations in the context Ψ are necessary to eliminate Σ-types. For both purposes, simple types, i.e., the dependency-erasure of Ψ ⊢ C would suffice. However, we keep dependencies in this presentation to scale this work from λ^{ΠΣ} to non-erasable dependent types such as featured by Agda.

A unification problem is described by Δ ⊩ K where Δ contains the typings of all the meta variables in K. A meta-variable u is solved, if there is a constraint Ψ ⊢ u ← M : C in K; otherwise we call u active. A solved metavariable does not appear in any other constraints nor in any type in Δ (nor in its solution M).

Intuitively, a set of constraints is well-formed if each constraint Ψ ⊢ M = N : C is well typed. Unfortunately, this is complicated by the fact that we may delay working on some sub-terms; to put it differently, we can work on subterms in an arbitrary order. Yet, the type of an equation may depend on the solvability of another postponed equation. Consider for example tuples. If (M_{1}, M_{2}) and (N_{1}, N_{2}) both have type Σx:A.B, then M_{1} and N_{1} have type A. However, types may get out of sync when we consider M_{2} and N_{2}. M_{2} has type [M_{1}/x]B while N_{2} has type [N_{1}/x]B, and we only know that their types agree, if we know that M_{1} is equal to N_{1}. Similar issues arise for function types and applications. Following Reed [17], we adopt here a weaker typing invariant, namely typing modulo constraints.

3.1 Typing modulo

For all typing judgments Δ; Ψ ⊢ J defined previously, we define Δ; Ψ ⊢_{K} J by the same rules as for Δ; Ψ ⊢ J except replacing eta equality =_{η} with =_{K}. We write α =_{K} β if for any ground meta-substitution θ that is a ground solution for K, we have [[θ]]α =_{η} [[θ]]β. To put it differently, if we can solve K, we can establish that α is equal to β.

The following lemmas proven by Reed [17] hold also for the extension to Σtypes; we keep in mind that the judgment J stands for either a typing judgment or an equality judgment. We first prove that typing modulo is preserved under equality modulo.

Lemma 1 (Conversion modulo). Let Δ_{0} ⊩ K and Δ =_{K} Δ′ and Ψ =_{K} Φ and A =_{K} B.

1. If Δ; Ψ ⊢_{K} M ⇐ A then Δ′; Φ ⊢_{K} M ⇐ B.

2. If Δ; Ψ ⊢_{K} R ⇒ A then Δ′; Φ ⊢_{K} R ⇒ B.

3. If Δ; Ψ ⊢_{K} σ ⇐ Ψ′ and Ψ′ =_{K} Φ′ then Δ′; Φ ⊢_{K} σ ⇐ Φ′.

Proof. We generalize the statement to types and kinds and prove them by simultaneous induction on the typing derivation.

Lemma 2 (Substitution principle modulo). Let Δ_{0} ⊩ K. If Δ; Ψ ⊢_{K} M ⇐ A and Δ; Ψ, x:B, Ψ′ ⊢_{K} J and A =_{K} B then Δ; Ψ, [M/x]_{A}Ψ′ ⊢_{K} [M/x]_{A}J.

Proof. This proof follows essentially the proof by Nanveski et al. [11] and we generalize the property to types, kinds, and contexts. Since we prove the substitution lemma modulo A =_{K} B, we use Lemma 1 when we for example consider the variable case.

Lemma 3 (Meta-substitution principle modulo). Let Δ_{0} ⊩ K. If Δ_{1} ⊢_{K} θ ⇐ Δ and Δ; Φ ⊢_{K} J then K′ = [[θ]]K is defined and Δ_{1}; [[θ]]Φ ⊢_{K′} [[θ]]J.

Proof. Let · ⊢ η ⇐ Δ_{0} be a ground solution of Δ_{0} ⊩ K. By assumption, [[η]]Δ_{1} ⊢ [[η]]θ ⇐ [[η]]Δ and [[η]]Δ; [[η]]Φ ⊢ [[η]]J.

Induction on Δ; Φ ⊢_{K} J. All cases are by inversion, appeal to the induction hypothesis (i.h.), reassembling the result and if necessary using Lemma 1 (see the case for meta-variables). We show the case where we transition between checking and synthesizing a type.

Case

D = \frac{Δ; Φ ⊢_{K} R ⇒ C_{1} C_{1} =_{K} C_{2}}{Δ; Φ ⊢_{K} R ⇐ C_{2}}

Δ_{1}; [[θ]]Φ ⊢_{[[θ]]K} [[θ]]R ⇒ [[θ]]C_{1} by i.h. [[θ]]C_{1} =_{[[θ]]K} [[θ]]C_{2} by i.h. C_{1} =_{K} C_{2} Δ_{1}; [[θ]]Φ ⊢_{[[θ]]K} [[θ]]R ⇐ [[θ]]C_{2}.

Case

D = \frac{Δ; Ψ ⊢_{K} σ ⇐ Ψ′ u:B[Ψ′] ∈ Δ}{Δ; Ψ ⊢_{K} u[σ] ⇐ [σ]_{Ψ′}(B)}

For Ψ̂′.M/u ∈ θ and u:B[Ψ′] ∈ Δ, Δ_{1}; [[θ]]Ψ′ ⊢_{K} M ⇐ [[θ]]B. Δ_{1}; [[θ]]Ψ ⊢_{[[θ]]K} [[θ]]σ ⇐ [[θ]]Ψ′ by i.h. [[θ]](u[σ]) = [[[θ]]σ]_{Ψ′}(M) by definition Δ_{1}; [[θ]]Ψ ⊢_{[[θ]]K} [[[θ]]σ]M ⇐ [[[θ]]σ]([[θ]]B) by ord. subst. lemma Δ_{1}; [[θ]]Ψ ⊢_{[[θ]]K} [[[θ]]σ]M ⇐ [[θ]]([σ]B) by definition of msubst. ⊓ ⊔

Intuitively, a unification problem Δ ⊩ K is well-formed if all constraints (Ψ ⊢ M = N : C) ∈ K are well-typed modulo K, i.e., Δ; Ψ ⊢_{K} M ⇐ C and Δ; Ψ ⊢_{K} N ⇐ C. We will come back to this later when we prove correctness of our algorithm, but it is helpful to keep the typing invariant in mind when explaining the transitions in our algorithm.

Decomposition of functions

Ψ ⊢ λx.M = λx.N : Πx:A. B  ↦_{d} Ψ, x:A ⊢ M = N : B
Ψ ⊢ λx.M = R : Πx:A. B  ↦_{d} Ψ, x:A ⊢ M = R x : B
Ψ ⊢ R = λx.M : Πx:A. B  ↦_{d} Ψ, x:A ⊢ R x = M : B

Decomposition of pairs

Ψ ⊢ (M_{1} , M_{2}) = (N_{1} , N_{2}) : Σx:A. B ↦_{d} Ψ ⊢ M_{1} = N_{1} : A ∧ Ψ ⊢ M_{2} = N_{2} : [M_{1}/x]B
Ψ ⊢ (M_{1} , M_{2}) = R : Σx:A. B  ↦_{d} Ψ ⊢ M_{1} = fst R : A ∧ Ψ ⊢ M_{2} = snd R : [M_{1}/x]B
Ψ ⊢ R = (M_{1} , M_{2}) : Σx:A. B  ↦_{d} Ψ ⊢ fst R = M_{1} : A ∧ Ψ ⊢ snd R = M_{2} : [fst R/x]B

Decomposition of neutrals

Ψ ⊢ E[H] = E′[H] : C  ↦_{d} Ψ | H : A ⊢ E = E′ where Ψ ⊢ H ⇒ A
Ψ ⊢ E[H] = E′[H′] : C  ↦_{d} ⊥ if H ≠ H′

Decomposition of evaluation contexts

Ψ | R : A ⊢ • = •  ↦_{d} ⊤
Ψ | R : Πx:A. B ⊢ E[• M] = E′[• M′] ↦_{d} Ψ ⊢ M = M′ : A ∧ Ψ | R M : [M/x]B ⊢ E = E′
Ψ | R : Σx:A. B ⊢ E[fst •] = E′[fst •] ↦_{d} Ψ | fst R : A ⊢ E = E′
Ψ | R : Σx:A. B ⊢ E[snd •] = E′[snd •] ↦_{d} Ψ | snd R : [fst R/x]B ⊢ E = E′
Ψ | R : Σx:A. B ⊢ E[π •] = E′[π′ •]  ↦_{d} ⊥ if π ≠ π′

Orientation

Ψ ⊢ M = u[σ] : C with M ≠ v[…]  ↦_{d} Ψ ⊢ u[σ] = M : C

η-Contraction

Ψ ⊢ u[σ{λx. R x}] = N : C  ↦_{e} Ψ ⊢ u[σ{R}] = N : C
Ψ ⊢ u[σ{(fst R, snd R)}] = N : C  ↦_{e} Ψ ⊢ u[σ{R}] = N : C

Eliminating projections

Ψ_{1}, x : Πy:A. Σz:B.C, Ψ_{2}  Ψ_{1}, x_{1} : Πy:A. B, x_{2} : Πy:A. [(x_{1} y)/z]C, Ψ_{2}
⊢ u[σ{π (x M)}] = N : D ↦_{p} ⊢ u[[τ]σ] = [τ]N : [τ]D
where π ∈ {fst, snd}  where τ = [λy. (x_{1} y, x_{2} y)/x]

Fig. 2. Local simplification K ↦_{m} K .

3.2 A higher-order dynamic pattern unification algorithm for dependent types and records

The higher-order dynamic pattern unification algorithm is presented as rewrite rules on the set of constraints K in meta-variable context Δ. The local simplification rules (Figure 2) apply to a single constraint, decomposing it and molding it towards a pattern by η-contraction and projection elimination. Decomposition of neutral terms is defined using evaluation contexts to have direct access to the head.

Local simplification

Δ ⊩ K ∧ K ↦ Δ ⊩ K ∧ K′  if K ↦_{m} K′  (m ∈ {d, e, p})

Instantiation (notation)

Δ ⊩ K + (Φ ⊢ u ← M : A)  = [[θ]]Δ ⊩ [[θ]]K ∧ [[θ]]Φ ⊢ u ← M : [[θ]]A
where θ = Φ̂.M/u

Lowering

Δ ⊩ K  ↦ Δ, v:B[Φ, x:A] ⊩ K
u:(Πx:A.B)[Φ] ∈ Δ active  + Φ ⊢ u ← λx.v : Πx:A. B
Δ ⊩ K  ↦ Δ, u_{1}:A[Φ], u_{2}:([u_{1}/x]_{A}B)[Φ] ⊩ K
u:(Σx:A.B)[Φ] ∈ Δ active  + Φ ⊢ u ← (u_{1} , u_{2}) : Σx:A. B

Flattening Σ-types

Δ ⊩ K (u:A[Φ] ∈ Δ active)  ↦ Δ, v:([σ^{−1}]A)[Φ′] ⊩ K + Φ ⊢ u ← v[σ] : A
Φ = Φ_{1}, x : Πy:A. Σz:B. C, Φ_{2}  Φ′ = Φ_{1}, x_{1} : Πy:A. B, x_{2} : Πy:A. [x_{1} y/z]C, Φ_{2}
σ^{−1} = [λy. (x_{1} y , x_{2} y)/x]  σ = [λy. fst (x y)/x_{1}, λy. snd (x y)/x_{2}]

Pruning

Δ ⊩ K  ↦ Δ′ ⊩ [[η]]K
(Ψ ⊢ u[ρ] = M : C) ∈ K  if Δ ⊢ prune_{ρ} M ⇒ Δ′; η and η ≠ id

Same meta-variable

Δ ⊩ K ∧ Ψ ⊢ u[ρ] = u[ξ] : C  ↦ Δ, v:A[Φ_{0}] ⊩ K + Φ ⊢ u ← v[wk_{Φ_{0}}] : A
u:A[Φ] ∈ Δ  if ρ ∩ ξ : Φ ⇒ Φ_{0}

Failing occurs check

Δ ⊩ K ∧ Ψ ⊢ u[ρ] = M : C  ↦ ⊥ if FV^{rig}(M) ⊈ ρ
Δ ⊩ K ∧ Ψ ⊢ u[ρ] = M : C  ↦ ⊥ if M = M′{u[ξ]}^{srig} ≠ u[ξ]

Solving (with successful occurs check)

Δ ⊩ K ∧ Ψ ⊢ u[ρ] = M : C  ↦ Δ ⊩ K + Φ ⊢ u ← M′ : A
(u:A[Φ]) ∈ Δ; u ∉ FMV(M)  if M′ = [ρ/Φ̂]^{−1}M exists and Δ; Φ ⊢ M′ ⇐ A

Fig. 3. Unification steps Δ ⊩ K ↦ Δ′ ⊩ K′ .

Decomposition of pairs could maybe more concisely defined by

Ψ ⊢ M = N : Σx:A. B ↦_{d} Ψ ⊢ fst@M = fst@N : A
∧ Ψ ⊢ snd@M = snd@N : [fst@M/x]B

where π@M computes the β-normal form of π M. However, this would also apply to a constraint Ψ ⊢ R = R′ : Σx:A. B of neutral terms, just duplicating the work of decomposing the neutrals later. Similar reasoning justifies of choice of function decomposition rules.

The other unification steps (Figure 3) work on a meta-variable and try to find an instantiation for it. We write Δ ⊩ K + Φ ⊢ u ← M : A for instantiating the meta variable u with the term M both in the meta-context Δ and in the constraints K. This abbreviation is defined in Figure 3. Lowering rules transform a meta-variable of higher type to one of lower type. Flattening Σ-types concentrates on a meta-variable u:A[Φ] and eliminates Σ-types from the context Φ. The combination of the flattening Σ-types transition and the eliminating projections transition allow us to transform a unification problem into one which resembles our traditional pattern unification problem. The pruning transition is explained in detail in Section 3.4 and unifying a meta-variable with itself is discussed in Section 3.5.

To motivate our rules, let us consider some problems Ψ ⊢ u[σ] = M : C that fall outside of the Miller pattern fragment, meaning that σ is not a list of disjoint variables. We may omit types and/or context if appropriate.

η-contraction u[λx. y (fst x , snd x)] = M.

Solved by contracting the l.h.s. to u[y].

Eliminating projections y : Πx:A. Σz:B. C ⊢ u[λx. fst (y x)] = M. Applying substitution τ = [λx. (y_{1} x , y_{2} x)/y] yields problem y_{1} : Πx:A. B, y_{2} : Πx:A. [y_{1} x/z]C ⊢ u[λx. y_{1} x] = [τ]M which is solved by η-contraction, provided y_{2} ∉ FV([τ]M).

Lowering Φ ⊢ fst (u[y]) = fst y where Φ = (y : Σx:A. B) and u : (Σx:A. B)[Φ]. This equation determines only the first component of the tuple u. Thus, decomposition into u[y] = y, which also determines the second component, loses solutions. Instead we replace u by a pair (u_{1}, u_{2}) of meta-variables of lower type, u_{1} : A[Φ] and u_{2} : ([u_{1}[y]/x]B)[Φ], yielding Φ ⊢ u_{1}[y] = fst y.

Flattening Σ-types Ψ ⊢ u[λx. (z_{1} x , z_{2} x)] = g z_{1} z_{2} where Ψ(z_{1}) = Πx:A. B and Ψ(z_{2}) = Πx:A. [z_{1} x/y]C and u : P [z : Πx:A. Σy:B. C]. By splitting z into two functions z_{1}, z_{2} in the context of u and replacing u by v : P [z_{1} : Πx:A. B, z_{2} : Πx:A. [z_{1} x/y]C] via meta sustitution z.v[λx. fst z x, λx. snd z x]/u, we arrive at Ψ ⊢ v[λx. z_{1} x, λx. z_{2} x] = g z_{1} z_{2} and continue with η-contraction.

Solving in spite of non-linearity u[x, x, z] = suc z.

The non-linear occurrence of x on the l.h.s. can be ignored since x is not free on the r.h.s. We can solve this constraint by u[x, y, z] = suc z. However, in case of non-linearity we need to make sure that the solution is well-typed. Consider u : P z [Φ] where Φ = (x:A, y : P x, z:A) and constraint

x:A, y : P x ⊢ u[x, y, x] = y : P x.

The solution x:A, y : P x ⊢ u ← y : P z is ill-typed. While the non-linear variables do not appear in the term of the rhs, they appear in the type and make the constraint well-typed. In our type theory, the above constraint is probably unsolvable (but we attemp no proof here). In richer type theories such as Agda one could imagine a solution for u which applies a type cast to y. Thus, we just leave such a constraint alone, instead of flagging unsolvability.

Pruning u[x] = suc(v[x, y]) and v[x, zero] = f(x, zero).

Since u depends only on x, necessarily v cannot depend on y. We can prune away the second parameter of v by setting v[x, y] = v′[x]. This turns the second constraint into the pattern v′[x] = f(x, zero), yielding the solution u[x] = suc(f(x, zero)). Note that pruning is more difficult in case of nested meta variables. If instead u[x] = suc(v[x, w[y]]) then there are two cases: either v does not depend on its second argument or w is constant. Pruning as we describe it in this article cannot be applied to this case; Reed [17] proceeds here by replacing y by a placeholder “ ”. Once w gets solved the placeholder might occur as argument to v, where it can be pruned. If the placeholder appears in a rigid position, the constraints have no solution.

Pruning and non-linearity u[x, x] = v[x] and u′[x, x] = v′[x, y].

Even though we cannot solve for u due to the non-linear x, pruning x from v could lose solutions. However, we can prune y from v′ since only x can occur in v′[x, y].

Failing occurs check u[x] = suc y.

Pruning y fails because it occurs rigidly. The constraint set has no solution.

Same meta-variable u[x, y, x, z] = u[x, y, y, x].

Since variables x, y, z are placeholders for arbitrary open well-typed terms, of which infinitely many exists for every type, the above equation can only hold if u does not depend on its 3rd and 4th argument. Thus, we can solve by u[x, y, z, x′] = v[x, y] where [x, y] is the intersection of the two variable environments [x, y, x, z] and [x, y, y, x].

Recursive occurrence u[x, y, x] = suc u[x, y, y].

Here, u has a strong rigid occurrence in its own definition. Even though not in the pattern fragment, this only has an infinite solution: consider the instance u[z, z, z] = suc u[z, z, z]. Consequently, the occurs check signals unsolvability. Reed [18, p. 105f] motivates why only strong rigid recursive occurrences force unsolvability. For instance, f : nat → nat ⊢ u[f] = suc (f (u[λx. zero])) has solution u[f] = suc (f (suc zero)) in spite of a rigid occurrence of u in its definition. If u occurs flexibly in its own definition, like in u[x] = v[u[x]], we cannot proceed until we know more of v. Using the other constraints, we might manage to prune v’s argument, arriving at u[x] = v[], or find the solution of v directly; in these cases, we can revisit the constraint on u.

The examples suggest a strategy for implementation: Lowering can be integrated triggered by decomposition to resolve eliminations of a meta variable E[u[σ]]. After decomposition we have a set of u[σ] = M problems. We try to turn the σs into variable substitutions by applying η-contraction, and where this gets stuck, elimination of projections and Σ-flattening. Solution of constraints u[ρ] = M can then be attempted by pruning, where a failing occurs check signals unsolvability.

3.3 Inverting substitutions

A most general solution for a constraint u[σ] = M can only be hoped for if σ is a variable substitution. For instance u[true] = true admits already two different solutions u[x] = x and u[x] = true that are pure λ-terms. In a language with computation such as Agda infinitely more solutions are possible, because u[x] could be defined by cases on x and the value of u[false] is completely undetermined.

But even constraints u[ρ] = M can be ambiguous if the variable substitution ρ is not linear, i. e., no bijective variable renaming. For example, u[x, x] = x has solutions u[x, y] = x and u[x, y] = y. Other examples, like u[x, x, z] = z, which has unique solution u[x, y, z] = z, suggest that we can ignore non-linear variable occurrences as long as they do not occur on the r.h.s. Indeed, if we define a variable substitution ρ to be invertible for term M if there is exactly one M′ such that [ρ]M′ = M, then linearity is a sufficient, but not necessary condition. However, it is necessary that ρ must be linear if restricted to the free variables of (β-normal!) M. Yet instead of computing the free variables of M, checking that ρ is invertible, inverting ρ and applying the result to M, we can directly try to invert the effect of the substitution ρ on M.

For a variable substitution Ψ ⊢ ρ ⇐ Φ and a term or substitution α ::= M | R | τ in context Ψ, we define the partial operation [ρ/Φ̂]^{−1}α by

[ρ/Φ̂]^{−1}x  = y  if x/y ∈ ρ/Φ̂ and there is no z ≠ y with x/z ∈ ρ/Φ̂,

undefined otherwise

[ρ/Φ̂]^{−1}c  = c
[ρ/Φ̂]^{−1}(u[τ]) = u[τ′] where τ′ = [ρ/Φ̂]^{−1}τ

and homeomorphic in all other cases by

[ρ/Φ̂]^{−1}(R M) = R′ M′  where R′ = [ρ/Φ̂]^{−1}R and M′ = [ρ/Φ̂]^{−1}M
[ρ/Φ̂]^{−1}(π R) = π R′  where R′ = [ρ/Φ̂]^{−1}R
[ρ/Φ̂]^{−1}(λx. M) = λx. M′  if x not declared or free in ρ
and M′ = [ρ, x / Φ̂, x]^{−1}M
[ρ/Φ̂]^{−1}(M , N) = (M′ , N′) where M′ = [ρ/Φ̂]^{−1}M and N′ = [ρ/Φ̂]^{−1}N

[ρ/Φ̂]^{−1}(·)  = ·
[ρ/Φ̂]^{−1}(τ, M) = τ′, M′  if τ′ = [ρ/Φ̂]^{−1}τ and M′ = [ρ/Φ̂]^{−1}M .

We can show by induction on α, that inverse substitution [ρ/Φ̂]^{−1}α is correct and commutes with meta substitutions.

Lemma 4 (Inverse and meta-substitution commute). Let ρ be a variable substitution, and α ::= M | R | τ. If [ρ/Φ̂]^{−1}α and [ρ/Φ̂]^{−1}([[θ]]α) exist then [ρ/Φ̂]^{−1}([[θ]]α) = [[θ]]([ρ/Φ̂]^{−1}α).

Proof. By simultaneous induction on the structure of α. ⊓ ⊔ Lemma 5 (Soundness of inverse substitution). If [ρ/Φ̂]^{−1}α exists then [ρ]_{Φ}([ρ/Φ̂]^{−1}α) = α.

Proof. By simultaneous induction on the structure of α. ⊓ ⊔

Lemma 6 (Completeness of inverse substitution). If [ρ]_{Φ}α = α′ and ρ ↾ FV(α) is linear then α = [ρ/Φ̂]^{−1}α′ exists.

Proof. By simultaneous induction on the structure of α. ⊓ ⊔

3.4 Pruning

If the constraint u[σ] = M has a solution θ, then [[[θ]]σ]θ(u) = [[θ]]M, and since θ is closed (FV(θ) = ∅), we have FV(σ) ⊇ FV([[θ]]σ) ⊇ FV([[[θ]]σ]θ(u)) ⊇ FV([[θ]]M) (note that a hereditary substitution can remove free variables). Thus, if FV(M) ⊈ FV(σ) we can try to find a most general meta-substitution η which prunes the free variables of M that are not in the range of σ, such that FV([[η]]M) ⊆ FV(σ). For instance, in case u[x] = suc v[x, y], the meta-substitution x, y. v′[x]/v does the job. However, pruning may fail for one of the following reasons:

1. Offending variables occur rigidly, like the y in u[x] = c y v[x, y]. This constraint is unsolvable.

2. The flexible occurrence of an offending variable is under another meta variable, like y in u[x] = v[x, w[x, y]]. Here, two minimal pruning substitutions η_{1} = x, y. v′[x]/v and η_{2} = x, y. w′[x]/w exist which are not instances of each other—applying pruning might lose solutions.

3. The offending flexible occurrence could be eliminated by the correct solution. For instance, consider the case u : C[x:A] and v : C[z : (A → A → A) → A] and constraint

x:A, y:A ⊢ u[x] = v[λk. k x y] : C.

The offending variable y occurs flexibly in this constraint and rigidly in v’s substitution. If we pruned away v’s dependency on z, we would lose the partial solution θ(v) = z. z (λxλy.x) which would simplify the constaint to u[x] = x. The point here is that y, although it occurs rigidly in λk. k x y, it is in an eliminateable position since the meta-substitution for v could place that term in a context that reduces y away. There are rigid occurences that cannot be eliminated in such a way, we call these occurrences bad, see judgement bad occ_{y} N in Fig. 4.

We restrict pruning to situations u[ρ] = M where ρ is a variable substitution. This is because we view pruning as a preparatory step to inverting ρ on M— which only makes sense for variable substitutions. Also, we do not consider partial pruning, as in pruning y from v in the situation u[x] = v[x, y, w[x, y]], obtaining u[x] = v′[x, w[x, y]]. Such extensions to pruning are conceivable, but we have no data indicating that they strengthen unification significantly in practice. We employ the following judgments to define pruning (see Fig. 4):

Δ ⊢ prune_{ρ} M ⇒ Δ′; η prune M such that FV([[η]]M) ⊆ ρ
prune ctx_{ρ}(τ / Ψ_{1}) ⇒ Ψ_{2} prune τ such that FV^{rig}([τ]wk_{Ψ_{2}}) ⊆ ρ.

bad occ_{x} M Term M has a non-eliminateable occurrence of variable x.

\overline{bad occ_{x} E[x]}  \frac{bad occ_{x} M}{bad occ_{x} λy. M} x ≠ y  \frac{bad occ_{x} M_{1}  bad occ_{x} M_{2}}{bad occ_{x} (M_{1}, M_{2})}

prune ctx_{ρ}(τ / Ψ_{1}) ⇒ Ψ_{2} Prune substitution τ : Ψ_{1}, returning a sub-context Ψ_{2} of Ψ_{1}. (I.e., Ψ_{1} ⊢ wk_{Ψ_{2}} : Ψ_{2}.)

prune ctx_{ρ}(· / ·) ⇒ ·

\frac{prune ctx_{ρ}(τ / Ψ_{1}) ⇒ Ψ_{2} bad occ_{x} M for some x ∈ ρ}{prune ctx_{ρ}(τ, M / Ψ_{1}, y:A) ⇒ Ψ_{2}}

\frac{prune ctx_{ρ}(τ / Ψ_{1}) ⇒ Ψ_{2}  FV(M) ⊆ ρ  A′ = [wk_{Ψ 2}/Ψ̂_{2}]^{−1}A exists}{prune ctx_{ρ}(τ, M / Ψ_{1}, x:A) ⇒ Ψ_{2}, x:A′}

Δ ⊢ prune_{ρ} M ⇒ Δ′; η Prune term M, returning Δ′ ⊢ η ⇐ Δ.

\frac{v:B[Ψ_{1}] ∈ Δ prune ctx_{ρ}(τ / Ψ_{1}) ⇒ Ψ_{2} Ψ_{2} ≠ Ψ_{1} B′ = [wk_{Ψ_{2}}/Ψ̂_{2}]^{−1}B η = Ψ̂_{1}.v′[wk_{Ψ_{2}}]/v}{Δ ⊢ prune_{ρ}(v[τ]) ⇒ [[η]](Δ, v′:B′[Ψ_{2}]); η}

\frac{v:B[Ψ_{1}] ∈ Δ  prune ctx_{ρ}(τ / Ψ_{1}) ⇒ Ψ_{1}}{Δ ⊢ prune_{ρ}(v[τ]) ⇒ Δ; id_{Δ}}  \frac{x ∈ ρ}{Δ ⊢ prune_{ρ} x ⇒ Δ; id_{Δ}}

\overline{Δ ⊢ prune_{ρ} c ⇒ Δ; id_{Δ}}  \frac{Δ ⊢ prune_{ρ} R ⇒ Δ_{1}; η_{1}  Δ_{1} ⊢ prune_{ρ}([[η_{1}]]M) ⇒ Δ_{2}; η_{2}}{Δ ⊢ prune_{ρ}(R M) ⇒ Δ_{2}; [[η_{2}]]η_{1}}

\frac{Δ ⊢ prune_{ρ} M ⇒ Δ′; η}{Δ ⊢ prune_{ρ}(π M) ⇒ Δ′; η}  \frac{Δ ⊢ prune_{ρ,x} M ⇒ Δ′; η}{Δ ⊢ prune_{ρ}(λx. M) ⇒ Δ′; η}

\frac{Δ ⊢ prune_{ρ} M ⇒ Δ_{1}; η_{1} Δ_{1} ⊢ prune_{ρ}([[η_{1}]]N) ⇒ Δ_{2}; η_{2}}{Δ ⊢ prune_{ρ} (M , N) ⇒ Δ_{2}; [[η_{2}]]η_{1}}

Fig. 4. Pruning.

The second judgement is applied to subterms v[τ] of M to prune substitution τ with, say, domain Ψ_{1}. We look at each term N in τ which substitutes for an x:A of Ψ_{1}. If N has a bad occurrence of a variable y ∉ ρ, we discard the entry x:A from the domain Ψ_{1}, thus, effectively removing N from τ. If N has no occurrence of such an y we keep x:A. However, since we might have removed prior entries from Ψ_{1} we need to ensure A is still well-formed, by validating that its free variables are bound in the pruned context. Pruning fails if N has a occurrence of a y ∉ ρ which is not bad, for instance flexible or rigid in an eliminateable position. Examples:

− prune ctx_{x}(c x, y / x′:A, y′:B) ⇒ x′:A bad occurrence y
− prune ctx_{y}(c x, u[y] / x′:A, y′:B) ⇒ y′:B bad occurrence c x
− prune ctx_{y}(λz. z x, y / x′:A, y′:B)  fails occ. of x eliminateable
− prune ctx_{y}(u[x], y / x′:A, y′:B)  fails flexible occurrence u[x]

Pruning a term M with respect to ρ ensures that all rigid variables of M are in the range of ρ (see variable rule). Also, for each rigid occurrence of a metavariable v[τ] in M we try to prune the substitution τ. If τ is already pruned, we leave v alone; otherwise, if the domain Ψ_{1} of τ shrinks to Ψ_{2} then we replace v : B[Ψ_{1}] by a new meta-variable v′ : B[Ψ_{2}] with domain Ψ_{2}. However, we need to ensure that the type B still makes sense in Ψ_{2}; otherwise, pruning fails. The last check is strengthening B from Ψ_{1} to Ψ_{2} and can be implemented as [wk_{Ψ_{2}}/Ψ̂_{2}]^{−1}B which exists whenever FV(B) ⊆ Ψ̂_{2}.

Lemma 7 (Bad occurrences stay). Let D :: bad occ_{x} M.

1. If x ≠ y, then D′ :: bad occ_{x} [N/y]M, and the derivation height of D′ is the same as the one of D.

2. x ∈ FV^{rig}(E[M]).

3. If y ∈ FV^{rig}(N) then x ∈ FV^{rig}([M/y]N).

Proof.

1. By induction on bad occ_{x} M.

2. By induction on D :: bad occ_{x} M. In case M = E′[x] we have trivially x ∈ FV^{rig}(E[E′[x]]). If M = λy. M′ then either E is empty (trivial) or E = E′[• N]. Then E[M] = E′[[N/y]M′], and by part 1 we get bad occ_{x} [N/y]M′ with a smaller derivation height than D. We conclude by induction hypothesis. If M = (M_{1}, M_{2}) then either E is empty (trivial) or E = E′[fst •] or E = E′[snd •]. In case of fst, E[M] = E′[M_{1}] and we conclude by induction hypothesis. Case snd analogously.

3. By induction on β-normal form N. If N is a function λz. N′ or a pair (N′, N′′), proceed with N′. If N = E[y] then apply part 2. Otherwise N is a neutral which does not have y as head variable, which implies that hereditarily substituting y will yield a neutral with the same spine form. If N = π R then y ∈ FV^{rig}(R) and [M/y]N = π R′ with R′ = [M/y]R. By induction hypothesis, x ∈ FV^{rig}(R′) = FV^{rig}([M/y]N). If N is an application R′ N′ then [M/y]N = R′′ N′′ with R′′ = [M/y]R′ and N′′ = [M/y]N′. Either y ∈ FV^{rig}(R′) or y ∈ FV^{rig}(N′) and we can conclude with the respective induction hypothesis, since FV^{rig}(R′′ N′′) = FV^{rig}(R′′) ∪ FV^{rig}(N′′). ⊓ ⊔

Lemma 8 (Soundness and completeness of pruning).

1. If Δ ⊢_{K} Ψ_{1} ctx and prune ctx_{ρ}(τ / Ψ_{1}) ⇒ Ψ_{2} then Δ ⊢_{K} Ψ_{2} ctx and FV([τ]wk_{Ψ_{2}}) ⊆ ρ. Additionally, if x ∈ Ψ_{1} \ Ψ_{2} then FV^{rig}([τ]x) ⊈ ρ.

2. If Δ ⊢ prune_{ρ} M ⇒ Δ′; η then Δ′ ⊢_{K} η ⇐ Δ and FV([[η]]M) ⊆ ρ. Also, if θ solves Ψ ⊢ u[ρ] = M_{0}{M}^{rig} : C then there is some θ′ such that θ = [[θ′]]η.

Proof. Each by induction on the pruning derivation.

We detail 2., existence of θ′: Since θ is a solution of the constraint, [[θ]](u[ρ]) = [[[θ]]ρ](θ(u)) = [ρ](θ(u)) = [[θ]]M_{0}, in particular FV(ρ) = ρ ⊇ FV([[θ]]M_{0}). This entails FV([[θ]]M) ⊆ ρ.

Consider the interesting case M = v[τ] with prune ctx_{ρ}(τ / Ψ_{1}) ⇒ Ψ_{2} and η = Ψ̂_{1}.v′[wk_{Ψ_{2}}]/v. Let N = θ(v). We have FV([[[θ]]τ]N) ⊆ ρ. If we can show FV(N) ⊆ Ψ̂_{2}, then we can finish by setting θ′ = θ, Ψ̂_{2}.N/v′.

Assume now some x ∈ FV(N) with x ∉ Ψ̂_{2}. By 1., FV^{rig}([τ]x) ⊈ ρ, which entails that FV([[[θ]]τ]x) ⊈ ρ. This is in contradiction to FV([[[θ]]τ]N) ⊆ ρ. ⊓ ⊔

In an implementation, we may combine pruning with inverse substitution and the occurs check. Since we already traverse the term M for pruning, we may also check whether [ρ/Φ̂]^{−1}M exists and whether u occurs in M.

3.5 Unifying two identical existential variables

Any solution Φ̂.N/u for a meta variable u : A[Φ] with constraint u[ρ] = u[ξ] must fulfill [ρ]N = [ξ]N, which means that [ρ]x = [ξ]x for all x ∈ FV(N). This means that u can only depend on those of its variables in Φ that are mapped to the same term by ρ and ξ. Thus, we can substitute u by Φ̂.v[ρ′] where ρ′ is the intersection of substitutions ρ and ξ. Similarly to context pruning, we obtain ρ′ as [ρ]wk_{Φ′}, which identical to [ξ]wk_{Φ′}, where Φ′ is a subcontext of Φ mentioning only the variables that have a common image under ρ and ξ. This process is given as judgement ρ ∩ ξ : Φ ⇒ Φ′ with the following rules:

\begin{matrix}· ∩ · : · ⇒ · \\ {ρ ∩ ξ : Φ ⇒ Φ′ \atop (ρ, y) ∩ (ξ, y) : (Φ, x:A) ⇒ (Φ′, x:A)} & \begin{matrix}ρ ∩ ξ : Φ ⇒ Φ′ & z ≠ y \\ (ρ, z) ∩ (ξ, y) : (Φ, x:A) ⇒ Φ′ \end{matrix} \end{matrix}

Lemma 9 (Soundness of intersection). If Δ; Ψ ⊢_{K} ρ, ξ ⇐ Φ and ρ∩ξ : Φ ⇒ Φ′, then Δ ⊢_{K} Φ′ ctx and Δ; Φ ⊢_{K} wk_{Φ′} ⇐ Φ′ and z ∈ dom(Φ′) iff ρ(z) = ξ(z).

Proof. By structural induction on the first derivation.

We consider the interesting case, where we actually retain a declaration x:A because the two substitutions map x to the same variable y.

{ρ ∩ ξ : Φ ⇒ Φ′ \atop (ρ, y) ∩ (ξ, y) : (Φ, x:A) ⇒ Φ′, x:A}

The main challenge is to show that type A is well-formed even in the subcontext Φ′ of Φ, which is the case if FV(A) ⊆ dom(Φ′).

From the assumption Δ; Ψ ⊢_{K} (ρ, y) ⇐ (Φ, x:A) we get Δ; Ψ ⊢_{K} ρ ⇐ Φ and Ψ(y) =_{K} [ρ]A by inversion, and the same for ξ. This allows us to apply the the induction hypothesis, which yields Δ ⊢_{K} Φ′ ctx and Δ; Φ ⊢_{K} wk_{Φ′} ⇐ Φ′ and dom(Φ′) = {z | ρ(z) = ξ(z)}. Since [ρ]A =_{K} Ψ(y) =_{K} [ξ]A, we have for all z ∈ FV(A) that ρ(z) =_{K} ξ(z). Since this is an equation between variables, the constraints K on meta-variables do not matter, and we even have ρ(z) = ξ(z). Yet this means that z ∈ dom(Φ′), thus, we obtain Δ; Φ′ ⊢_{K} A ⇐ type by strengthening. This entails Δ ⊢_{K} (Φ′, x:A) ctx, hence, trivially, Δ; (Φ, x:A) ⊢_{K} wk_{Φ′,x:A} ⇐ (Φ′, x:A). Finally, dom(Φ′, x:A) = {z | ρ(z) = ξ(z)} follows from this property for Φ′ and the fact ρ(x) = y = ξ(x). ⊓ ⊔

Let us now reconsider the rule “Same meta-variable”.

\begin{matrix}Δ ⊩ K ∧ Ψ ⊢ u[ρ] = u[ξ] : C & ↦ & Δ, v:A[Φ′] ⊩ K + Φ ⊢ u ← v[wk_{Φ′}] : A \\ u:A[Φ] ∈ Δ & & if ρ ∩ ξ : Φ ⇒ Φ′ \end{matrix}

We have just shown that the resulting Φ′ of computing the intersection of ρ and ξ, is indeed well-formed. We can also justify why in the unification rule itself the type A of two existential variables must be well-typed in the pruned context Φ′. Recall that by typing invariant, we know that Δ; Ψ ⊢_{K} ρ ⇐ Φ and Δ; Ψ ⊢_{K} ξ ⇐ Φ and [ρ]A =_{K} [ξ]A. But this means that A can only depend on the variables mapped to the same term by ρ and ξ. Since Φ_{0} is exactly the context which captures those shared variables, A must also be well-typed in Φ_{0} modulo K.

Note that intersection cannot easily be extended beyond variable substitutions. For instance, consider the following problem:

(λf. f ∘ f, g, N) ∩ (λf. f, g ∘ g, N) : (x : A^{4}, y : A^{2}, z : P (x y)) ⇒ ?

where N : P (g ∘ g) and A^{4} := (A → A) → A → A and A^{2} := A → A, and f ∘g := λn. f (g n) abbreviates function composition. We cannot remove x and y from the context only because the two substitutions differ at these positions. The resulting context (z : P (x y)) would be ill-typed. The difference to the variable case is that substitution is no longer injective, i.e., we can have [σ]M = [τ]M but σ(x) ≠ τ(x) for some x ∈ FV(M).

4 Correctness

Theorem 1 (Termination). The algorithm terminates and results in one of the following states:

– A solved state where only assignments Ψ ⊢ u ← M : A remain.

– A stuck state, i.e., no transition rule applies.

– Failure ⊥.

Proof. Let the size |M| of a term be as usual the number of nodes and leaves in its tree representation, with the exception that we count λ-nodes twice. This modification has the effect that |λx.M|+|R| > |M|+|R x|, hence, an η-expanding decomposition step also decreases the sum of the sizes of the involved terms [7]. We define the size |A[Φ]| of a type A in context Φ by |P [Φ]| = 1 + ∑_{A∈Φ} |A[]|, |(Πx:A. B)[Φ]| = 1 + |B[Φ, x:A]| and |(Σx:A. B)[Φ]| = 1 + |A[Φ]| + |B[Φ]|. The size of a type can then be obtained as |A| = |A[]| and the size of a context as |Φ| = ∑_{A∈Φ} |A|. The purpose of this measure is to give Σ-types a large weight that can “pay” for flattening.

Let the weight of a solved constraint be 0, whereas the weight |K| for a constraint Ψ ⊢ M = M′ : C be the ordinal (|M|+|M′|)ω+|Ψ| if a decomposition step can be applied, and simply |Ψ| else. Similarly, let the weight of constraint Φ | R:A ⊢ E = E′ be (|E| + |E′|)ω + |Ψ|. Finally, let the weight |Δ ⊩ K| of a unification problem be the ordinal

∑_{u:A[Φ]∈Δ active} |A[Φ]|ω^{2} + ∑_{K∈K} |K|.

By inspection of the transition rules we can show that each unification step reduces the weight of the unification problem. ⊓ ⊔

4.1 Solutions to unification

A solution to a set of equations K is a meta-substitution θ for all the metavariables in Δ s.t. Δ′ ⊢ θ ⇐ Δ and

1. for every Ψ ⊢ u ← M : A in K we have Ψ̂.M/u ∈ θ,

2. for all equations Ψ ⊢ M = N : A in K, we have [[θ]]M = [[θ]]N.

A ground solution to a set of equations K can be obtained from a solution to K by applying a grounding meta-substitution θ′ where · ⊢ θ′ ⇐ Δ′ to the solution θ. We write θ ∈ Sol(Δ ⊩ K) for a ground solution to the constraints K.

Before we prove that transitions preserve solutions, we first prove that there always exists a meta-substitution relating the original meta-variable context Δ_{0} to the meta-variable context Δ_{1} we transition to. It is useful to state this property in isolation, although it is also folded into Theorem 2.

Lemma 10. If Δ_{0} ⊩ K_{0} ↦ Δ_{1} ⊩ K_{1} then there exists a meta-substitution θ s.t. Δ_{1} ⊢_{K_{1}} θ ⇐ Δ_{0}.

Proof. By case analysis on the unification steps. ⊓ ⊔

We also observe that if we start in a state Δ_{0} ⊩ K_{0} and transition to a state Δ_{1} ⊩ K_{1} the meta-variable context strictly grows, i.e., dom(Δ_{0}) ⊆ dom(Δ_{1}). We subsequently show that if we have a solution for Δ_{0} ⊩ K_{0}, then transitioning to a new state Δ_{1} ⊩ K_{1} will not add any additional solutions nor will it destroy some solution we may already have. In other words, any additional constraints which may be added in Δ_{1} ⊩ K_{1} are consistent with the already existing solution.

Theorem 2 (Transitions preserve solutions). Let Δ_{0} ⊩ K_{0} ↦ Δ_{1} ⊩ K_{1}.

1. If θ_{0} ∈ Sol(Δ_{0} ⊩ K_{0}) then there exists a meta-substitution θ′ s.t. Δ_{1} ⊢_{K_{1}} θ′ ⇐ Δ_{0} and a solution θ_{1} ∈ Sol(Δ_{1} ⊩ K_{1}) such that [[θ_{1}]]θ′ = θ_{0}.

2. If θ_{1} ∈ Sol(Δ_{1} ⊩ K_{1}) then [[θ_{1}]]wk_{Δ_{0}} ∈ Sol(Δ_{0} ⊩ K_{0}).

Proof. Proof by case analysis on the transitions. We only show the cases to prove that we are forward closed (statement 1). The second statement, that unification steps are backwards closed, is obvious: by if we transition from Δ_{0} ⊩ K_{0} to Δ_{1} ⊩ K_{1} then there exists a meta-substitution Δ_{1} ⊢_{K_{1}} θ ⇐ Δ_{0}; hence, by composition [[θ_{1}]]θ is ground and is a solution for Δ_{0} ⊩ K_{0}.

In all the following cases, θ_{0} is a solution for K_{0}.

Decomposition. Since Δ_{0} does not change in any of the decomposition rules, the solution is almost trivially preserved; for the η-contraction rules, we simply observe that equality is always modulo η. For the eliminating projections transition, we use the substitution lemma and observe that meta-substitutions and ordinary substitutions commute.

Lowering. Let u : (Πx:A.B)[Φ] ∈ Δ active and

Δ ⊩ K ↦ (Δ, v:B[Φ, x:A] ⊩ K) + (Φ ⊢ u ← λx.v : Πx:A. B)

Let Φ̂.M := θ_{0}(u) and observe ·; [[θ_{0}]]Φ ⊢ M ⇐ [[θ_{0}]](Πx:A.B). By inversion on typing, M = λx.N and ·; [[θ_{0}]](Φ, x:A) ⊢ N ⇐ [[θ_{0}]]B. Hence, (Φ̂, x).N is a solution for v. Choose θ′ = wk_{Δ_{0}} and θ_{1} = θ, (Φ̂, x).N/v. Since v is a new meta variables, θ_{1} is still a solution for the old state Δ ⊩ K.

The case for lowering Σ-types is similar.

Flattening. Using the substitution lemma, solutions are preserved.

Pruning. θ_{0} is a solution for K_{0} and the active meta-variable u:A[Φ] ∈ Δ_{0}. Hence, Φ̂.M/u ∈ θ_{0}. Moreover, if we have the constraint Ψ ⊢ u[ρ] = N : B, we have [ρ]M = [[θ_{0}]]N. By previous soundness lemma for pruning, Δ_{p} ⊢ θ_{p} ⇐ Δ_{0} and there exists a θ′ s.t. [[θ′]]θ_{p} = θ.

Same meta-variable. θ_{0} is a solution for K_{0} and the active meta-variable u:A[Φ] ∈ Δ_{0}. Hence, Φ̂.M/u ∈ θ and ·; [[θ_{0}]](Φ) ⊢ M ⇐ [[θ_{0}]]A. Moreover, [ρ]M = [ξ]M. Therefore, FV([ρ]M) = FV([ξ]M) and Φ_{0} contains exactly those meta-variables which are shared among ρ and ξ by definition of ρ ∩ ξ; moreover, we must have [[θ_{0}]]([ρ]A) = [[θ_{0}]]([η]A). Since meta-substitutions commute with variable substitutions, we have [ρ]([[θ_{0}]]A) = [η]([[θ_{0}]]A), hence FV(M) = Φ̂_{0} and FV([[θ_{0}]]A) = Φ̂_{0} and ·; [[θ_{0}]](Φ_{0}) ⊢ M ⇐ [[θ_{0}]]A; choosing id_{Δ_{0}} for θ′ and for θ_{1} = θ, Φ̂_{0}.M/v solutions are preserved.

Solving. θ_{0} is a solution for K_{0} and the active meta-variable u:A[Φ] ∈ Δ_{0}. Hence, Φ̂.N/u ∈ θ_{0}. Therefore, we have [ρ]N = [[θ]]M. By completeness of inverse substitution, we know N = [ρ/Φ]^{−1}([[θ]]M). By assumption we also know [ρ/Φ]^{−1}M = M′ exists. Therefore, by lemma that inverse and meta-substitution commute, we have N = [[θ]]([ρ/Φ]^{−1}M) = [[θ]]M′. Therefore, the solution θ_{0} is preserved. ⊓ ⊔ 4.2 Transitions preserve types

Our goal is to prove that if we start with a well-typed unification problem our transitions preserve the type, i.e., we can never reach an ill-typed state and hence, we cannot generate a solution which may contain an ill-typed term. Lemma 11 (Equality modulo is preserved by transitions). If Δ_{0} ⊩ K_{0} ↦ Δ_{1} ⊩ K_{1} and A =_{K_{0}} B, then A =_{K_{1}} B.

Proof. Let θ be a solution for K_{0}; by assumption, we have that [[θ]]A = [[θ]]B. By theorem 2, transitions preserve solutions, we know θ is also a solution for K_{1}, and therefore A =_{K_{1}} B. ⊓ ⊔

In the statement below it is again important to note that the meta-context strictly grows, i.e., Δ_{0} ⊆ Δ_{1} and that there always exists a meta-substitution θ which maps Δ_{0} to Δ_{1}. Moreover, since transitions preserve solutions, if we have a solution for K_{0} there exists a solution for K_{1}.

Lemma 12 (Transitions preserve typing). Let Δ_{0} ⊩ K_{0} ↦ Δ_{1} ⊩ K_{1} and Δ_{1} ⊢_{K_{1}} θ ⇐ Δ_{0}.

1. If Δ_{0}; Ψ ⊢_{K_{0}} M ⇐ A then Δ_{1}; [[θ]]Ψ ⊢_{K_{1}} [[θ]]M ⇐ [[θ]]A.

2. If Δ_{0}; Ψ ⊢_{K_{0}} R ⇒ A then Δ_{1}; [[θ]]Ψ ⊢_{K_{1}} [[θ]]R ⇒ A′ and [[θ]]A =_{K_{1}} A′.

Proof. By induction on the derivation of Δ_{0}; Ψ ⊢_{K_{0}} J. Most cases are by inversion, appeal to induction hypothesis, and re-assembling the result. The most interesting case is transitioning between normal and neutral terms. Here we use the previous lemma on “Equality modulo preserved by transitions”. ⊓ ⊔

Next, we define when a set of equations which constitute a unification problem are well-formed using the judgment Δ_{0} ⊩_{K_{0}} K wf, which states that each equation Ψ ⊢ M = N : A must be well-typed modulo the equations in K_{0}, i.e., Δ_{0}; Ψ ⊢_{K_{0}} M ⇐ A and Δ_{0}; Ψ ⊢_{K_{0}} N ⇐ A . We simply write Δ_{0} ⊩ K wf to mean Δ_{0} ⊩_{K} K wf.

Lemma 13 (Equations remain well-formed under meta-substitutions). If Δ_{0} ⊩ K wf and Δ_{1} ⊢_{[[θ]]K} θ ⇐ Δ_{0} then Δ_{1} ⊩ [[θ]]K wf.

Proof. By assumption Δ_{0} ⊩ K wf. By definition, for every constraint Ψ ⊢ M = N : A ∈ K, we have Δ_{0}; Ψ ⊢_{K} M ⇐ A and Δ_{0}; Ψ ⊢_{K} N ⇐ A. By metasubstitution principle modulo (lemma 3), we know Δ_{1}; [[θ]]Ψ ⊢_{[[θ]]K} [[θ]]M ⇐ [[θ]]A and Δ_{1}; [[θ]]Ψ ⊢_{[[θ]]K} [[θ]]N ⇐ [[θ]]A, and hence Δ_{1} ⊢_{[[θ]]K} [[θ]]K wf. ⊓ ⊔

Lemma 14 (Well-formedness of equations is preserved by transitions). If Δ_{0} ⊩ K_{0} ↦ Δ_{1} ⊩ K_{1} and Δ_{0} ⊩_{K_{0}} K wf then Δ_{1} ⊢_{K_{1}} K wf.

Proof. By assumption Δ ⊩_{K_{0}} K wf, we know that for each Ψ ⊢ M = N : A ∈ K, Δ; Ψ ⊢_{K_{0}} M ⇐ A and Δ; Ψ ⊢_{K_{0}} N ⇐ A. By lemma 12, typing is preserved by transitions, we know that Δ; Ψ ⊢_{K_{1}} M ⇐ A and Δ; Ψ ⊢_{K_{1}} N ⇐ A. Therefore Δ ⊩_{K_{1}} K wf. ⊓ ⊔

Theorem 3 (Unification preserves types). If Δ_{0} ⊩ K_{0} wf and Δ_{0} ⊩ K_{0} ↦ Δ_{1} ⊩ K_{1} then Δ_{1} ⊩ K_{1} wf.

Proof. By case analysis on the transition rules and lemma 10.

Decomposition rules. We consider the decomposition rule for pairs. Let K_{0} be the set of equations which contains Ψ ⊢ (M_{1}, M_{2}) = (N_{1}, N_{2}) : Σx:A.B . By assumption we have Δ_{0}; Ψ ⊢_{K_{0}} (M_{1}, M_{2}) ⇐ Σx:A.B. By inversion, we have Δ_{0}; Ψ ⊢_{K_{0}} M_{1} ⇐ A and Δ_{0}; Ψ ⊢_{K_{0}} M_{2} ⇐ [M_{1}/x]_{A}(B). By assumption we have Δ_{0}; Ψ ⊢_{K_{0}} (N_{1}, N_{2}) ⇐ Σx:A.B. By inversion, we have Δ_{0}; Ψ ⊢_{K_{0}} N_{1} ⇐ A and Δ_{0}; Ψ ⊢_{K_{0}} N_{2} ⇐ [N_{1}/x]_{A}(B). Let K_{1} = K_{0} ∧ Ψ ⊢ M_{1} = N_{1} : A. Then Δ_{0} ⊩ K_{1} wf. Moreover, Δ_{0}; Ψ ⊢_{K_{1}} N_{2} ⇐ [M_{2}/x]_{A}(B). Hence, Ψ ⊢ M_{2} = N_{2} : [M_{1}/x]_{A}(B) is well-formed and Δ_{0} ⊩ K_{2} wf where we replace the constraint Ψ ⊢ (M_{1}, M_{2}) : Σx:A.B with Ψ ⊢ M_{1} = N_{1} : A ∧ Ψ ⊢ M_{2} = N_{2} : [M_{1}/x]_{A}(B) in K.

Next, we consider the decomposition rules for evaluation contexts. Let K_{0} be the set of equations containing Ψ | R : Πx:A. B ⊢ E[• M] = E′[• M′]. By assumption this constraint is well-typed, and hence Δ_{0}; Ψ ⊢_{K_{0}} R ⇒ Πx:A. B and Δ_{0}; Ψ ⊢_{K_{0}} R M ⇒ B_{2} and Δ_{0}; Ψ ⊢_{K_{0}} R M′ ⇒ B_{1} where B_{1} =_{K_{0}} B_{2}. In addition Δ_{0}; Ψ ⊢_{K_{0}} M ⇐ A and Δ_{0}; Ψ ⊢_{K_{0}} M′ ⇐ A. Let K_{1} = K_{0} ∧ Ψ ⊢ M = M′ : A. Clearly, Δ_{0} ⊩ K_{1} wf. Moreover, since the evaluation E[R M] and E′[R M′] are well-typed modulo K_{0} and the fact that Ψ ⊢ M = M′ : A, we have also that E′[R M] is well-typed modulo K_{1} and Ψ | R M : [M/x]B ⊢ E = E′ is well-typed in Δ_{0} modulo K_{1}. Therefore, we have Δ_{0} ⊩ K_{2} wf where K_{2} = K_{1} ∧ Ψ | R M : [M/x]B ⊢ E = E′.

Pruning rule. Let K_{0} be the set of equations containing Ψ ⊢ u[ρ] = M : A. By assumption, we know that Δ_{0}; Ψ ⊢_{K_{0}} u[ρ] ⇐ A and Δ_{0}; Ψ ⊢_{K_{0}} M ⇐ A.

By soundness of pruning (lemma 8), we know that Δ_{1} ⊢_{K_{0}} η ⇐ Δ_{0}. By lemma 13, we know that Δ_{1} ⊩ [[η]](K_{0}) wf.

Intersections. Let K_{0} be the set of equations containing Ψ ⊢ u[ρ] = u[ξ] : C. By assumption, we know that Δ_{0}; Ψ ⊢_{K_{0}} u[ρ] ⇐ C and Δ_{0}; Ψ ⊢_{K_{0}} u[ξ] ⇐ C. Let u : A[Φ] ∈ Δ. By inversion, we have [ξ]A =_{K_{0}} C =_{K_{0}} [ρ]A. This means FV([ξ]A) = FV([ρ]A) and by definition of ρ ∩ ξ : Φ ⇒ Φ_{0}, the context Φ_{0} will contain exactly those variables shared in ξ and ρ. By soundness lemma 9, we have Δ_{0} ⊢_{K_{0}} Φ_{0} ctx. Therefore, Δ_{0}; Φ_{0} ⊢_{K_{0}} A ⇐ type and (Δ_{0}, v:A[Φ_{0}]) mctx. By typing rules, we have (Δ_{0}, v:A[Φ_{0}]); Φ ⊢_{K_{0}} u ⇐ A and (Δ_{0}, v:A[Φ_{0}]); Φ ⊢_{K_{0}} v[wk_{Φ_{0}}] ⇐ A. Hence, Φ ⊢ u ← v[wk_{Φ_{0}} : A is well-typed in Δ_{0} modulo K_{0}. Hence, θ = Φ̂.v[wk_{Φ_{0}}]/u is a well-formed meta-substitution. By lemma 3, we have [[θ]]Δ ⊩ ([[θ]]K_{0} ∧ [[θ]]Φ ⊢ u ← M : [[θ]]A) wf.

Solving. Let K_{0} be the set of equations containing Ψ ⊢ u[ρ] = M : C. By assumption M′ = [ρ/Φ̂]^{−1}M exists and u:A[Φ] ∈ Δ. Since Δ_{0} ⊩ K_{0} wf, we also have Δ_{0}; Ψ ⊢_{K_{0}} M ⇐ C and Δ_{0}; Ψ ⊢_{K_{0}} u[ρ] ⇐ C. By inversion, we have C =_{K_{0}} [ρ]A. By assumption we have Δ_{0}; Φ ⊢_{K_{0}} M′ ⇐ A. Hence, θ = Φ̂.M′/u is a well-formed meta-substitution and by lemma 3, we have [[θ]]Δ_{0} ⊩ [[θ]](K_{0} ∧Φ ⊢ u ← M′ : A) wf. ⊓ ⊔

5 Conclusion

We have presented a constraint-based unification algorithm which solves higherorder patterns dynamically and showed its correctness. There are several key aspects of our algorithm: First, we define pruning formally and show soundness in the dependently typed case. Our pruning operation differs from previous formulations in how it treats non-patterns which may occur in the term to be pruned: if it encounters a non-pattern term M where FV(M) ⊆ ρ, then pruning may succeed; otherwise it fails. This strategy avoids non-termination problems present in previous formulations [3], but is also less ambitious than the algorithm proposed by Reed [17]. We have extended higher-order pattern unification to handle Σ-types; this has been an open problem so far, yet it is of practical relevance:

1. In LF-based systems such as Beluga, Twelf or Delphin, a limited form of Σ-types arises due to context blocks: Σ-types are used to introduce several assumptions simultaneously. For Beluga, the second author has implemented the flattening of context blocks and it works well in type reconstruction.

2. In dependently typed languages such as Agda, Σ-types, or, more generally, record types, are commonly used but unification has original not been adapted to records. McBride [9, p.6] gives a practical example where the unification problem T (fst γ) (snd γ) = T′ γ appears. Using the techniques presented in this paper, the first author has extended Agda’s unification algorithm to solve those kinds of problems.

Correctness of our unification constraint solver is proved using typing modulo [17]. This is possible since we have no constraints on the type level and we are dealing with terms whose normalization via hereditary substitutions can be defined by recursion on their type. Even in the presence of unsolvable constraints, which lead to ill-typed terms, normalization is terminating. This does not scale to Agda which has large eliminations and unification on the type level; there, ill-typed terms may lead to divergence of type reconstruction. A solution has been described by Norell [12]: unsolved constraints block normalization, thus guaranteeing termination of the unification algorithm. The idea has been implemented in Agda 2 and been extended to Σ-types and the unification rules described in this article.

Acknowledgments. We thank Jason Reed for his insightful work and his explanations given via email. Thanks to Conor McBride for in-depth comments on this text and his suggestions for improvement. We also acknowledge the anonymous referees who have given constructive critique on a previous version of this article.

References

1. Andreas Abel and Brigitte Pientka. Higher-order dynamic pattern unification for dependent types and records. In C.-H. Luke Ong, editor, Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011, Proceedings, volume 6690 of Lecture Notes in Computer Science, pages 10–26. Springer, 2011.

2. Iliano Cervesato and Frank Pfenning. A linear spine calculus. Journal of Logic and Computation, 13(5):639–688, 2003.

3. Gilles Dowek, Thérèse Hardin, Claude Kirchner, and Frank Pfenning. Unification via explicit substitutions: The case of higher-order patterns. In Joint International Conference Logic Programming, pages 259–273. MIT Press, 1996.

4. Dominic Duggan. Unification with extended patterns. Theoretical Computer Science, 206(1-2):1–50, 1998.

5. Conal Elliott. Extensions and Applications of Higher-Order Unification. PhD thesis, School of Computer Science, Carnegie Mellon University, 1990.

6. Roland Fettig and Bernd Löchner. Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type. In 7th International Conference on Rewriting Techniques and Applications (RTA’96), LNCS 1103, pages 347–361. Springer, 1996.

7. Healfdene Goguen. Justifying algorithms for βη conversion. In 8th Int. Conf. on Foundations of Software Science and Computational Structures (FoSSaCS’05), LNCS 3441, pages 410–424. Springer, 2005.

8. W. D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225–230, 1981.

9. Conor McBride. Outrageous but meaningful coincidences: Dependent type-safe syntax and evaluation. In ACM SIGPLAN Workshop on Genetic Programming (WGP’10), pages 1–12. ACM, 2010.

10. Dale Miller. Unification of simply typed lambda-terms as logic programming. In Eighth International Logic Programming Conference, pages 255–269. MIT Press, 1991.

11. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM Transactions on Computational Logic, 9(3):1–49, 2008.

12. Ulf Norell. Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, Göteborg, Sweden, September 2007.

13. Frank Pfenning and Carsten Schürmann. System description: Twelf — a metalogical framework for deductive systems. In 16th International Conference on Automated Deduction (CADE-16), LNAI 1632, pages 202–206. Springer, 1999.

14. Brigitte Pientka. Tabled higher-order logic programming. PhD thesis, Department of Computer Science, Carnegie Mellon University, 2003. CMU-CS-03-185.

15. Brigitte Pientka and Joshua Dunfield. Beluga: a framework for programming and reasoning with deductive systems (System Description). In 5th International Joint Conference on Automated Reasoning (IJCAR’10), LNAI 6173, pages 15–21, 2010.

16. Adam Poswolsky and Carsten Schürmann. System description: Delphin—a functional programming language for deductive systems. In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP’08), ENTCS 228, pages 135–141. Elsevier, 2009.

17. Jason Reed. Higher-order constraint simplification in dependent type theory. In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP’09), 2009.

18. Jason Reed. A Hybrid Logical Framework. PhD thesis, School of Computer Science, Carnegie Mellon University, 2009.

19. Anders Schack-Nielsen and Carsten Schürmann. Pattern unification for the lambda calculus with linear and affine types. In Karl Crary and Marino Miculan, editors, 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2010), Edinburgh, Scotland, UK, July 14, 2010, volume 34 of Electronic Proceedings in Theoretical Computer Science, pages 101–116, 2010.

20. Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework I: Judgements and properties. Technical report, School of Computer Science, Carnegie Mellon University, Pittsburgh, 2003.

A Hereditary substitution

Normal forms are maintained through the use of hereditary substitution, written as [N/x]_{A}(B) to guarantee that when we substitute term N which has type A for the variable x in the type B, we obtain a type B′ which is in normal form. Hereditary substitutions continue to substitute, if a redex is created; for example, when replacing naively x by λy.c y in the object x z, we would obtain (λy.c y) z which is not in normal form and hence not a valid term in our grammar. Hereditary substitutions continue to substitute z for y in c y to obtain c z as a final result.

Hereditary substitution can be defined recursively considering the term to which the substitution operation is applied and the type of the object which is being substituted. We define the hereditary substitution operations for normal object, neutral objects and substitutions. The hereditary substitution operations will be defined by nested induction, first on the structure of the type A and second on the structure of the objects N, R, and σ. In other words, we either go to a smaller type, in which case the objects themselves can become larger, or the type remains the same and the objects become smaller. We write A ≤ B and A < B if A occurs in B (as a proper sub-expression in the latter case)^{4}. Hereditary substitution is defined in Figure 5. For an in depth discussion, we refer the reader to Nanevski et al. [11].

If the original term is not well-typed, a hereditary substitution, though terminating, cannot always return a meaningful term. We formalize this as failure to return a result. However, on well-typed terms, hereditary substitution will always return well-typed terms. The definition for single hereditary substitutions can be easily extended to simultaneous substitutions substitution written as [σ]_{Ψ} (M). We annotate the substitution with the sub-script Ψ for two reasons. First, σ itself does not carry its domain and hence we will look up the instantiation for a variable x in σ/Ψ. Second, we rely on the type of x in the context Ψ to guarantee that applying σ to an object terminates. Either we apply σ to sub-expressions or the type of the object we substitute will be smaller. Subsequently, we often omit the typing subscript at the substitution operation for better readability.

4 To ensure termination, it suffices to rely on type approximations of the dependent type; we leave this out from the discussion.

\underline{26}

Normal terms / types [M/x]_{A}(Πy:B_{1}.B_{2}) = Πy:B′_{1}.B′_{2} where B′_{1} = [M/x]_{A}(B_{1}) and B′_{2} = [M/x]_{A}(B_{2}),

y ∉ FV(M), and y ≠ x

[M/x]_{A}(Σy:B_{1}.B_{2}) = Σy:B′_{1}.B′_{2} where B′_{1} = [M/x]_{A}(B_{1}) and B′_{2} = [M/x]_{A}(B_{2}),

y ∉ FV(M), and y ≠ x

[M/x]_{A}(type)  = type
[M/x]_{A}(λy.N) = λy.N′ where [M/x]_{A}(N) = N′, y ∉ FV(M), and y ≠ x
[M/x]_{A}(N_{1}, N_{2}) = (N′_{1}, N′_{2}) where [M/x]_{A}(N_{1}) = N′_{1} and [M/x]_{A}(N_{1}) = N′_{1}
[M/x]_{A}(R)  = M′  if [M/x]_{A}(R) = M′ : A′
[M/x]_{A}(R)  = R′  if [M/x]_{A}(R) = R′
[M/x]_{A}(N)  fails  otherwise

Neutral terms

[M/x]_{A}(x)  = M : A
[M/x]_{A}(y)  = y  if y ≠ x
[M/x]_{A}(u[σ])  = u[σ′]  where [M/x]_{A}(σ) = σ′
[M/x]_{A}(R N)  = R′N′  where [M/x]_{A}(R) = R′ and [M/x]_{A}(N) = N′
[M/x]_{A}(R N)  = M′′ : B if [M/x]_{A}(R) = λy.M′:Πy:A_{1}.B where
Πx:A_{1}.B ≤ A and [M/x]_{A}(N) = N′
and [N′/y]_{A_{1}}(M′) = M′′
[M/x]_{A}(πR) = πR′ where [M/x]_{A}(R) = R′
[M/x]_{A}(fst R)  = M_{1} : B_{1} where [M/x]_{A}(R) = (M_{1}, M_{2}):Σx:B_{1}.B_{2} where
Σx:B_{1}.B_{2} ≤ A
[M/x]_{A}(snd R)  = M_{2} : B_{2} where [M/x]_{A}(R) = (M_{1}, M_{2}):Σx:B_{1}.B_{2} where
Σx:B_{1}.B_{2} ≤ A
[M/x]_{A}(R) fails otherwise

Substitution

[M/x]_{A}(·)  = ·
[M/x]_{A}(σ , N)  = (σ′ , N′) where [M/x]_{A}(σ) = σ′ and [M/x]_{A}(N) = N′
[M/x]_{A}(σ)  fails  otherwise

Fig. 5. Hereditary substitutions for LF objects with contextual variables

B Meta substitution

The single meta-substitution operation is written as [[Ψ̂.M/u]]_{A[Ψ]}(N) and the simultaneous meta-substitution is written as [[θ]]_{Δ}(N) . Subsequently, we define the application of the single meta-substitution to a given term and type, but the simultaneous meta-substitution definition can be easily derived from it.

As we annotate meta-substitutions with their type, we can appropriately annotate σ′ with its domain Ψ to obtain M′. Without annotating meta-substitution with the type C[Ψ], we would not be able annotate the operation [σ′]M appropriately. Because M′ may not be neutral, we may trigger a β-reduction and we return M′ together with its (approximate) type C.

Applying the meta-substitution to an LF object will terminate for the same reasons as the ordinary substitution operation terminates; either we apply the substitution to a sub-expression or the objects we substitute are smaller. For an in-depth discussion, we refer the reader to Nanevski et al. [11].

\underline{28}

Meta substitution on normal terms / types

[[Ψ̂.M/u]]_{C[Ψ]}(Πx:A.B) = Πx:A′.B′ where [[Ψ̂.M/u]]_{C[Ψ]}(A) = A′
and [[Ψ̂.M/u]]_{C[Ψ]}(B) = B′
[[Ψ̂.M/u]]_{C[Ψ]}(Σx:A.B) = Σx:A′.B′ where [[Ψ̂.M/u]]_{C[Ψ]}(A) = A′
and [[Ψ̂.M/u]]_{C[Ψ} (B) = B′
[[Ψ̂.M/u]]_{C[Ψ]}(type)  = type
[[Ψ̂.M/u]]_{C[Ψ]}(λx.N) = λx.N′ where [[Ψ̂.M/u]]_{C[Ψ]}(N) = N′
[[Ψ̂.M/u]]_{C[Ψ]}(N_{1}, N_{2}) = (N′_{1}, N′_{2}) where [[Ψ̂.M/u]]_{C[Ψ]}(N_{2}) = N′_{2}

and [[Ψ̂.M/u]]_{C[Ψ]}(N_{2}) = N′_{2}

[[Ψ̂.M/u]]_{C[Ψ]}(R)  = N  where [[Ψ̂.M/u]]_{C[Ψ]}R = N : A
[[Ψ̂.M/u]]_{C[Ψ]}(R)  = R′  where [[Ψ̂.M/u]]_{C[Ψ]}R = R′
[[Ψ̂.M/x]]_{C[Ψ]}(N)  fails  otherwise

Meta substitution on neutral terms

[[Ψ̂.M/u]]_{A[Ψ]}(u[σ])  = M′ : A where [[Ψ̂.M/u]]_{C[Ψ]}(σ) = σ′
and [σ′]_{Ψ} (M) = M′
[[Ψ̂.M/u]]_{A[Ψ]}(v[σ])  = v[σ′]  where [[Ψ̂.M/u]]_{C[Ψ]}(σ) = σ′
[[Ψ̂.M/u]]_{C[Ψ]}(R N)  = R′N′  where [[Ψ̂.M/u]]_{C[Ψ]}(R) = R′

and [[Ψ̂.M/u]]_{C[Ψ]}(N) = N′

[[Ψ̂.M/u]]_{C[Ψ]}(R N)  = M′′ : B if [[Ψ̂.M/u]]_{C[Ψ]}(R) = λy.M′ : Πx:A.B

where Πx:A.B≤C, N′ = [[Ψ̂.M/u]]_{C[Ψ]}(N)

and M′′ = [N′/y]_{A}(M′)
[[Ψ̂.M/u]]_{C[Ψ]}(πR) = πR′ where [[Ψ̂.M/u]]_{C[Ψ]}(R) = R′
[[Ψ̂.M/u]]_{C[Ψ]}(fst R) = N_{1} : A {if [[Ψ̂.M/u]]_{C[Ψ]}(R) = (N_{1}, N_{2}) : Σx:A.B \atop where Σx:A.B ≤ C}
[[Ψ̂.M/u]]_{C[Ψ]}(snd R) = N_{2} : B {if [[Ψ̂.M/u]]_{C[Ψ]}(R) = (N_{1}, N_{2}) : Σx:A.B \atop where Σx:A.B ≤ C}
[[Ψ̂.M/u]]_{C[Ψ]}(x)  = x
[[Ψ̂.M/u]]_{C[Ψ]}(c)  = c
[[Ψ̂.M/u]]_{C[Ψ]}(a)  = a
[[Ψ̂.M/x]]_{C[Ψ]}(R) fails otherwise

Meta substitution on substitutions

[[Ψ̂.M/u]]_{C[Ψ]}(·)  = ·
[[Ψ̂.M/u]]_{C[Ψ]}(σ, M) = σ′, M′ where [[Ψ̂.M/u]]_{C[Ψ]}(σ) = σ′
and [[Ψ̂.M/u]]_{C[Ψ]}(M) = M′
[[Ψ̂.M/x]]_{C[Ψ]}(σ) fails otherwise

Meta substitution on contexts

[[Ψ̂.M/u]]_{C[Ψ]}(·)  = ·
[[Ψ̂.M/u]]_{C[Ψ]}(Ψ, x:A) = Ψ′, x:A′ where [[Ψ̂.M/u]]_{C[Ψ]}(Ψ) = Ψ′
and [[Ψ̂.M/u]]_{C[Ψ]}(A) = A′
[[Ψ̂.M/x]]_{C[Ψ]}(Ψ)  fails  otherwise

Fig. 6. Meta substitution DRAFT July 4, 2017—12 : 53