Higher-Order Unification, Polymorphism, and Subsorts (Extended Abstract)

Tobias Nipkow^{∗} University of Cambridge Computer Laboratory Pembroke Street Cambridge CB2 3QG England

                              Tobias.Nipkow@cl.cam.ac.uk

Abstract This paper analyzes the problems that arise in extending Huet’s higher-order unification algorithm from the simply typed λ-calculus to one with type variables. A simple, incomplete, but in practice very useful extension to Huet’s algorithm is discussed. This extension takes an abstract view of types. As a particular instance we explore a type system with ml-style polymorphism enriched with a notion of sorts. Sorts are partially ordered and classify types, thus giving rise to an order-sorted algebra of types. Type classes in the functional language Haskell can be understood as sorts in this sense. Sufficient conditions on the sort structure to ensure the existence of principal types are discussed. Finally we suggest a new type system for the λ-calculus which may pave the way to a complete unification algorithm for polymorphic terms.

1 Introduction

Huet’s algorithm for higher-order unification in the simply typed λ-calculus [11] forms the core of a number of theorem provers based on higher-order logic [1, 17, 14]. In this paper we discuss extensions to this unification algorithm which permit more expressive type systems: ml-style polymorphism enriched with a notion of sorts constraining type variables. It turns out that the step from the simply typed λ-calculus considered by Huet to one with type variables is nontrivial. The unification algorithm we analyze is in fact incomplete. A complete extension remains an open problem which is briefly considered at the end. On a more positive note, the introduction of sorts is completely orthogonal to the higher-order unification algorithm and causes no problems whatsoever.

It has to be stressed that this is not the first extension of Huet’s algorithm to a polymorphic type system. Nadathur [14] reports on an implementation of the programming language λProlog which features polymorphism. His extensions seem to be very similar to the ones analyzed in this paper. In particular he faces the same problem with completeness that we have. However, the author is not aware of a formal treatment of these issues, in particular not in connection with an order-sorted type system.

All the features described in this paper have recently been implemented in the generic theorem prover Isabelle. Isabelle is generic in the sense that it can be parameterized with the intended object-logic. Its meta-logic is a fragment of higher-order logic and its inference mechanism is based on higher-order unification. Detailed descriptions of the monomorphic version of Isabelle can be found in [18, 19]. Before we go into technical details, the motivation for the extensions to the type system in presented.

∗Research supported by ESPRIT BRA 3245, Logical Frameworks.

Although ml-style polymorphism hardly needs to be motivated in a programming language context, some simple examples from the realm of generic theorem provers seem appropriate. The basic reason for the introduction of polymorphism is the desire to shift type-checking in many-sorted logics from the object to the meta level. A typical example is the definition of an ordinary many-sorted first-order logic. We need to model a type of formulae form, and an unbounded number of different types of terms like natural numbers, reals, lists etc. In a polymorphic type system, the operation of equality between terms has type α → α → form where α is a type variable. The built-in type checker ensures that equality always compares terms of the same type.

In a monomorphic type system, we would have to declare a new equality =_{s} of type s → s → form for each new type of terms s, and give the same inference rules over and over again. This is clearly impractical. Alternatively, we can formalize types as part of the object-logic. In this case terms have to be decorated with their types, the type checking rules are part of the inference system and type checking is part of a proof. This is the approach taken in all logics defined in the monomorphic version of Isabelle. If a logic’s type system is sufficiently expressive to become undecidable, for example Intuitionistic Type Theory [12], this is in fact the only possible approach. For simpler systems, however, ml-polymorphism is clearly preferable.

Having adopted polymorphism, we need to tame its power. Initially one might be tempted to declare equality and universal quantification as follows:

\begin{matrix}=: & α → α → form \\ ∀ : & (α → form) → form \end{matrix}

The intention is that α ranges only over different types of terms, but certainly not over formulae or arbitrary function types (if the logic is supposed to be first-order). However, there is nothing in this declaration to enforce those constraints. As a consequence, some rather surprising inferences are possible. In first-order logic ∀-elimination is

\frac{∀x. P (x)}{P (t)}

where x : α, t : α, P : α → form and α are variables. Using the substitution {α ↦ form, t ↦ Q, P ↦ λx.x} we obtain the derived rule

\frac{∀x. x}{Q}.

In a first order-logic, ∀x. x is ill-formed. This formula could only arise because of the instantiation of α by form. In a higher-order logic, ∀x. x is in fact a valid formula, usually identified with falsity, and the rule expresses ex falso quodlibet.

In order to avoid such pitfalls, Isabelle’s types are classified by so called sorts. The sort of a type variable defines the subset of types the variable ranges over, thus prohibiting undesirable instantiations. Details are given in Section 4. Note that a similar mechanism for restricted polymorphism is embodied in ml’s equality types and, in a more general form, in Haskell’s type classes [24, 16].

After fixing the basic notation in Section 2, Section 3 presents the extension to Huet’s algorithm, taking an abstract view of types. Section 4 focuses on the type system, introducing polymorphism, sorts and subsorts. Finally, we speculate on a way to obtain a complete unification algorithm for the polymorphic case.

2 Preliminaries

The reader should be familiar with the basic notations and facts of equational logic as found for example in Dershowitz and Jouannaud [4]. We are broadly consistent with their notation, except that we treat substitutions as ordinary functions. Function composition is denoted by ∘: (f ∘ g)(x) = f(g(x)). The rest of this section presents the notation for the typed λ-calculus with α, β and η equality. For more details see [23, 10].

For the time being we take an abstract view of types with just enough detail to describe the unification process. Section 4 gives the full description of the intended type system. This separation is possible because the unification of terms and types proceeds largely independently.

The set T of all types is a subset of the free algebra over some set of type constructors, including the function-space constructor “→”, generated by a set of type variables V_{T}. The idea is that the types themselves form a sorted algebra and T is the set of all “well-sorted”, i.e. well-formed types. Types whose outermost constructor is “→” are called function types, all other types are called base types. The letters σ, τ and γ represent types. Function types associate to the right: σ → τ → γ means σ → (τ → γ). Instead of σ_{1} → ⋯ → σ_{n} → τ we write \overline{σ_{m}} → τ. The latter form is used only if τ is a base type. The type variables occurring in a type σ are denoted by V_{T} (σ).

T comes with a set of type substitutions S_{T} which is some subset of the set of all possible mappings from V_{T} to T and contains {}, the empty map. Again, the sorted nature of types has to be taken into account. Elements of S_{T} are denoted by Θ and Δ. The quasi-order ≤ on terms and substitutions is defined in the usual way. Correspondingly, there is a unification function U : T × T → 2^{S_{T}} which returns a complete set of unifiers: for any two σ, τ ∈ T and any Δ ∈ S_{T} with Δ(σ) = Δ(τ) there is a Θ ∈ U(σ, τ) such that Θ ≤ Δ [V_{T} (σ, τ)]. For simplicity we assume that all variables in the range of a substitution returned by U are “new”.

Terms are generated from a set of free variables V, a set of bound variables X, and a set of constants C by λ-abstraction and application. Free variables are denoted by F, G, and H, bound variables by x, y and z, and constants by a, b, and c. Terms are denoted by s, t, and u. The inductive definition of typed terms in a context Γ, which is just a mapping from X to T , is as follows:

\frac{Γ(x) = τ}{Γ ⊢ x : τ}  Γ ⊢ F^{τ} : τ  Γ ⊢ c^{τ} : τ

\frac{Γ ⊢ s : σ → τ Γ ⊢ t : σ}{Γ ⊢ (s t) : τ}  \frac{Γ ∘ \{x ↦ σ\} ⊢ s : τ}{Γ ⊢ (λx^{σ}.s) : σ → τ}

Note that free variables and constants on their own are not legal terms. They have to be tagged with some type, as in the second and third formation rule above. In particular we assume that all occurrences of a free variable in a term are decorated with the same type. There is no corresponding requirement for constants because they can be polymorphic. A term t is well-typed if {} ⊢ t : τ holds for some τ ∈ T . Instead of {} ⊢ t : τ we simply write t : τ. In the sequel we consider only well-typed terms, which means in particular that there are no “loose” bound variables: x, for example, is illegal. Instead of λx_{1}…. λx_{n}.s we write λx_{1}, …, x_{n}.s or just λ\overline{x_{n}}.s. Similarly we write t(u_{1}, …, u_{n}) or just t(\overline{u_{n}}) instead of (… (t u_{1}) …)u_{n}. The free variables in t are denoted by V(t), the type variables by V_{T} (t). Type decorations are omitted if they are not important.

We assume α, β and η conversion on terms. Relying on the strong normalization property of the typed λ-calculus we assume that terms are in β-normal form. We also ignore α conversion by working with α-equivalence classes of terms, using the generic bound variable names x and y. The η-expanded form [23] of the β-normal form of a term t is denoted by t↓.

A term λ\overline{x_{m}}.s(\overline{u_{k}}) in β-normal form is called rigid if s ∈ X ∪ C, and flexible if s ∈ V.

Substitutions on terms are defined as mappings from free variables to λ-terms in the usual way. They are denoted by θ and δ. Applying a type substitution to a term means applying it to all type decorations in the term.

A unifier of two terms s and t is a pair of substitutions ⟨Θ, θ⟩ on types and terms respectively such that θ(Θ(s)) and θ(Θ(t)) are equivalent modulo α, β and η-conversion.

3 Higher-Order Unification

The starting point for most work on higher-order unification is Huet’s algorithm [11] which enumerates a complete and minimal set of unifiers with respect to the simply typed λ-calculus [10]. As higher-order unification is undecidable in general [9], this is the best one can hope for. Snyder and Gallier [23] have recently reformulated Huet’s algorithm in terms of inference rules, which simplifies the presentation. Their version will be our reference point.

Isabelle was originally based on the simply typed λ-calculus and used Huet’s algorithm. A recent extension permits polymorphic constants in the ml sense. As a consequence, terms may now contain type variables as well as term variables, both of which may need to be instantiated during the unification process. This is a significant departure from the original problem.

Example 3.1 Let τ be some base type and α a type variable, let a : τ be a constant and G : α and F : α → τ be two variables. The following matching problem is given:

F (G) = a  (1)

Let us first look at (some of) the infinitely many solutions to this problem. We know that any instantiation of α must be of the form

τ_{1} → ⋯ → τ_{n} → γ

for suitable types τ_{1}, …, τ_{n} and γ. In particular we may assume that γ is not a function type. Without any assumptions about α we get the solution F = λx.a. In terms of Huet’s algorithm this is the solution obtained after a single imitation step. In fact, for any instantiation of α where γ ≠ τ, this is the only solution.

If we also assume that γ = τ, we get the following infinite set of solutions, indexed by n:

F = λx.x(A_{1}(x), …, A_{n}(x)), G = λx_{1}, …, x_{n}.a

The A_{i} are new free function variables.

Further instantiations of α yield yet more solutions. For example α = τ → τ alone has an infinite set of independent solutions:

F = λx.x^{k}(a), G = λx.x

is a solution for any natural number k, where x^{k} is the k-fold composition of x.

This shows quite drastically that type variables introduce a new degree of freedom into unification problems. Different type instantiations give rise to completely independent sets of solutions with greatly varying cardinality (finite vs. infinite). This is not in itself surprising, but it raises the question how this new freedom can be incorporated into the unification algorithm. We shall try to “lift” Huet’s algorithm to this new setting by replacing equality tests on types by unification. The following example shows why such a simple-minded extension is problematic. You need to be familiar with Huet’s algorithm to follow it.

Example 3.2 We return to the unification problem in Example 3.1. As mentioned above, a single imitation step finds the solution F = λx.a which requires no type instantiations. Projection, however, is different. F can be a projection only if the result type of its argument G is τ. This means that projection is applicable for any instance of α of the form τ_{1} → ⋯ → τ_{n} → τ. Unfortunately, the set of these types does not have a finite representation in terms of function types and type variables. Hence we can either try all possible type instantiations (which is complete but completely impractical) or sacrifice completeness for efficiency. In the latter case we pick the simplest type instantiation that permits projection. In this example it means unifying α and τ. This results in the instantiation of α by τ and the single additional solution

F = λx.x(A(x)), G = λx.a.

This is obviously incomplete. In particular, if (1) is just one in a set of equations to be solved simultaneously, some of the other equations may well require α to be instantiated by a different type. In that case we would find no solution unless we also backtrack over possible type instantiations.

Despite its incompleteness, the solution outlined in the above example has been adopted in both λProlog and Isabelle. In the sequel we present a formal treatment of this extension to Huet’s algorithm.

3.1 The Algorithm

This section formalizes the idea of “lifting” Huet’s algorithm. Our treatment is very close to that of Snyder and Gallier [23]. In fact, parts of our algorithm are identical to the one they present. The price we pay is the incompleteness discussed above.

The unification algorithm is presented as a collection of conditional rewrite rules on pairs ⟨Θ, D⟩, where Θ is a type substitution and D a multiset of unification problems s =^{?} t. D is called a system in the sequel. We assume that all occurrences of a free variable in D are decorated with the same type, a property that is preserved by the inference rules below. Note that Θ merely records and accumulates the type substitutions, whereas D represents both the current multiset of unification problems and the term substitutions obtained so far.

\frac{s : σ t : τ σ ≠ τ Δ ∈ U(σ, τ)}{⟨Θ, \{s =^{?} t\} ∪ D⟩ ⟹ ⟨Δ ∘ Θ, Δ(\{s =^{?} t\} ∪ D)⟩}  (T)

⟨Θ, {s =^{?} s} ∪ D⟩ ⟹ ⟨Θ, D⟩  (D)

\frac{t ∈ X ∪ C}{⟨Θ, \{λ\overline{x_{k}}.t(\overline{s_{n}}) =^{?} λ\overline{x_{l}}.F (\overline{u_{m}})\} ∪ D⟩ ⟹ ⟨Θ, \{λ\overline{x_{l}}.F (\overline{u_{m}}) =^{?} λ\overline{x_{k}}.t(\overline{s_{n}})\} ∪ D⟩}  (O)

\frac{F ∉ V(t) F ∈ V(D)}{⟨Θ, \{λ\overline{x_{k}}.F (\overline{x_{k}}) =^{?} t\} ∪ D⟩ ⟹ ⟨Θ, \{λ\overline{x_{k}}.F (\overline{x_{k}}) =^{?} t\} ∪ \{F ↦ t\}(D)⟩}  (V)

\frac{σ ≠ τ Δ ∈ U(σ, τ)}{\begin{matrix}⟨Θ, \{λ\overline{x_{k}}.c^{σ}(\overline{s_{m}}) =^{?} λ\overline{x_{l}}.c^{τ}(\overline{u_{n}})\} ∪ D⟩ ⟹ \\ ⟨Δ ∘ Θ, Δ(\{λ\overline{x_{k}}.c^{σ}(\overline{s_{m}}) =^{?} λ\overline{x_{l}}.c^{τ}(\overline{u_{n}})\} ∪ D)⟩ \end{matrix}}  (T_{S})

\frac{t ∈ X ∪ C}{\begin{matrix}⟨Θ, \{λ\overline{x_{k}}.t(\overline{s_{n}}) =^{?} λ\overline{x_{k}}.t(\overline{u_{n}})\} ∪ D⟩ ⟹ \\ ⟨Θ, \{λ\overline{x_{k}}.s_{i} =^{?} λ\overline{x_{k}}.u_{i} | i ∈ \{1, …, n\}\} ∪ D⟩ \end{matrix}}  (S)

\frac{σ = \overline{σ_{m+i}} → σ′ τ = \overline{τ_{n+j}} → σ′}{\begin{matrix}⟨Θ, \{λ\overline{x_{k}}.F^{σ}(\overline{s_{m}}) =^{?} λ\overline{x_{l}}.c^{τ}(\overline{u_{n}})\} ∪ D⟩ ⟹ \\ ⟨Θ, \{F =^{?} λ\overline{x_{m+i}}.c^{τ}(\overline{H_{n+j}(\overline{x_{m+i}})}), λ\overline{x_{k}}.F^{σ}(\overline{s_{m}}) =^{?} λ\overline{x_{l}}.c^{τ}(\overline{u_{n}})\} ∪ D⟩ \end{matrix}}  (I)

\frac{t ∈ X ∪ C σ = \overline{σ_{m+i}} → σ′ σ_{j} = \overline{τ_{p}} → τ σ′ ≠ τ Δ ∈ U(σ′, τ)}{\begin{matrix}⟨Θ, \{λ\overline{x_{k}}.F^{σ}(\overline{s_{m}}) =^{?} λ\overline{x_{l}}.t(\overline{u_{n}})\} ∪ D⟩ ⟹ \\ ⟨Δ ∘ Θ, Δ(\{λ\overline{x_{k}}.F^{σ}(\overline{s_{m}}) =^{?} λ\overline{x_{l}}.t(\overline{u_{n}})\} ∪ D)⟩ \end{matrix}}  (T_{P})

\frac{t ∈ X ∪ C σ = \overline{σ_{m+i}} → τ σ_{j} = \overline{τ_{p}} → τ}{\begin{matrix}⟨Θ, \{λ\overline{x_{k}}.F^{σ}(\overline{s_{m}}) =^{?} λ\overline{x_{l}}.t(\overline{u_{n}})\} ∪ D⟩ ⟹ \\ ⟨Θ, \{F^{σ} =^{?} λ\overline{x_{m+i}}.x_{j}(\overline{H_{p}(\overline{x_{m+i}})}), λ\overline{x_{k}}.F^{σ}(\overline{s_{m}}) =^{?} λ\overline{x_{l}}.t(\overline{u_{n}})\} ∪ D⟩ \end{matrix}}  (P)

The rules (T), (T_{S}), and (T_{P}) unify types and are new. Rule (O) orients rigid-flexible pairs. The remaining rules unify terms and are almost identical to the ones given by Snyder and Gallier. (T) unifies the types of two terms. (T_{S}) unifies the types of two rigid heads. (T_{P}) unifies the result type of a rigid term with the result type of one of its arguments. (T_{S}) and (T_{P}) may need to be applied before (S) and (P) respectively in order to make types meet. We assume that (I) and (P) are immediately followed by (V), eliminating F. The free variables H_{r} in (I) and (P) are assumed to be new.

Huet’s insight, which turned higher-order unification from a mere curiosity into computational reality, was that flexible-flexible pairs need not be solved. This simplifies the algorithm but requires some new terminology. The following definitions are broadly consistent with the literature.

A system D is in presolved form if for every unification problem s =^{?} t in D

• either s = λ\overline{x_{m}}.F (\overline{x_{m}}) and F occurs neither in t nor in the rest of D, or both s and t are flexible, and

• s and t have the same type.

If D is in presolved form, define

D⃗ = \{F ↦ t | (λ\overline{x_{k}}.F (\overline{x_{k}}) =^{?} t) ∈ D\}.

Like Gallier and Snyder [23] we define ≅ to be the least congruence on well-typed terms of the same type containing all flexible-flexible pairs. The pair ⟨Θ, θ⟩ is a preunifier of D if θ(Θ(s))↓ ≅ θ(Θ(t))↓ for all pairs s =^{?} t in D.

The next simple lemma shows that the terminology is consistent in that presolved forms give rise to preunifiers which in turn extend to unifiers. The precise statement requires some more notation. With every base type σ we associate some arbitrary but fixed free variable F_{σ}, and with every type τ = \overline{σ_{m}} → σ a term û_{τ} = λ\overline{x_{m}^{σ_{m}}}.F_{σ} where the x_{i} are all distinct.

Lemma 3.3 If D is in presolved form, ⟨{}, D⃗⟩ is a preunifier of D. If ⟨Θ, θ⟩ is a preunifier of D, then ⟨Θ, θ ∪ ξ⟩ is a unifier of D, where

ξ = {F ↦ û_{σ} | F^{σ} ∈ V(D) − dom(θ)}

The following soundness and completeness theorems can be proved along the same lines as their counterparts in [11, 23]:

Theorem 3.4 If ⟨Θ, D⟩ ⟹^{∗} ⟨Θ′, D′⟩ and D′ is in presolved form, then ⟨Θ′, D⃗′⟩ is a preunifier of D.

Theorem 3.5 Let ⟨Δ, δ⟩ be a unifier of a system D such that no type in the range of Δ is a function type. Then there exists a presolved form ⟨Θ, D′⟩ such that ⟨{}, D⟩ ⟹^{∗} ⟨Θ, D′⟩, Θ ≤ Δ [V_{T} (D)], D⃗′ ≤ δ [V(D)], and δ is a unifier of all flexible-flexible pairs in D′.

The completeness theorem is rather more conservative than the actual algorithm. In many practical cases it will find all solutions, although some of them require type variables to be instantiated by function types.

As with all unification algorithms expressed as rewrite rules on collections of unification problems, there are two kinds of nondeterminism during execution: the choice between different transformations that apply (“don’t know”) and between different unification problems they can be applied to (“don’t care”). Ideally, all strategies for selecting unification problems should be equivalent with respect to completeness. For example Huet [11] and Elliot [5] show this quite explicitly for their algorithms. This result also holds with respect to the limited completeness theorem above. However, our algorithm is in general not just incomplete but also sensitive to the selection of unification problems. The point is that (T_{P}) commits to a particular type instantiation out of an infinite set, thus reducing the solution space. Hence the application of (T_{P}) should be delayed as long as possible in order to minimize incompleteness. More precisely, one can give an operational characterization of completeness: the above set of transformation rules enumerates a complete set of unifiers for a particular unification problem if (T_{P}) need not be applied in such a way that either γ or τ are type variables. This means that no solutions are lost if the application of (T_{P}) to a particular unification problem can always be delayed until the types are sufficiently instantiated.

3.2 Optimizations

In this section we briefly consider some simple optimizations of the above rather high-level algorithm. First we look at issues connected with conversion of λ-terms. In the description above, we have abstracted from all three conversion rules by considering α-equivalence classes of η-expanded β-normal forms. Here are some remarks on how to minimize the work of obtaining these normal forms:

α If De Bruijn notation [3] is used, α-conversion can be ignored completely.

β The question here is mainly how much of the normal form to compute when. As we can see from the rules, full β-normal form is not required — head-normal form will do. If all terms are in β-normal form initially, only the application of (V) entails further normalization.

η In contrast to unification for the simply typed λ-calculus, our transformation rules do not leave terms in η-expanded form because type-variables may become instantiated. Fortunately, only (S) requires the η-expansion of the head, thus minimizing the need for η-expansion. In Isabelle we have gone so far as banning the instantiation of type variables by function types during the unification process, thus removing the need for η-expansion completely (provided the input is in η-expanded form). However, preliminary experiments suggest that in practice this is a rather drastic restriction, requiring frequent explicit type instantiations by the user.

Further important optimizations concern the order in which rules are applied. In contrast to (T_{P}), (T) and (T_{S}) should be performed as soon as possible, to detect nonunifiability by typeclashes. It is in fact sufficient to apply (T) to the input because the remaining rules maintain the invariant that the two terms of a unification problem have the same type. The rules for unification of terms, simplification (S), imitation (I), and projection (P), should be tried in the order embodied in Huet’s algorithm.

4 Polymorphism and Subsorts

This section fills in the details left open by the rather general discussion of types in Section 2. As indicated in that section and motivated in the introduction, type variables need to be constrained in order to capture certain restrictions, for example the first-order nature of some proof system. In Isabelle, type variables are constrained by introducing a third level into the system: so far we had terms, and types which qualify terms. Now we add sorts which qualify types. This is very reminiscent of generalized type systems [2], a relationship that needs further investigation. In contrast to generalized type systems we have a partial order on the sorts, indicating that a subclass of types identified by one sort is contained in the subclass identified by the another sort. This embodies the central ideas behind the notion of type classes in the functional language Haskell [24], a relationship that is made precise in [16]. Note that we are dealing with coercion on the level of sorts, not of types. Hence the system is quite different from OBJ [6], where we have a partial order between types^{1}.

The step from ml-style polymorphism to one with partially ordered sorts leads from a single-sorted to an order-sorted algebra of types. Therefore we need some basic vocabulary of order-sorted types. After that we look at order-sorted unification, which fulfills two functions in Isabelle: it is required for type checking [16] and for higher-order unification of polymorphic terms as described in Section 3.

The following definitions are consistent with [21, 22, 25]. Note that the naming conventions established in Section 2 do not all carry over. This is important to keep in mind since the order-sorted terms discussed below are the types in the λ-calculus discussed in Section 2.

An order-sorted signature consists of a set of sorts S, a partial order ≤ on S, and a set of function declarations f : (\overline{s_{n}})s. Given a fixed signature and an S-sorted set V = ⋃_{s∈S} V_{s} of disjoint sets of variables, a set of typed terms is defined inductively:

\frac{x ∈ V_{s} s ≤ s′}{x : s′}  \frac{f : (\overline{s_{n}})s s ≤ s′ ∀i. t_{i} : s_{i}}{f(\overline{t_{n}}) : s′}

The definitions of substitutions, unifiers, complete sets of unifiers etc. are straightforward generalizations of the unsorted case and can be found for example in [21]. In the sequel the ordering ≤ is extended from S to S^{∗} in the canonical componentwise way.

A signature is called regular [22] if every term has a least sort. Regularity is decidable for finite signatures:

Theorem 4.1 (Smolka et al. [22, 25]) A signature (S, ≤, Σ) is regular iff for every f ∈ Σ and w ∈ S^{∗} the set {s | ∃w′ ≥ w. f : (w′)s} either is empty or contains a least element.

Regularity is important because it implies that order-sorted unification is finitary. Order-sorted unification in non-regular signatures may be infinitary [22].

As in the section on higher-order unification, the algorithm is presented as a rewrite system on multisets of equations. The following rules are similar to those in Jouannaud and Kirchner’s survey [8]. With respect to some fixed signature define

1Which happen to be called sorts in OBJ, an unfortunate confusion.

s_{1} ∧ s_{2} = max{s | s ≤ s_{1} ∧ s ≤ s_{2}}
D(f, s) = max{w | ∃s′. f : (w)s′ ∧ s′ ≤ s}

If E = {x_{1} =^{?} t_{1}, …, x_{n} =^{?} t_{n}} such that all x_{i} are distinct and no x_{i} occurs in one of the t_{j}, E is in solved form and E⃗ = {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}} is a most general unifier of E.

{t =^{?} t} ∪ E ⟹ E

\{f(\overline{r_{n}}) =^{?} f(\overline{t_{n}})\} ∪ E ⟹ \{r_{1} =^{?} t_{1}, …, r_{n} =^{?} t_{n}\} ∪ E

\frac{t ∉ V}{\{t =^{?} x\} ∪ E ⟹ \{x =^{?} t\} ∪ E}

\frac{x ∈ V_{s} ∩ V(E) x ∉ V(t) t : s}{\{x =^{?} t\} ∪ E ⟹ \{x =^{?} t\} ∪ \{x ↦ t\}(E)}

\frac{x ∈ V_{s} y ∈ V_{s′} s < s′}{\{x =^{?} y\} ∪ E ⟹ \{y =^{?} x\} ∪ E}

\frac{x ∈ V_{s} y ∈ V_{s′} s ≰ s′ s′ ≰ s z ∈ V_{s′′} s′′ ∈ s ∧ s′ z ∉ \{x, y\} ∪ V(E)}{\{x =^{?} y\} ∪ E ⟹ \{x =^{?} z, y =^{?} z\} ∪ E}

\frac{x ∈ V_{s} n > 0 \overline{s_{n}} ∈ D(f, s) ∀i. x_{i} ∈ V_{s_{i}} ∧ x_{i} ∉ \{x\} ∪ V(t_{1}, …, t_{n}, E)}{\{x =^{?} f(\overline{t_{n}})\} ∪ E ⟹ \{x =^{?} f(\overline{x_{n}}), x_{1} =^{?} t_{1}, …, x_{n} =^{?} t_{n}\} ∪ E}

This algorithm is less deterministic but essentially equivalent to the ones given by Schmidt-Schauß [20] and Waldmann [25]. Adapting their results one can easily show:

Theorem 4.2 For any regular signature the set of all S⃗ such that E ⟹^{∗} S and S is in solved form is a complete set of unifiers for E.

It follows that in finite regular signatures, where s∧s′ and D(f, s) must be finite, finite complete sets of unifiers always exist.

The remainder of this section focuses on the existence of single most general unifiers. Since our terms represent types, this happens to coincide with the existence of principal types. A lack of principal types is undesirable for two reasons: expressions may have any finite number of incomparable types, making them rather hard to comprehend from a user’s point of view; finite sets of type unifiers increase the search space for higher-order unification.

Waldmann [25] characterizes unitary signatures, i.e. those leading to unitary unification problems^{2}. He calls a partial order (S, ≤) downward complete iff the set s ∧ s′ contains at most one element.

Theorem 4.3 (Waldmann [25]) A regular signature is unitary iff it is downward complete and for all s, w, and f : (w^{0})s^{0} such that w ≤ w^{0} and s ≤ s^{0} the set

W (f, w, s) = \{w′ | ∃\overline{w}, \overline{s}. f : (\overline{w})\overline{s} ∧ \overline{s} ≤ s ∧ w′ ≤ w ∧ w′ ≤ \overline{w}\}

either is empty or contains a greatest element.

2The characterization results by Meseguer et al. [13] do not immediately apply to our situation because they admit unsorted variables in their unification problems.

Unfortunately, the definition of the set W (f, w, s) is not very intuitive, difficult to check, and hence unsuitable as a guideline for users.

The programming language Haskell [7] solves this problem by imposing a number of severe context conditions which are sufficient to guarantee principal types. Although they are not necessary, they make a lot of sense from a programming language point of view. Their essence is captured in the next lemma, which follows easily from Lemma 4.5 below.

Lemma 4.4 A signature is unitary if it is finite, regular, downward complete,

• injective: f : (w)s and f(w′)s imply w = w′, and

• subsort reflecting: f : (w′)s′ and s′ ≤ s imply the existence of w such that w′ ≤ w and f : (w)s.

Isabelle uses a slightly weaker criterion called coregularity. A signature is coregular if for all f and s the set D(f, s) contains at most one element. The following lemma goes back to Schmidt-Schauß and is also given by Smolka et al. [22].

Lemma 4.5 Signatures which are finite, regular, downward complete, and coregular are unitary.

This lemma follows directly from the correctness of the unification algorithm above because downward completeness and coregularity eliminate all essential nondeterminism from that algorithm.

It is easy to see that injectivity and subsort reflection together imply coregularity but that coregularity implies neither. Nevertheless, the two criteria are equivalent in the following sense: given a coregular signature Σ, there exists an injective and subsort reflecting signature Σ′ on the same sort structure but with declarations

{f : (w)s | D_{Σ}(f, s) = {w}}

such that t : s holds w.r.t. Σ iff it holds w.r.t. Σ′. This means that the sorting judgements derivable w.r.t. Σ and Σ′ are identical. Hence Σ and Σ′ are interchangeable for all intents and purposes.

5 Speculation

The algorithm for higher-order unification in the presence of type variables presented in Section 3 is incomplete. The source of this incompleteness is our inability, given a type σ, to find a finite representation for the set of all types \overline{σ_{n}} → σ. We propose a radical extension to the type system which overcomes this limitation. We introduce a “pseudo”-product type ∗ and a unit-type 1 which are related to → as follows:

α ∗ β → γ = α → β → γ α → β ∗ γ = (α → β) ∗ (α → γ)
α ∗ 1 = α  1 ∗ α = α
1 → α = α  α → 1 = 1
(α ∗ β) ∗ γ = α ∗ (β ∗ γ)

Read from left to right, this is a terminating and confluent rewriting system. Normal forms are products of simple types. Notice that this system, together with commutativity of ∗, axiomatizes isomorphism in Cartesian Closed Categories. The unification problem for the latter and related systems, but not for the one above, has already been considered by Narendran et al. [15].

The point of this new type system is that the set of all types \overline{σ_{n}} → σ can be represented by α → σ, where α is a type variable. To obtain \overline{σ_{n}} → σ, simply instantiate α with σ_{1} ∗ ⋯ ∗ σ_{n}.

The new type constructors ∗ and 1 are accompanied by two new term constructors ⟨ , ⟩ and ⟨⟩ and a number of equalities between λ-terms containing pairs and units.

Whether this approach leads to a complete higher-order unification algorithm for polymorphic λ-terms over these new types is not clear yet, in particular since the unification problem for the types themselves is now highly nontrivial (it contains associative unification as a special case).

Acknowledgements

The author wishes to thank Larry Paulson and David Wolfram for many discussions on higherorder unification and polymorphism, Uwe Waldmann for his patient explanations of order-sorted unification, and Annette Schumann for proof reading.

References

[1] P.B. Andrews, D.A. Miller, E.L. Cohen, F. Pfenning. Automating Higher-Order Logic. In Automated Theorem Proving: After 25 Years, AMS Contemporary Mathematics Series 29 (1984), 169–192.

[2] H. Barendregt. Introduction to Generalised Type Systems. To appear in J. Functional Programming.

[3] N. G. de Bruijn. Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem. Indagationes Mathematicae 34 (1972), 381–392.

[4] N. Dershowitz, J.-P. Jouannaud. Rewrite Systems. In J. van Leeuwen (editor), Handbook of Theoretical Computer Science, Vol B: Formal Methods and Semantics, North-Holland, to appear.

[5] C. Elliot. Higher-Order Unification with Dependent Function Types. Proc. Rewriting Techniques and Applications, LNCS 355 (1989), 121–136.

[6] K. Futatsugi, J.A. Goguen, J.-P. Jouannaud, J. Meseguer. Principles of OBJ2. Proc. 12th ACM Symp. Principles of Programming Languages (1985), 52–66.

[7] P. Hudak, P. Wadler (Eds.). Report on the Programming Language Haskell. Version 1.0, April 1990.

[8] J.-P. Jouannaud, C. Kirchner. Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification. Technical report, March 1990.

[9] W. Goldfarb. The Undecidability of the Second-Order Unification Problem. Theoretical Computer Science 13 (1981), 225-230.

[10] J.R. Hindley, J.P. Seldin. Introduction to Combinators and λ-Calculus, Cambridge University Press (1986).

[11] G.P. Huet. A Unification Algorithm for Typed λ-Calculus. Theoretical Computer Science 1 (1975), 27–57.

[12] P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis (1984).

[13] J. Meseguer, J.A. Goguen, G. Smolka. Order-Sorted Unification. J. Symbolic Computation 8 (1989), 383–413.

[14] G. Nadathur. A Higher-Order Logic as the Basis for Logic Programming. PhD Thesis, University of Pennsylvania (1987).

[15] P. Narendran, F. Pfenning, R. Statman. On the Unification Problem for Cartesian Closed Categories. Ergo Report 89–082, School of Computer Science, Carnegie Mellon University, September 1989.

[16] T. Nipkow, G. Snelting. Type Classes and Overloading Resolution via Order-Sorted Unification. Tech. Rep. 200, University of Cambridge, Computer Laboratory, August 1990.

[17] L.C. Paulson. Natural Deduction as Higher-Order Resolution. J. Logic Programming 3 (1986), 237–258.

[18] L.C. Paulson. Isabelle: The Next 700 Theorem Provers. In P. Odifreddi (editor), Logic and Computer Science, Academic Press (1990), 361–385.

[19] L.C. Paulson, T. Nipkow: Isabelle Tutorial and User’s Manual, Tech. Rep. 189, University of Cambridge, Computer Laboratory, January 1990.

[20] M. Schmidt-Schauß. A Many-Sorted Calculus with Polymorphic Functions Based on Resolution and Paramodulation. Proc. 9th Int. Joint Conf. Artificial Intelligence (1985), 1162– 1168.

[21] M. Schmidt-Schauß. Computational Aspects of an Order-Sorted Logic with Term Declarations, LNCS 395 (1989).

[22] G. Smolka, W. Nutt, J.A. Goguen, J. Meseguer. Order-Sorted Equational Computation. In H. Aït-Kaci and M. Nivat (eds.), Resolution of Equations in Algebraic Structures Vol. 2, Academic Press (1989), 297–367.

[23] W. Snyder, J. Gallier. Higher-Order Unification Revisited: Complete Sets of Transformations. J. Symbolic Computation 8 (1989), 101–140.

[24] P. Wadler, S. Blott. How to Make ad-hoc Polymorphism Less ad hoc. Proc. 16th ACM Symp. Principles of Programming Languages (1989), 60–76.

[25] U. Waldmann: Unification in Order-Sorted Signatures. Forschungsbericht 298, Universität Dortmund, Fachbereich Informatik (1989).