Under consideration for publication in Math. Struct. in Comp. Science

Polarized Subtyping for Sized Types

A N D R E A S A B E L^{†}

Department of Computer Science, University of Munich Oettingenstr. 67, D-80538 München, Germany

abel@tcs.ifi.lmu.de

Received March 15, 2006

We present an algorithm for deciding polarized higher-order subtyping without bounded quantification. Constructors are identified not only modulo β, but also η. We give a direct proof of completeness, without constructing a model or establishing a strong normalization theorem. Inductive and coinductive types are enriched with a notion of size and the subtyping calculus is extended to account for the arising inclusions between the sized types.

1. Introduction

Polarized kinding and subtyping has recently received interest in two contexts. First, in the analysis of container types in object-oriented programming languages (Duggan and Compagnoni, 1999): If List A is a functional (meaning: read-only) collection of objects of type A and A is a subtype (subclass) of B then List A should be a subtype of List B. However, for read-write collections, as for instance Array, such a subtyping relation is unsound^{‡}, hence these two collection constructors must be kept apart. The conventional modeling language for object types, System F_{≤}^{ω}, does not distinguish List and Array in their kind—both map types to types, thus, have kind ∗ → ∗. To store subtyping properties in the kind of constructors, polarities were added by Cardelli, Pierce (unpublished), Steffen (1998), and Duggan and Compagnoni (1999). Now, the type constructor List gets kind ∗ →^{+} ∗, meaning that it is a monotone (or covariant) type-valued function, whereas Array gets kind ∗ →^{∘} ∗, meaning that Array is neither co- nor contravariant or its variance is unknown to the type system.

Another application of polarized kinding are normalizing languages^{§} with recursive datatypes. It is well-known that if a data type definition has a negative recursive occurrence, a looping term can be constructed by just using the constructors and destructors of this data type, without actually requiring recursion on the level of programs (Mendler, 1987). Negative occurrences can be excluded by polarized kinding (Abel and Matthes, 2004)—a recursive type μF is only admitted if F : ∗ →^{+} ∗.

A promising way to formulate a normalizing language is by using sized types. Hughes, Pareto,

† Research supported by the coordination action TYPES (510996) and thematic network Applied Semantics II (IST-2001-38957) of the European Union and the project Cover of the Swedish Foundation of Strategic Research (SSF). ‡ Nevertheless, such a subtyping rule has been added for arrays in Java. § In a normalizing language, each program is terminating.

and Sabry (1996) have presented such a language, which can be used, e. g., as a basis for embedded programming. It features sized first-order parametric data types, where the size parameter induces a natural subtyping relation. Independently, Barthe et. al. (2004) have arrived at a similar system, which is intended as the core of a theorem prover language. Both systems, however, fail to treat higher-order and heterogeneous (or nested) data types which have received growing interest in the functional programming community (Altenkirch and Reus, 1999; Bird and Paterson, 1999; Hinze, 2000; Okasaki, 1999; Abel et al., 2005).

In order to extend the sized type system to such higher-order constructions, we need to handle polarized higher-order subtyping! Steffen (1998) has already defined the necessary concepts and an algorithm that decides this kind of subtyping. But because he features also bounded quantification, his completeness proof for the algorithm is long and complicated. In this article, I present a different subtyping algorithm, without bounded quantification, but instead fitted to the needs of sized types, and prove it sound and complete in a rather straight-forward manner.

Main technical contribution. We define a polarized higher-order subtyping algorithm that respects not only β but also η-equality and computes the normal form of the considered type constructors incrementally. A novelty is the succinct and direct proof of completeness, which relies neither on a normalization theorem nor a model construction. Instead, a lexicographic induction on kinds and derivations is used.

Organization. In Section 2, we recapitulate the polarized version of F^{ω} defined in a previous paper (Abel and Matthes, 2004) and extend it by subkinding and polarized higher-order subtyping. A subtyping algorithm is presented in Section 3. In Section 4, we prove completeness of the algorithmic equality. The extension to sized types is presented in Section 5, and we close with a discussion of related work.

Preliminaries. The reader should be familiar with higher-order polymorphism and subtyping. Pierce (2002) provides an excellent introduction.

Judgements. In the following, we summarize the inductively defined judgements used in this article.

κ ≤ κ′  κ is a subkind of κ′
Γ ⊢ F : κ  constructor F has kind κ in context Γ
Γ ⊢ F = F′ : κ  F and F′ of kind κ are βη-equal
Γ ⊢ F ≤ F′ : κ  F is a higher-order subtype of F′
F ↘ W  F has weak head normal form W
Γ ⊢ N ≤^{q} N′ ⇉ κ algorithmic subtyping (inference mode)
Γ ⊢ W ≤^{q} W′ ⇇ κ algorithmic subtyping (checking mode)

When we write D :: J, we mean that judgement J has derivation D. Then, |D| denotes the height of this derivation. We consider derivations ordered by their height: D_{1} ≤ D_{2} iff |D_{1}| ≤ |D_{2}|.

2. Polarized System F^{ω}

In this section, we present a modification of F^{ω} where function kinds are decorated with polarities. This is essentially Fix^{ω} (Abel and Matthes, 2004) without fixed-points, but the additional polarity ⊤, subkinding and subtyping. A technical difference is that Fix^{ω} uses Church-style (kind-annotated) constructors whereas we use Curry-style (domain-free) constructors. However, all result of this paper apply also to the Church style.

p, q ∈ Pol  p ≤ q  pq
p, q ::= ∘  non-variant
| + covariant
| − contravariant
| ⊤ invariant

[figure: ⊤; +; −; ∘] \begin{aligned}& ∘ & + & − & ⊤ \\ ∘ & ∘ & ∘ & ∘ & ⊤ \\ + & ∘ & + & − & ⊤ \\ − & ∘ & − & + & ⊤ \\ ⊤ & ⊤ & ⊤ & ⊤ & ⊤ \end{aligned}

Fig. 1. Polarities: definition, ordering, composition.

2.1. Polarities

We aim to distinguish constructors with regard to their monotonicity or variance. For instance, the product constructor × is monotone or covariant in both of its arguments. If one enlarges the type A or B, more terms inhabit A×B. The opposite behavior is called antitone or contravariant. Two more scenarios are possible: the value F A does not change when we modify A. Then F is called constant or invariant. Finally, a function F might not exhibit a uniform behavior, it might grow or shrink with its argument, or we just do not know how F behaves. This is the general case, we call it mixed-variant. Each of the behaviors is called a polarity and abbreviated by one of the four symbols displayed in Fig. 1.

The polarities are related: Since mixed-variant means that we do not have any information about the function, and we can always disregard our knowledge about variance, each function is mixed-variant. The inclusion order between the four sets of in-, co-, contra-, and mixed-variant functions induces a partial information order ≤ on Pol. The smaller a set is, the more information it carries. Hence ∘ ≤ p, p ≤ ⊤, and p ≤ p for all p. This makes Pol a bounded 4-element lattice as visualized in Fig. 1.

Polarity of composed functions. Let F, G be two functions such that the composition F ∘ G is well-defined. If F has polarity p and G has polarity q, we denote the polarity of the composed function F ∘ G by pq. It is clear that polarity composition is monotone: if one gets more information about F or G, certainly one cannot have less information about F ∘ G. Then, if one of the functions is constant, so is their composition. Otherwise, if one of them is mixed-variant, the same holds for the composition. In the remaining cases, the composition is covariant if F and G have the same variance, otherwise it is contravariant. This yields the multiplication table in Fig. 1. Polarity composition, as function composition, is associative. It is even commutative, but not a priori, since function composition is not commutative.

Inverse application of polarities. If f(y) = py is the function which composes a polarity with p, what would be its inverse g(x) = p^{−1}x? It is possible to define g in such a way that f and g form a Galois connection, i.e.,

p^{−1}x ≤ y ⟺ x ≤ py.

It is not hard to see that the unique solution is given by the equations: +^{−1}x = x, −^{−1}x = −x, ⊤^{−1}x = ∘, ∘^{−1}∘ = ∘ and ∘^{−1}x′ = ⊤ (for x′ ≠ ∘). As for every Galois connection, it holds that p^{−1}py ≤ y and x ≤ pp^{−1}x, and both f and g are monotone.

2.2. Kinds

Constructors are classified by their kind, i. e., as types, functions on types, functions on such functions etc.

Kind ∋ κ ::= ∗  types
| pκ_{1} → κ_{2}  p-variant constructor transformers

A constructor of kind pκ_{1} → κ_{2} is a p-variant function which maps constructors of kind κ_{1} to constructors of kind κ_{2}. Sometimes it is written as κ_{1} →^{p} κ_{2}. Let p⃗κ⃗ → κ′ be an abbreviation for p_{1}κ_{1} → ⋯ → p_{n}κ_{n} → κ′ where we presuppose |p⃗| = |κ⃗| = n. It is clear that every kind can be written as p⃗κ⃗ → ∗ with potentially empty vectors p⃗ and κ⃗. The rank of a kind is defined recursively as rk(p⃗κ⃗ → ∗) = max{1 + rk(κ_{i}) | 1 ≤ i ≤ |κ⃗|} (where the maximum of an empty set is 0).

Subkinding. The order on polarities induces an order κ ≤ κ′ on kinds. We say that κ is a subkind of κ′ or κ′ is a superkind of κ. As usual, this shall mean that each constructor of kind κ is also of kind κ′. The subkinding relation is given inductively by the following rules:

\overline{∗ ≤ ∗}  \overline{ord ≤ ord}  \frac{p′ ≤ p  κ′_{1} ≤ κ_{1}  κ_{2} ≤ κ′_{2}}{pκ_{1} → κ_{2} ≤ p′κ′_{1} → κ′_{2}}

Subkinding is reflexive, transitive, and antisymmetric; hence, a proper partial order.

Lemma 2.1 (Inversion of subkinding). Related kinds have the same shape: 1 If p⃗κ⃗ → κ_{0} ≤ κ′ then there are p′, κ′, κ′_{0} with κ′ = p′κ′ → κ′_{0} and |p′| = |κ′| = |p⃗| = |κ⃗| =:

n such that κ_{0} ≤ κ′_{0} and both p′_{i} ≤ p_{i} and κ′_{i} ≤ κ_{i} for all 1 ≤ i ≤ n. 2 The last sentence remains true when we trade ≤ for ≥.

2.3. Constructors

Constructors are given by the following Curry-style type-level lambda-calculus with some constants. The meta-variable X ranges over a countably infinite set of constructor variables and C over a fixed set of constructor constants.

Constr ∋ A, B, F, G, H, I, J ::= C | X | λXF | F G

As usual, λXF binds variable X in F. We identify constructors under α-equivalence, i. e., under renaming of bound variables. FV(F) shall denote the set of free variables of constructor F.

Signature. The constructor constants C are taken from a fixed signature Σ which contains at least the following constants together with their kinding:

→ : ∗ →^{−} ∗ →^{+} ∗  function space,
for each κ: ∀_{κ} : (κ →^{∘} ∗) →^{+} ∗  quantification.

2.4. Kinding

In this section, we present rules of kinding, i. e., assigning kinds to constructors. The rules extend the kinding rules of F^{ω} by the treatment of polarities.

Polarized contexts. A polarized context Γ fixes a polarity p and a kind κ for each free variable X of a constructor F. If p = +, then X may only appear positively in F; this ensures that λXF is an monotone function. Similarly, if p = −, then X may only occur negatively, and if p = ∘, then X may appear in both positive and negative positions. A variable labeled with ⊤ may only appear in arguments of an invariant function.

PCxt ∋ Γ ::= ⋄  empty context
| Γ, X:pκ extended context (X ∉ dom(Γ))

The domain dom(Γ) is the set of constructor variables Γ mentions. As usual, each variable can appear in the context only once. The order of hypotheses X : pκ in the context does not matter, so we may silently reorder them.

Ordering on contexts. We say context Γ′ is more liberal than context Γ, written Γ′ ≤ Γ, iff for all variables X,

(X:pκ) ∈ Γ implies (X:p′κ′) ∈ Γ′ for some p′ ≤ p and κ′ ≤ κ.

In particular, Γ′ may declare more variables than Γ and assign weaker polarities to them. The intuition is that all constructors which are well-kinded in Γ are also well-kinded in a more permissive context Γ′.

Application of polarities to contexts. The application pΓ of a polarity p to a context Γ is defined as pointwise application, i. e., if (X: qκ) ∈ Γ, then (X: (pq)κ) ∈ pΓ. Inverse application p^{−1}Γ is defined analogously. Together, they form a Galois connection, i. e., for all Γ and Γ′,

p^{−1}Γ ≤ Γ′ ⟺ Γ ≤ pΓ′.

Lemma 2.2. If Γ_{1} ≤ Γ_{2} and q_{1} ≤ q_{2} then q_{1}Γ_{1} ≤ q_{2}Γ_{2} and q_{2}^{−1}Γ_{1} ≤ q_{1}^{−1}Γ_{2}.

Lemma 2.3 (Some simplification laws). p(qΓ) = (pq)Γ, p^{−1}(qΓ) = (p^{−1}q)Γ, +^{−1}Γ = +Γ = Γ, −^{−1}Γ = −Γ, −−Γ = Γ.

Kinding. We will introduce a judgement Γ ⊢ F : κ which combines the usual notions of wellkindedness and positive and negative occurrences of type variables. A candidate for the application rule is

\frac{Γ ⊢ F : pκ → κ′ Γ′ ⊢ G : κ}{Γ ⊢ F G : κ′} Γ ≤ pΓ′.

The side condition is motivated by polarity composition. Consider the case that X ∉ FV(F). If G is viewed as a function of X, then F G is the composition of F and G. Now if G is q-variant in X, then F G is pq-variant in X. This means that all q-variant variables of Γ′ must appear in Γ with a polarity of at most pq. Now if X ∈ FV(F), it could be that it is actually declared in Γ with a polarity smaller than pq. Also, variables which are not free in G are not affected by the application F G, hence they can carry the same polarity in F G as in F. Together this motivates the condition Γ ≤ pΓ′.

Since p^{−1}Γ is the most liberal context which satisfies the side condition, we can safely replace Γ′ by p^{−1}Γ in the above rule. Hence, we arrive at the following formulation of the kinding rules:

kind-c \frac{C:κ ∈ Σ}{Γ ⊢ C : κ}  kind-var \frac{X:pκ ∈ Γ  p ≤ +}{Γ ⊢ X : κ}

kind-λ \frac{Γ, X:pκ ⊢ F : κ′}{Γ ⊢ λXF : pκ → κ′}  kind-app \frac{Γ ⊢ F : pκ → κ′  p^{−1}Γ ⊢ G : κ}{Γ ⊢ F G : κ′}

kind-sub \frac{Γ ⊢ F : κ  κ ≤ κ′}{Γ ⊢ F : κ′}

Although these rules are not fully deterministic, they can easily be turned into a bidirectional kind checking algorithm for constructors in β-normal form (see, e. g., Davies and Pfenning (2000)).

Example 2.4 (Derived rules for function space and quantification). The following rules are derivable:

\frac{−Γ ⊢ A : ∗  Γ ⊢ B : ∗}{Γ ⊢ A → B : ∗}  \frac{Γ, X:∘κ ⊢ A : ∗}{Γ ⊢ ∀_{κ}λXA : ∗}

Lemma 2.5 (Admissible rules for kinding). 1 Weakening: If D :: Γ ⊢ F : κ and both Γ′ ≤ Γ and κ ≤ κ′, then D′ :: Γ′ ⊢ F : κ′ for some

D′ ≤ D. 2 Strengthening: If D :: Γ, X: pκ ⊢ F : κ′ and X ∉ FV(F), then D′ :: Γ ⊢ F : κ′ for some

D′ ≤ D. 3 Substitution: If D :: Γ, X:pκ ⊢ F : κ′ and p^{−1}Γ ⊢ G : κ, then Γ ⊢ [G/X]F : κ′.

Proof. Each by induction on D.

Lemma 2.6 (Inversion of kinding). 1 If D :: Γ ⊢ C : κ′ then (C:κ) ∈ Σ for some κ ≤ κ′. 2 If D :: Γ ⊢ X : κ′ then (X:pκ) ∈ Γ for some p ≤ +, κ ≤ κ′. 3 If D :: Γ ⊢ λXF : κ′ then κ′ = pκ_{1} → κ_{2} for some p, κ_{1}, κ_{2} and D′ :: Γ, X:pκ_{1} ⊢ F : κ_{2}

for some D′ < D. 4 If D :: Γ ⊢ F G : κ′ then D_{1} :: Γ ⊢ F : pκ → κ′ and D_{2} :: p^{−1}Γ ⊢ G : κ for some p, κ,

and D_{1}, D_{2} < D.

Proof. Each by induction on D. For example, 3: If the last rule in D was kind-λ , we are done, otherwise, the last rule must have been kind-sub :

\frac{Γ ⊢ λXF : κ κ ≤ κ′}{Γ ⊢ λXF : κ′}

By induction hypothesis, κ = pκ_{1} → κ_{2} and Γ, X: pκ_{1} ⊢ F : κ_{2}. By inversion on subkinding, κ′ = p′κ′_{1} → κ′_{2} with p′ ≤ p, κ′_{1} ≤ κ_{1}, and κ_{2} ≤ κ′_{2}. This entails that the context (Γ, X: p′κ′_{1}) is more liberal than (Γ, X : pκ_{1}), hence, we can apply the weakening lemma to obtain Γ, X : p′κ′_{1} ⊢ F : κ′_{2}.

2.5. Equality

In contrast to most presentations of System F^{ω}, we consider constructors equivalent modulo β and η.

Axioms.

eq-β \frac{Γ, X:pκ ⊢ F : κ′  p^{−1}Γ ⊢ G : κ}{Γ ⊢ (λXF) G = [G/X]F : κ′}

eq-η \frac{Γ ⊢ F : pκ → κ′}{Γ ⊢ (λX. F X) = F : pκ → κ′} X ∉ FV(F)

eq-⊤ \frac{Γ ⊢ F : ⊤κ → κ′  ⊤^{−1}Γ ⊢ G : κ  ⊤^{−1}Γ ⊢ G′ : κ}{Γ ⊢ F G = F G′ : κ′}

Rule eq-⊤ expresses that the value of an invariant function does not depend on its argument. Only well-kindedness of the argument is required, in order to ensure the validity property (Lemma 2.7.1).

Congruence rules and subsumption.

eq-c \frac{C:κ ∈ Σ}{Γ ⊢ C = C : κ}  eq-var \frac{X:pκ ∈ Γ  p ≤ +}{Γ ⊢ X = X : κ}

eq-λ \frac{Γ, X:pκ ⊢ F = F′ : κ′}{Γ ⊢ λXF = λXF′ : pκ → κ′}  eq-app \frac{Γ ⊢ F = F′ : pκ → κ′  p^{−1}Γ ⊢ G = G′ : κ}{Γ ⊢ F G = F′ G′ : κ′}

eq-sub \frac{Γ ⊢ F = F′ : κ  κ ≤ κ′}{Γ ⊢ F = F′ : κ′}

Symmetry and transitivity.

eq-sym \frac{Γ ⊢ F = F′ : κ}{Γ ⊢ F′ = F : κ}  eq-trans \frac{Γ ⊢ F_{1} = F_{2} : κ  Γ ⊢ F_{2} = F_{3} : κ}{Γ ⊢ F_{1} = F_{3} : κ}

2.6. Subtyping

In this section, we specify subtyping for constructors of polarized kinds. The rules are inspired by Steffen (1998).

Reflexivity, transitivity and antisymmetry. These three properties make subtyping a partial order on constructors of the same kind.

leq-refl \frac{Γ ⊢ F = F′ : κ}{Γ ⊢ F ≤ F′ : κ}  leq-trans \frac{Γ ⊢ F_{1} ≤ F_{2} : κ  Γ ⊢ F_{2} ≤ F_{3} : κ}{Γ ⊢ F_{1} ≤ F_{3} : κ}

leq-antisym \frac{Γ ⊢ F ≤ F′ : κ  Γ ⊢ F′ ≤ F : κ}{Γ ⊢ F = F′ : κ}

The reflexivity rule leq-refl includes the subtyping axioms for variables and constants as special cases. Reflexivity and transitivity together ensure that subtyping is compatible with equality. The antisymmetry rule leq-antisym potentially enlarges our notion of equality.

Abstraction.

leq-λ \frac{Γ, X:pκ ⊢ F ≤ F′ : κ′}{Γ ⊢ λXF ≤ λXF′ : pκ → κ′}

Application. There are two kinds of congruence rules for application: one kind states that if functions F and F′ are in the subtyping relation, so are their values F G and F′ G at a certain argument G.

leq-fun \frac{Γ ⊢ F ≤ F′ : pκ → κ′  p^{−1}Γ ⊢ G : κ}{Γ ⊢ F G ≤ F′ G : κ′}

The other kind of rules concern the opposite case: If F is a function and two arguments G and G′ are in a subtyping relation, so are the values F G and F G′ of the function at these arguments. However, such a relation can only exist if F is covariant or contravariant.

leq-arg+ \frac{Γ ⊢ F : +κ → κ′  Γ ⊢ G ≤ G′ : κ}{Γ ⊢ F G ≤ F G′ : κ′}

leq-arg− \frac{Γ ⊢ F : −κ → κ′  −Γ ⊢ G′ ≤ G : κ}{Γ ⊢ F G ≤ F G′ : κ′}

Note that we only included a subsumption rule for equality (eq-sub ), not for subtyping. Subsumption for subtyping is admissible, as item 2 of the following lemma states:

Lemma 2.7 (Admissible rules for equality and subtyping I). Let R ∈ {=, ≤}. 1 Validity: If D :: Γ ⊢ F R F′ : κ then Γ ⊢ F : κ and Γ ⊢ F′ : κ. 2 Weakening: If D :: Γ ⊢ F R F′ : κ and both Γ′ ≤ Γ and κ ≤ κ′, then Γ′ ⊢ F R F′ : κ′. 3 Strengthening: If D :: Γ, X:pκ ⊢ F R F′ : κ′ and X ∉ FV(F, F′), then Γ ⊢ F R F′ : κ′.

Proof. Each by induction on D.

Lemma 2.8 (Admissible rules for equality and subtyping II). See Fig. 2.

3. Algorithmic Polarized Subtyping

In this section, we present an algorithm for deciding whether two well-kinded constructors are equal or related by subtyping. The algorithm is an adaption of Coquand’s βη-equality test (Coquand, 1991) to the needs of subtyping and polarities. The idea is to first weak-head normalize

eq-refl \frac{Γ ⊢ F : κ}{Γ ⊢ F = F : κ}
leq-app∘ \frac{Γ ⊢ F ≤ F′ : ∘κ → κ′  ∘^{−1}Γ ⊢ G = G′ : κ}{Γ ⊢ F G ≤ F′ G′ : κ′}

leq-app+ \frac{Γ ⊢ F ≤ F′ : +κ → κ′  Γ ⊢ G ≤ G′ : κ}{Γ ⊢ F G ≤ F′ G′ : κ′}

leq-app− \frac{Γ ⊢ F ≤ F′ : −κ → κ′  −Γ ⊢ G′ ≤ G : κ}{Γ ⊢ F G ≤ F′ G′ : κ′}

leq-app⊤ \frac{Γ ⊢ F ≤ F′ : ⊤κ → κ′  ⊤^{−1}Γ ⊢ G : κ  ⊤^{−1}Γ ⊢ G′ : κ}{Γ ⊢ F G ≤ F′ G′ : κ′}

eq-app-⊤ \frac{Γ ⊢ F = F′ : ⊤κ → κ′  ⊤^{−1}Γ ⊢ G : κ  ⊤^{−1}Γ ⊢ G′ : κ}{Γ ⊢ F G = F′ G′ : κ′}

Fig. 2. Admissible rules for equality and subtyping.

the constructors under consideration and then compare their head symbols. If they are related, one continues to recursively compare the subcomponents, otherwise subtyping fails.

Weak head normal forms W ∈ Val are given by the grammar:

Ne ∋ N  ::= C | X | N G neutral constructors
Val ∋ V, W ::= N | λXF  weak head values

Weak head evaluation F ↘ W, a big-step call-by-name operational semantics, is defined inductively by the following rules:

eval-c \overline{C ↘ C}  eval-var \overline{X ↘ X}  eval-lam \overline{λXF ↘ λXF}

eval-app-ne \frac{F ↘ N}{F G ↘ N G}  eval-app-β \frac{F ↘ λXF′  [G/X]F′ ↘ W}{F G ↘ W}

Lemma 3.1 (Properties of weak head evaluation).

1 If F X ↘ W then either F ↘ λXF′ and F′ ↘ W, or F ↘ N and W = N X. If

X ∉ FV(F) then X ∉ FV(N). 2 If F ↘ W and [G/X]W ↘ V then [G/X]F ↘ V. 3 If F ↘ W and W G ↘ V then F G ↘ V.

Lemma 3.2 (Soundness of weak head evaluation). If Γ ⊢ F : κ and F ↘ W then Γ ⊢ F = W : κ.

Proof. By induction on F ↘ W. The interesting case is:

eval-app-β \frac{F ↘ λXF′  [G/X]F′ ↘ W}{F G ↘ W}
Γ ⊢ F G : κ′  by assumption
Γ ⊢ F : pκ → κ′  and
p^{−1}Γ ⊢ G : κ  by inversion
Γ ⊢ F = λXF′ : pκ → κ′  by induction hypothesis
Γ ⊢ λXF′ : pκ → κ′  by validity
Γ, X:pκ ⊢ F′ : κ′  by inversion
Γ ⊢ (λXF′) G = [G/X]F′ : κ′  by rule eq-β
Γ ⊢ [G/X]F′ : κ′  by substitution
Γ ⊢ [G/X]F′ = W : κ′  by induction hypothesis
p^{−1}Γ ⊢ G = G : κ  by reflexivity
Γ ⊢ F G = (λXF′) G : κ′  by rule eq-app
Γ ⊢ F G = W : κ′  by rule eq-trans

Corollary 3.3 (Subject reduction). If Γ ⊢ F : κ and F ↘ W then Γ ⊢ W : κ.

Proof. From the lemma by validity (Lemma 2.7.1).

We are ready to define the subtyping algorithm. Note that at any point during subtyping checking we may require kinding information. For example, consider checking X G ≤ X G′. If X is covariant, we need to continue with G ≤ G′, but if X is contravariant, the next step would be checking G′ ≤ G. Hence, the algorithm needs both context Γ and kind κ of the two considered constructors as additional input. Although the subtyping algorithm is kinded, it is not kind-directed as, for instance, Harper and Pfenning’s (2005) algorithmic equality for the logical framework LF.

The general form of the algorithmic subtyping judgement is defined by

Γ ⊢ F ≤^{q} F′ ⇇ κ :⟺ q = ⊤
or F ↘ W and F′ ↘ W′ and Γ ⊢ W ≤^{q} W′ ⇇ κ,

where Γ ⊢ W ≤^{q} W′ ⇇ κ is a judgement defined inductively in Fig. 3. The polarity q codes the relation that we seek to establish between F and F′: If q = ∘, we expect them to be equal, if q = +, we expect F ≤ F′, and if q = −, then the other way round. Finally if q = ⊤, then F and F′ need not be related, and the algorithm succeeds immediately.

The judgements for algorithmic subtyping Γ ⊢ N ≤^{q} N′ ⇉ κ for neutral constructors and Γ ⊢ W ≤^{q} W′ ⇇ κ for weak head values are defined inductively by the rules in Fig. 3. They are deterministic and can be directly implemented as an algorithm (apply the rules backwards). Both judgements take the context Γ, the polarity q, and the two constructors as input. Judgement Γ ⊢ N ≤^{q} N′ ⇉ κ produces kind κ if it succeeds, whereas the judgement Γ ⊢ F ≤^{q} F′ ⇇ κ

al-c \frac{(C:κ) ∈ Σ}{Γ ⊢ C ≤^{q} C ⇉ κ}  al-var \frac{(X:pκ) ∈ Γ  p ≤ +}{Γ ⊢ X ≤^{q} X ⇉ κ}

al-app-ne \frac{Γ ⊢ N ≤^{q} N′ ⇉ pκ → κ′  p^{−1}Γ ⊢ G ≤^{pq} G′ ⇇ κ}{Γ ⊢ N G ≤^{q} N′ G′ ⇉ κ′}

al-ne \frac{Γ ⊢ N ≤^{q} N′ ⇉ κ′}{Γ ⊢ N ≤^{q} N′ ⇇ κ}

al-λ \frac{Γ, X:pκ ⊢ F ≤^{q} F′ ⇇ κ′}{Γ ⊢ λXF ≤^{q} λXF′ ⇇ pκ → κ′}

For X ∉ FV(N) : al-η-l \frac{Γ, X:pκ ⊢ F ≤^{q} N X : κ′}{Γ ⊢ λXF ≤^{q} N : pκ → κ′} al-η-r \frac{Γ, X:pκ ⊢ N X ≤^{q} F : κ′}{Γ ⊢ N ≤^{q} λXF : pκ → κ′}

Fig. 3. Algorithmic subtyping and equality.

takes κ as an additional input and either succeeds or fails. The direction of the double arrow indicates the flow of the kinding information out of (⇇) or into (⇉) κ.

Note that due to rule al-ne , algorithmic subtyping does not guarantee that the involved constructors have the ascribed kind. For example, X : +∗ ⊢ X ≤^{∘} X ⇇ −∗ → ∗ is a valid derivation. It does not even entail that the involved constructors are well-kinded at all. For example:

Y :+(∗ →^{+} ∗), X:+(∗ →^{∘} ∗) ⊢ Y X ≤^{∘} Y X ⇉ ∗

Consequently, algorithmic subtyping is only sound for well-kinded constructors:

Theorem 3.4 (Soundness of algorithmic subtyping). Let Γ ⊢ N, N′, W, W′ : κ. 1 If D :: Γ ⊢ N ≤^{∘} N′ ⇉ κ′ then Γ ⊢ N = N′ : κ′ and κ′ ≤ κ. 2 If D :: Γ ⊢ N ≤^{+} N′ ⇉ κ′ then Γ ⊢ N ≤ N′ : κ′ and κ′ ≤ κ. 3 If D :: Γ ⊢ N ≤^{−} N′ ⇉ κ′ then Γ ⊢ N′ ≤ N : κ′ and κ′ ≤ κ. 4 If D :: Γ ⊢ W ≤^{∘} W′ ⇇ κ then Γ ⊢ W = W′ : κ. 5 If D :: Γ ⊢ W ≤^{+} W′ ⇇ κ then Γ ⊢ W ≤ W′ : κ. 6 If D :: Γ ⊢ W ≤^{−} W′ ⇇ κ then Γ ⊢ W′ ≤ W : κ.

Corollary 3.5. The soundness results hold also in the general form Γ ⊢ F ≤^{q} F′ ⇇ κ for well-kinded F, F′.

Proof of the corollary. For example, assume F ↘ W, F′ ↘ W′, and Γ ⊢ W ≤^{+} W′ ⇇ κ. By the theorem Γ ⊢ W ≤ W′ : κ, and by soundness of weak head evaluation, Γ ⊢ F = W : κ and similarly for F′, W′. Since subtyping is compatible with equality, we get Γ ⊢ F ≤ F′ : κ (to see this, use rules leq-refl and leq-trans ).

Proof of the soundness theorem. Simultaneously, by induction on D and by inversion on the typing derivations. We pick some representative cases:

Case

al-app-ne \frac{Γ ⊢ N ≤^{+} N′ ⇉ p′κ′_{1} → κ′_{2}  p^{′−1}Γ ⊢ G ≤^{p′} G′ ⇇ κ′_{1}}{Γ ⊢ N G ≤^{+} N′ G′ ⇉ κ′_{2}}
Γ ⊢ N G, N′ G′ : κ_{2}  by assumption
Γ ⊢ N, N′ : pκ_{1} → κ_{2}  by inversion
p^{−1}Γ ⊢ G, G′ : κ_{1}  by inversion
Γ ⊢ N ≤ N′ : p′κ′_{1} → κ′_{2}  by induction hypothesis
p′κ′_{1} → κ′_{2} ≤ pκ_{1} → κ_{2}  by induction hypothesis
p ≤ p′, κ_{1} ≤ κ′_{1}, κ′_{2} ≤ κ_{2}  by inversion
p^{′−1}Γ ≤ p^{−1}Γ  by Lemma 2.2
p^{′−1}Γ ⊢ G, G′ : κ′_{1}  by weakening (Lemma 2.5)

If p′ = ⊤, we are immediately done by leq-app⊤ (Lemma 2.8). Otherwise, obtain the induction hypothesis for G, G′ and apply leq-app p.

Case

al-ne \frac{Γ ⊢ N ≤^{−} N′ ⇉ κ′}{Γ ⊢ N ≤^{−} N′ ⇇ κ}

By induction hypothesis Γ ⊢ N′ ≤ N : κ′ and κ′ ≤ κ. Hence, by weakening, Γ ⊢ N′ ≤ N : κ.

Case

al-η-l \frac{Γ, X:pκ ⊢ F ≤^{∘} N X ⇇ κ′}{Γ ⊢ λXF ≤^{∘} N ⇇ pκ → κ′} X ∉ FV(N)

By induction hypothesis, Γ, X : pκ ⊢ F = N X : κ′, which gives by validity Γ, X : pκ ⊢ N X : κ′. Since X ∉ FV(N), we can infer by inversion and strengthening that Γ ⊢ N : pκ → κ′. Rule eq-η entails Γ ⊢ λX. N X = N : pκ → κ′. From the induction hypothesis we also get Γ ⊢ λXF = λX. N X : pκ → κ′ (rule leq-λ ), hence the goal Γ ⊢ λXF = N : pκ → κ′ follows by transitivity.

4. Completeness

While soundness of the algorithmic subtyping/equality is easy to show, the opposite direction, completeness, is usually hard and requires either the construction of a model (Compagnoni and Goguen, 2003; Harper and Pfenning, 2005) or strong normalization for constructors (Pierce and Steffen, 1997; Steffen, 1998; Goguen, 2005). We will require neither.

Algorithmic subtyping is cut-free in a twofold sense: First, a rule for transitivity is missing (this is the cut on the level of subtyping). Its admissibility can often be shown directly by induction on the derivations (Pierce and Steffen, 1997; Compagnoni and Goguen, 2003)—so also in our case. The second kind of cut is on the level of kinds: Kinds can be viewed as propositions in minimal logic and constructors as their proof terms, and an application which introduces a redex is a cut in natural deduction. Algorithmic subtyping lacks a general rule for application; its admissibility corresponds to the property of normalization or cut admissibility, resp. We manage to show the admissibility of application directly by a lexicographic induction of the kind of the argument part and the derivation length of the function part. This way, we save ourselves considerable work, and completeness is relatively straightforward.

Lemma 4.1 (Weakening). Let Γ′ ≤ Γ and q ≤ q′ ≠ ⊤. 1 If D :: Γ ⊢ N ≤^{q} N′ ⇉ κ then D′ :: Γ′ ⊢ N ≤^{q′} N′ ⇉ κ′ for some D′ ≤ D and κ′ ≤ κ. 2 If D :: Γ ⊢ W ≤^{q} W′ ⇇ κ and κ ≤ κ′ then D′ :: Γ′ ⊢ W ≤^{q′} W′ ⇇ κ′ for some D′ ≤ D.

Corollary 4.2 (Weakening). Let Γ′ ≤ Γ, q ≤ q′, and κ ≤ κ′. If D :: Γ ⊢ F ≤^{q} F′ ⇇ κ then D′ :: Γ′ ⊢ F ≤^{q′} F′ ⇇ κ′ for some D′ ≤ D.

Lemma 4.3 (Strengthening). Assume X ∉ FV(N, N′, F, F′). 1 If Γ, X:pκ ⊢ N ≤^{q} N′ ⇉ κ′ then Γ ⊢ N ≤^{q} N′ ⇉ κ′. 2 If Γ, X:pκ ⊢ F ≤^{q} F′ ⇇ κ′ then Γ ⊢ F ≤^{q} F′ ⇇ κ′.

Lemma 4.4 (Swapping). 1 If Γ ⊢ N ≤^{q} N′ ⇉ κ then Γ ⊢ N′ ≤^{−q} N ⇉ κ. 2 If Γ ⊢ F ≤^{q} F′ ⇇ κ then Γ ⊢ F′ ≤^{−q} F ⇇ κ.

Antisymmetry of algorithmic subtyping is straightforward in our case since our judgement is deterministic—it is more difficult in the presence of bounded quantification (Compagnoni and Goguen, 1999).

Lemma 4.5 (Antisymmetry). 1 If Γ ⊢ N ≤^{q} N′ ⇉ κ and Γ ⊢ N ≤^{q′} N′ ⇉ κ′ then κ = κ′ and Γ ⊢ N ≤^{inf(q,q′)} N′ ⇉ κ. 2 If Γ ⊢ F ≤^{q} F′ ⇇ κ and Γ ⊢ F ≤^{q′} F′ ⇇ κ then Γ ⊢ F ≤^{inf(q,q′)} F′ ⇇ κ.

Proof. Simultaneously by induction. The proof is almost trivial, since algorithmic subtyping is deterministic. The most “difficult” case is:

\frac{Γ ⊢ N ≤^{q} N′ ⇉ pκ_{1} → κ_{2} p^{−1}Γ ⊢ G ≤^{pq} G′ ⇇ κ_{1}}{Γ ⊢ N G ≤^{q} N′ G′ ⇉ κ_{2}}

\frac{Γ ⊢ N ≤^{q′} N′ ⇉ p′κ′_{1} → κ′_{2} p^{′−1}Γ ⊢ G ≤^{p′q′} G′ ⇇ κ′_{1}}{Γ ⊢ N G ≤^{q′} N′ G′ ⇉ κ′_{2}}

Let q′′ = inf(q, q′). By induction hypothesis 1, Γ ⊢ N ≤^{q′′} N′ ⇉ pκ_{1} → κ_{2} and p = p′, κ_{1} = κ′_{1}, and κ_{2} = κ′_{2}. Hence, we can apply induction hypothesis 2 to obtain p^{−1}Γ ⊢ G ≤^{pq′′} G′ ⇇ κ_{1} and conclude with rule al-app-ne .

Transitivity is basically proven by induction on the sum of the lengths of the two given derivations. For the η-rules to go through we need to strengthen the induction hypothesis a bit; alternatively, one can use a different measure (Goguen, 2005).

Lemma 4.6 (Transitivity). Let q, q′ such that q′′ = sup(q, q′) ≠ ⊤. 1 If D_{1} :: Γ ⊢ N_{1} ≤^{q} N_{2} ⇉ κ and D_{2} :: Γ ⊢ N_{2} ≤^{q′} N_{3} ⇉ κ′ then κ = κ′ and

Γ ⊢ N_{1} ≤^{q′′} N_{3} ⇉ κ. 2 If D_{1} :: Γ ⊢ N_{1} ≤^{q} N_{2} ⇉ and D_{2} :: Γ ⊢ N_{2} X⃗ ≤^{q′} N ⇉ κ then Γ ⊢ N_{1} X⃗ ≤^{q′′} N ⇉ κ.

3 If D_{1} :: Γ ⊢ N_{1} ≤^{q} N_{2} ⇉ and D_{2} :: Γ ⊢ N_{2} X⃗ ≤^{q′} W ⇇ κ then Γ ⊢ N_{1} X⃗ ≤^{q′′} W ⇇

κ. 4 Symmetrical to 2: If D_{1} :: Γ ⊢ N ≤^{q} N_{2} X⃗ ⇉ κ and D_{2} :: Γ ⊢ N_{2} ≤^{q′} N_{3} ⇉ then

Γ ⊢ N ≤^{q′′} N_{3} X⃗ ⇉ κ. 5 Symmetrical to 3: If D_{1} :: Γ ⊢ W ≤^{q} N_{2} X⃗ ⇇ κ and D_{2} :: Γ ⊢ N_{2} ≤^{q′} N_{3} ⇉ then

Γ ⊢ W ≤^{q′′} N_{3} X⃗ ⇇ κ. 6 If D_{1} :: Γ ⊢ W_{1} ≤^{q} W_{2} ⇇ κ and D_{2} :: Γ ⊢ W_{2} ≤^{q′} W_{3} ⇇ κ then Γ ⊢ W_{1} ≤^{q′′} W_{3} ⇇ κ.

A direct consequence of part 6 is the following corollary, which holds also for q = ⊤ or q′ = ⊤.

Corollary 4.7 (Transitivity). If Γ ⊢ F_{1} ≤^{q} F_{2} ⇇ κ and Γ ⊢ F_{2} ≤^{q′} F_{3} ⇇ κ then Γ ⊢ F_{1} ≤^{sup(q,q′)} F_{3} ⇇ κ.

Proof of the transitivity lemma. Simultaneously by induction on |D_{1}| + |D_{2}|. Case (part 1):

al-app-ne \frac{Γ ⊢ N_{1} ≤^{q} N_{2} ⇉ pκ_{1} → κ_{2}  p^{−1}Γ ⊢ G_{1} ≤^{pq} G_{2} ⇇ κ_{1}}{Γ ⊢ N_{1} G_{1} ≤^{q} N_{2} G_{2} ⇉ κ_{2}}
al-app-ne \frac{Γ ⊢ N_{2} ≤^{q′} N_{3} ⇉ p′κ′_{1} → κ′_{2}  p^{′−1}Γ ⊢ G_{2} ≤^{p′q′} G_{3} ⇇ κ′_{1}}{Γ ⊢ N_{2} G_{2} ≤^{q′} N_{3} G_{3} ⇉ κ′_{2}}

By induction hypothesis 1 we have p = p′, κ_{1} = κ′_{1} and κ_{2} = κ′_{2} and Γ ⊢ N_{1} ≤^{q′′} N_{3} ⇉ pκ_{1} → κ_{2}. Since sup(pq, pq′) = p sup(q, q′), by induction hypothesis 6 we get Γ ⊢ G_{1} ≤^{pq′′} G_{3} : κ_{1}, and we conclude by rule al-app-ne .

Case (part 2):

Γ ⊢ N_{1} ≤^{q} N_{2} ⇉

al-app-ne \frac{Γ ⊢ N_{2} X⃗ ≤^{q′} N′ ⇉ pκ → κ′  p^{−1}Γ ⊢ X ≤^{pq′} G′ ⇇ κ}{Γ ⊢ N_{2} X⃗ X ≤^{q′} N′ G′ ⇉ κ′}

By induction hypothesis Γ ⊢ N_{1} X⃗ ≤^{q′′} N′ ⇉ pκ → κ′. By the weakening lemma, p^{−1}Γ ⊢ X ≤^{pq′′} G′ ⇇ κ. Hence, the claim follows by rule al-app-ne .

Case (part 3):

Γ ⊢ N_{1} ≤^{q} N_{2} ⇉ al-η-r \frac{Γ, X:pκ ⊢ N_{2} X⃗ X ≤^{q′} F ⇇ κ′}{Γ ⊢ N_{2} X⃗ ≤^{q′} λXF ⇇ pκ → κ′}

By assumption, F ↘ W and Γ, X: pκ ⊢ N_{2} X⃗ X ≤^{q′} W ⇇ κ′. The induction hypothesis yields Γ, X:pκ ⊢ N_{1} X⃗ X ≤^{q′′} W ⇇ κ′, hence we can conclude with rule al-η-r .

Parts 4 and 5 are proven analogously to parts 2 and 3. For part 6, if at least one inequality talks about two neutral constructors, we can use parts 3 and 5, respectively. The remaining cases are represented by: Case Assume X ∉ FV(N_{1}, N_{3}).

al-η-r \frac{Γ, X:pκ ⊢ N_{1} X ≤^{q} F ⇇ κ′}{Γ ⊢ N_{1} ≤^{q} λXF ⇇ pκ → κ′}  al-η-l \frac{Γ, X:pκ ⊢ F ≤^{q} N_{3} X ⇇ κ′}{Γ ⊢ λXF ≤^{q} N_{3} ⇇ pκ → κ′}

By induction hypothesis, Γ, X:pκ ⊢ N_{1} X ≤^{q} N_{3} X ⇇ κ′. This derivation must have been generated from Γ, X: pκ ⊢ N_{1} ≤^{q} N_{3} ⇉ κ′′. By strengthening (Lemma 4.3), Γ ⊢ N_{1} ≤^{q} N_{3} ⇉ κ′′. Applying al-ne , we are done.

Case

al-η-r \frac{Γ, X:pκ ⊢ N X ≤^{q} F ⇇ κ′}{Γ ⊢ N ≤^{q} λXF ⇇ pκ → κ′}  al-λ \frac{Γ, X:pκ ⊢ F ≤^{q′} F′ ⇇ κ′}{Γ ⊢ λXF ≤^{q′} λXF′ ⇇ pκ → κ′}

By induction hypothesis and al-η-r . Case

al-λ \frac{Γ, X:pκ ⊢ F_{1} ≤^{q} F_{2} ⇇ κ′}{Γ ⊢ λXF_{1} ≤^{q} λXF_{2} ⇇ pκ → κ′}  al-λ \frac{Γ, X:pκ ⊢ F_{2} ≤^{q′} F_{3} ⇇ κ′}{Γ ⊢ λXF_{2} ≤^{q′} λXF_{3} ⇇ pκ → κ′}

By induction hypothesis and al-λ .

The next lemma states that the η-rules can be extended beyond neutral constructors. It can be proven directly:

Lemma 4.8 (Generalizing the η-rules). 1 If Γ, Y :pκ ⊢ F Y ≤^{q} F′ ⇇ κ′ and Y ∉ FV(F) then Γ ⊢ F ≤^{q} λY F′ ⇇ pκ → κ′. 2 If Γ, Y :pκ ⊢ F′ ≤^{q} F Y ⇇ κ′ and Y ∉ FV(F) then Γ ⊢ λY F′ ≤^{q} F ⇇ pκ → κ′.

Proof. We prove the first statement, the second is symmetrical. By assumption F Y ↘ W, and by Lemma 3.1 we can distinguish two cases: Case F ↘ N neutral. Then Γ ⊢ N ≤^{q} λY F′ ⇇ pκ → κ′ by rule al-η-r and the goal follows. Case F ↘ λY G and G ↘ W. We get Γ ⊢ λY G ≤^{q} λY F′ ⇇ pκ → κ′ by rule al-λ and

again, the goal follows.

Now we come to the main lemma:

Lemma 4.9 (Substitution and application). Let Γ ≤ pΔ and Δ ⊢ G ≤^{pq} G′ ⇇ κ. 1 If D :: Γ, X : pκ ⊢ N ≤^{q} N′ ⇉ κ′ then either Γ ⊢ [G/X]N ≤^{q} [G′/X]N′ ⇉ κ′ or

rk(κ′) ≤ rk(κ) and Γ ⊢ [G/X]N ≤^{q} [G′/X]N′ ⇇ κ′. 2 If D :: Γ, X : pκ ⊢ W ≤^{q} W′ ⇇ κ′ and Γ ⊢ W, W′ : κ′ then Γ ⊢ [G/X]W ≤^{q}

[G′/X]W′ ⇇ κ′. 3 If D :: Γ ⊢ W ≤^{q} W′ ⇇ pκ → κ′ and Γ ⊢ W, W′ : pκ → κ′ then Γ ⊢ W G ≤^{q} W′ G′ ⇇

κ′.

Note that part 1 works for ill-kinded neutral constructors as well, whereas parts 2 and 3 require well-kinded constructors. Well-kindedness is needed for the case al-ne in part 2.

The three propositions are proven simultaneously by a lexicographic induction on (rk(κ), |D|). It works because the constructor language is essentially the simply-typed λ-calculus (STL), which has a small proof-theoretical strength. The idea is taken from Joachimski and Matthes’ proof of weak normalization for the STL (Joachimski and Matthes, 2003) which I have formalized in Twelf (Abel, 2004). The argument goes probably back to Anne Troelstra, it is implicit in Girard’s combinatorial weak normalization proof (Girard et al., 1989, Ch. 4.3) and has been reused by Watkins et. al. (2003) and Adams (2005, p. 65ff) to define a logical framework based solely on normal terms.

Before proving this lemma, we state some of its immediate consequences that can be proven directly (without induction), and, hence, we can use them on the induction hypotheses in the proof of the lemma.

Corollary 4.10 (Application for arbitrary constructors). Let Γ ≤ pΔ, Δ ⊢ G_{1} ≤^{pq} G_{2} ⇇ κ, and Γ ⊢ F_{1}, F_{2} : pκ → κ′. If Γ ⊢ F_{1} ≤^{q} F_{2} ⇇ pκ → κ′ then Γ ⊢ F_{1} G_{1} ≤^{q} F_{2} G_{2} ⇇ κ′.

Proof. If q = ⊤, there is nothing to show. Otherwise, by assumption F_{1} ↘ W_{1}, F_{2} ↘ W_{2}, and Γ ⊢ W_{1} ≤^{q} W_{2} ⇇ pκ → κ′. By subject reduction, Γ ⊢ W_{1}, W_{2} : pκ → κ′, thus, we can apply the lemma. It yields Γ ⊢ W_{1} G_{1} ≤^{q} W_{2} G_{2} ⇇ κ′, meaning that W_{i} G_{i} ↘ V_{i} and Γ ⊢ V_{1} ≤^{q} V_{2} ⇇ κ′. We are done, since by Lemma 3.1, F_{i} G_{i} ↘ V_{i}.

Corollary 4.11 (Substitution with modified contexts). Let Γ ≤ pΔ, Δ ⊢ G ≤^{pq} G′ ⇇ κ, and p_{0}^{−1}(Γ, X:pκ) ⊢ F, F′ : κ′. If p_{0}^{−1}(Γ, X:pκ) ⊢ F ≤^{p_{0}q} F′ ⇇ κ′ then p_{0}^{−1}Γ ⊢ [G/X]F ≤^{p_{0}q} [G′/X]F′ ⇇ κ′.

Proof. By assumption, F ↘ W, F′ ↘ W′, and p_{0}^{−1}(Γ, X : pκ) ⊢ W ≤^{p_{0}q} W′ ⇇ κ′. Subject reduction entails p_{0}^{−1}(Γ, X:pκ) ⊢ W, W′ : κ′. We need to show

p_{0}^{−1}Γ ⊢ [G/X]W ≤^{p_{0}q} [G′/X]W′ ⇇ κ′,

then the corollary follows by properties of weak head evaluation (Lemma 3.1).

We distinguish cases on p and p_{0}. If p_{0}q = ⊤, there is nothing to show, thus, in the following, we can exclude q = ⊤ and p_{0} = ⊤. Case p_{0} = +. The goal is a direct instance of the lemma. Case p_{0}^{−1}p = ⊤. Setting p′ := ⊤, q′ := p_{0}q, and Γ′ := p_{0}^{−1}Γ, the assumption simplifies to

Γ′, X:p′κ ⊢ W ≤^{q′} W ⇇ κ′. We have Γ′ ≤ p′Δ (by taking the inverse of p_{0} on Γ ≤ pΔ), and trivially Δ ⊢ G ≤^{p′q′} G′ ⇇ κ, since p′q′ = ⊤. Now the goal is an instance of the lemma with Γ′, p′, and q′.

Case p_{0} = ∘. If p ≠ ∘, then p_{0}^{−1}p = ⊤, and this case has already been treated. Otherwise, p = ∘ and our assumptions simplify to Δ ⊢ G ≤^{∘∘} G′ ⇇ κ and ∘^{−1}Γ, X:∘κ ⊢ W ≤^{∘} W′ ⇇ κ′. The goal ∘^{−1}Γ ⊢ [G/X]W ≤^{∘} [G′/X]W′ : κ′ follows now from the lemma, since from the assumption Γ ≤ ∘Δ = ∘∘Δ we obtain ∘^{−1}Γ ≤ ∘Δ.

Case p_{0} = −. The assumptions can be written as Δ ⊢ G ≤^{(−p)(−q)} G′ : κ and −Γ, X:(−p)κ ⊢ W ≤^{−q} W′ ⇇ κ′. Since Γ ≤ pΔ entails −Γ ≤ (−p)Δ, our goal follows from the lemma.

Proof of Lemma 4.9. The three statements are shown simultaneously by lexicographic induction on (rk(κ), |D|). First, we prove the substitution lemma for neutral constructors: Case p ≤ + and κ′ = κ and

D = \overline{Γ, X:pκ ⊢ X ≤^{q} X ⇉ κ}

Since pq ≤ q and Γ ≤ pΔ ≤ Δ, we can weaken the assumption Δ ⊢ G ≤^{pq} G′ ⇇ κ to Γ ⊢ G ≤^{q} G′ ⇇ κ and have trivially rk(κ′) ≤ rk(κ).

Case

D = \frac{(Y :p′κ′) ∈ Γ p′ ≤ +}{Γ, X:pκ ⊢ Y ≤^{q} Y ⇉ κ′}

Then of course Γ ⊢ Y ≤^{q} Y ⇉ κ′. Case

D = \frac{\begin{matrix}D_{1} \\ Γ, X:pκ ⊢ N ≤^{q} N′ ⇉ p_{0}κ_{0} → κ′ \end{matrix} \begin{matrix}D_{2} \\ p_{0}^{−1}(Γ, X:pκ) ⊢ I ≤^{p_{0}q} I′ ⇇ κ_{0} \end{matrix}}{Γ, X:pκ ⊢ N I ≤^{q} N′ I′ ⇉ κ′}

Let M = [G/X]N, M′ = [G′/X]N′, J = [G/X]I, and J′ = [G′/X]I′. Using Cor. 4.11, the induction hypothesis 2 on D_{2} yields p_{0}^{−1}Γ ⊢ J ≤^{p_{0}q} J′ ⇇ κ_{0}. Induction hypothesis 1 on D_{1} has two possible results: Subcase Γ ⊢ M ≤^{q} M′ ⇉ p_{0}κ_{0} → κ′. Apply al-app-ne . Subcase Γ ⊢ M ≤^{q} M′ ⇇ p_{0}κ_{0} → κ′. Since rk(κ_{0}) < rk(p_{0}κ_{0} → κ′) ≤ rk(κ), we can

use induction hypothesis 3 to obtain our goal Γ ⊢ M J ≤^{q} M′ J′ ⇇ κ′. The required inequation rk(κ′) ≤ rk(κ) follows trivially.

Secondly, we consider some cases of substitution into checking-mode subtyping derivations: Case

D = \frac{Γ, X:pκ ⊢ N ≤^{q} N′ ⇉ κ′′}{Γ, X:pκ ⊢ N ≤^{q} N′ ⇇ κ′}

By induction hypothesis, either Γ ⊢ [G/X]N ≤^{q} [G′/X]N′ ⇉ κ′′. Then we simply apply rule al-ne . Or Γ ⊢ [G/X]N ≤^{q} [G′/X]N′ ⇇ κ′′. Since Γ, X : pκ ⊢ N, N′ : κ′, we have by the soundness theorem (Thm 3.4) that κ′′ ≤ κ′. By the weakening lemma, Γ ⊢ [G/X]N ≤^{q} [G′/X]N′ ⇇ κ′.

Case κ′ = p_{1}κ_{1} → κ_{2} and

D = \frac{Γ, Y :p_{1}κ_{1}, X:pκ ⊢ N Y ≤^{q} F ⇇ κ_{2}}{Γ, X:pκ ⊢ N ≤^{q} λY F ⇇ p_{1}κ_{1} → κ_{2}} .

W. l. o. g., Y ∉ FV(G, G′). Since Γ, X: pκ ⊢ N, λY F : p_{1}κ_{1} → κ_{2} by assumption, we get Γ, Y :p_{1}κ_{1}, X:pκ ⊢ N Y, F : κ_{2} by inversion and weakening on kinding. Hence, we can apply the induction hypothesis yielding Γ, Y :p_{1}κ_{1} ⊢ ([G/X]N) Y ≤^{q} [G′/X]F ⇇ κ_{2}. Thus, Γ ⊢ [G/X]N ≤^{q} [G′/X](λY F) ⇇ p_{1}κ_{1} → κ_{2} by the generalized η-rule (Lemma 4.8).

Finally, we turn our attention to the application lemma: Case

D = \frac{Γ ⊢ N ≤^{q} N′ ⇉ κ′}{Γ ⊢ N ≤^{q} N′ ⇇ pκ_{1} → κ_{2}}

By the soundness theorem, κ′ = p′κ′_{1} → κ′_{2} ≤ pκ_{1} → κ_{2}. We weaken the assumption to Δ ⊢ G ≤^{p′q} G′ ⇇ κ′_{1}, and conclude by al-app-ne and al-ne .

Case

D = \frac{Γ, X:pκ ⊢ N X ≤^{q} F ⇇ κ′}{Γ ⊢ N ≤^{q} λXF ⇇ pκ → κ′} X ∉ FV(N)

By induction hypothesis 2 (with Cor. 4.11) we get Γ ⊢ N G ≤^{q} [G/X]F ⇇ κ′. We are done, since (λXF) G and [G/X]F have the same weak head normal form.

Theorem 4.12 (Completeness). 1 If D :: Γ ⊢ F : κ then Γ ⊢ F ≤^{q} F ⇇ κ. 2 If D :: Γ ⊢ F = F′ : κ then Γ ⊢ F ≤^{∘} F′ ⇇ κ. 3 If D :: Γ ⊢ F ≤ F′ : κ then Γ ⊢ F ≤^{+} F′ ⇇ κ.

Proof. Simultaneously by induction on D. Case kind-c , eq-c : Use al-c and al-ne . Case kind-var , eq-var : Use al-var and al-ne . Case kind-λ , eq-λ , leq-λ : Use al-λ on the induction hypothesis. Case kind-app , eq-app : Use application lemma (Cor. 4.10) on the induction hypotheses. Case

eq-β \frac{Γ, X:pκ ⊢ F : κ′  p^{−1}Γ ⊢ G : κ}{Γ ⊢ (λXF) G = [G/X]F : κ′}

By induction hypothesis, Γ, X : pκ ⊢ F ≤^{∘} F ⇇ κ′ and p^{−1}Γ ⊢ G ≤^{p∘} G′ ⇇ κ. By the substitution lemma (Cor. 4.11) we get Γ ⊢ [G/X]F ≤^{∘} [G/X]F ⇇ κ. Since [G/X]F ↘ W implies (λXF) G ↘ W, we are done.

Case

eq-η \frac{Γ ⊢ F : pκ → κ′}{Γ ⊢ (λX. F X) = F : pκ → κ′}

By induction hypothesis, Γ ⊢ F ≤^{∘} F ⇇ pκ → κ′, and we can use the application lemma to get Γ, X: pκ ⊢ F X ≤^{∘} F X ⇇ κ′. Using the generalized η-rule (Lemma 4.8), we infer Γ ⊢ λX. F X ≤^{∘} F ⇇ pκ → κ′.

Case

eq-⊤ \frac{Γ ⊢ F : ⊤κ → κ′  ⊤^{−1}Γ ⊢ G : κ  ⊤^{−1}Γ ⊢ G′ : κ}{Γ ⊢ F G = F G′ : κ′}

By induction hypothesis Γ ⊢ F ≤^{∘} F ⇇ ⊤κ → κ′. Since trivially ⊤^{−1}Γ ⊢ G ≤^{⊤} G′ ⇇ κ, the goal follows by the application lemma.

Case eq-sym : Use swapping lemma (4.4). Case eq-trans , leq-trans : Use transitivity lemma. Case leq-refl : Use weakening lemma. Case leq-antisym :

leq-antisym \frac{Γ ⊢ F ≤ F′ : κ  Γ ⊢ F′ ≤ F : κ}{Γ ⊢ F = F′ : κ}

By induction hypothesis Γ ⊢ F ≤^{+} F′ ⇇ κ and Γ ⊢ F′ ≤^{+} F ⇇ κ. Swapping the second judgement with Lemma 4.4, we can apply the antisymmetry lemma to infer Γ ⊢ F′ ≤^{∘} F ⇇ κ, since inf(+, −) = ∘.

Case leq-fun , leq-arg+ , leq-arg− : Use application lemma (Cor. 4.10), in the last case also swapping.

Now we have a sound and complete subtyping algorithm, but we have nothing yet to get it started. Since there are no subtyping assumptions or basic subtyping relations (like Nat ≤ Real), two related constructors are already equal. In the next section we will extend the subtyping relation to make it more meaningful.

5. Extension to Sized Types

We extend our type language by size expressions a, which have kind ord, and sized-type constructors of kind pord → κ. This leads to the following grammar for kinds.

\begin{aligned}κ̂ & ::= & κ | ord \\ κ & ::= & ∗ | pκ̂ → κ \end{aligned}

Note that there are no functions into ord, i. e., no kinds pκ̂ → ord. Size expressions obey a simple grammar, they can only be successors of zero or a of variable, or be infinity. (The successor of infinity is identified with infinity, see below.)

SExp ∋ a, b  ::= X | 0 | s a | ∞  size expressions
Constr ∋ A, B, F, G, H ::= a | C | X | λXF | F G type constructors

The constants C are drawn from an extended signature Σ, which features sum, product, inductive, and coinductive types:

1  : ∗  unit type
+ : ∗ →^{+} ∗ →^{+} ∗  disjoint sum
× : ∗ →^{+} ∗ →^{+} ∗  cartesian product
μ_{κ_{∗}} : ord →^{+} (κ_{∗} →^{+} κ_{∗}) →^{+} κ_{∗}  inductive constructors
ν_{κ_{∗}} : ord →^{−} (κ_{∗} →^{+} κ_{∗}) →^{+} κ_{∗}  coinductive constructors

The first argument to μ_{κ} and ν_{κ} shall be written as superscript. Inductive types μ_{κ_{∗}}^{a}F and coinductive types ν_{κ_{∗}}^{a}F can only be of kinds that do not mention ord. These are called pure kinds from here and denoted by κ_{∗}.

In the extended signature we can, for instance, model lists of length < n as List^{a}A := μ_{∗}^{a}λX. 1 + A × X where a = s (s … (s 0)) (n times s). Streams of depth of at least n are represented as Stream^{a} A := ν_{∗}^{a}λX. A × X. The type List^{∞}A contains lists or arbitrary length, and Stream^{∞}A productive streams (which never run out of elements). We call such types with an ordinal index sized. Naturally, lists are covariant in their size argument and streams are contravariant (each stream which produces at least n + 1 elements produces of course also at least n elements).

Barthe et. al. (2004) define a calculus λ with sized inductive and coinductive types in which all recursive functions are terminating and all streams are productive. Their sizes follow the same grammar, but are called stage expressions. Sized data types are introduced by a set of data constructors—we can define them using μ and ν. The normalization property is ensured by a restricted typing rule for recursion; in our notation it reads

\frac{ı : ord, f : μ_{∗}^{ı}F → G ı ⊢ e : μ_{∗}^{s ı}F → G (s ı)  F : ∗ →^{+} ∗  G : ord →^{+} ∗}{(letrec f = e) : ∀_{ord}λı. μ_{∗}^{ı}F → G ı}.

Similarly, corecursive functions are introduced by

\frac{ı : ord, f : G⃗ ı → ν_{∗}^{ı}F ⊢ e : G⃗ (s ı) → ν_{∗}^{s ı}F  F : ∗ →^{+} ∗  G⃗ : ord →^{−} ∗}{(^{co}letrec f = e) : ∀_{ord}λı. G⃗ ı → ν_{∗}^{ı}F}.

We have reduced the stage expressions of λ to just constructors of a special kind and model the inclusion between sized types of different stages simply by variance. Lifting the restriction of λ that type constructors must be monotone in all arguments comes at no cost in our formulation: We can define the type of A-labeled, B-branching trees as Tree^{a} A B = μ_{∗}^{a}λX. 1 + A × (B → X), where now

Tree : ord →^{+} ∗ →^{+} ∗ →^{−} ∗.

Higher-order subtyping becomes really necessary when we allow inductive constructors instead of inductive types. These are necessary to model higher-order and heterogeneous (also called nested) datatypes, as for instance powerlists:

PList : ord →^{+} ∗ →^{+} ∗
PList^{a} := μ_{+∗→∗}^{a}λXλA. A + X (A × A)

Many more examples for datatypes of this kind can be found in the literature (Okasaki, 1999; Altenkirch and Reus, 1999; Bird and Paterson, 1999; Hinze, 2000; Abel et al., 2005).

Having the machinery of higher-order subtyping running, the extensions needed for sized types are minimal:

Kinding, equality and subtyping. These judgements are now considered w. r. t. the extended kind and constructor grammar. Additional rules are:

kind-0 \overline{Γ ⊢ 0 : ord}  kind-s \frac{Γ ⊢ a : ord}{Γ ⊢ s a : ord}  kind-∞ \overline{Γ ⊢ ∞ : ord}
eq-s-∞ \overline{Γ ⊢ s ∞ = ∞ : ord}

eq-0 \overline{Γ ⊢ 0 = 0 : ord}  eq-s \frac{Γ ⊢ a = a′ : ord}{Γ ⊢ s a = s a′ : ord}  eq-∞ \overline{Γ ⊢ ∞ = ∞ : ord}

leq-0 \frac{Γ ⊢ a : ord}{Γ ⊢ 0 ≤ a : ord}  leq-s-r \frac{Γ ⊢ a : ord}{Γ ⊢ a ≤ s a : ord}  leq-∞ \frac{Γ ⊢ a : ord}{Γ ⊢ a ≤ ∞ : ord}

leq-s \frac{Γ ⊢ a ≤ a′ : ord}{Γ ⊢ s a ≤ s a′ : ord}

Weak head normal forms and evaluation contexts.

Ne  ∋ N ::= C | X | N G  neutral constructors
Ne_{ord} ∋ n ::= X | 0 | s n  neutral size expressions
Val_{ord} ∋ w ::= n | ∞  size values
Val  ∋ W ::= w | N | λXF weak head values

Weak head evaluation is extended by the following rules:

eval-s-∞ \frac{a ↘ ∞}{s a ↘ ∞}  eval-s \frac{a ↘ n}{s a ↘ s n}  eval-0 \overline{0 ↘ 0}  eval-∞ \overline{∞ ↘ ∞}

Weak head evaluation is still deterministic.

Lemma 5.1 (Soundness of weak head evaluation and completeness of size evaluation). 1 If Γ ⊢ F : κ̂ and F ↘ W then Γ ⊢ F = W : κ̂. 2 If Γ ⊢ a : ord then a ↘ w for some w. 3 If Γ ⊢ a = a′ : ord then a ↘ w and a′ ↘ w for some w.

Neutral size values are compared w. r. t. the following rules:

comp-var \overline{X ≤ X}  comp-s-r \frac{X ≤ n′}{X ≤ s n′}  comp-0 \overline{0 ≤ n}  comp-s \frac{n ≤ n′}{s n ≤ s n′}

Neutral size value comparison is reflexive, transitive and antisymmetric.

Lemma 5.2 (Soundness and completeness of size comparison). 1 If Γ ⊢ n, n′ : ord and n ≤ n′ then Γ ⊢ n ≤ n′ : ord. 2 If Γ ⊢ a ≤ a′ : ord then a ↘ w and a′ ↘ w′ and either w′ = ∞ or w ≤ w′.

Algorithmic subtyping. Now we can extend algorithmic subtyping to kinds κ̂. We need to cover the case κ̂ = ord:

Γ ⊢ a ≤^{⊤} a′ ⇇ ord ⟺ true
Γ ⊢ a ≤^{∘} a′ ⇇ ord ⟺ a ↘ w and a′ ↘ w
Γ ⊢ a ≤^{+} a′ ⇇ ord ⟺ a ↘ w and a′ ↘ w′ and w′ = ∞ or w ≤ w′
Γ ⊢ a ≤^{−} a′ ⇇ ord ⟺ a ↘ w and a′ ↘ w′ and w = ∞ or w′ ≤ w

Lemma 5.3 (Soundness of algorithmic subtyping for ord). Let Γ ⊢ a, a′ : ord. 1 If Γ ⊢ a ≤^{∘} a′ ⇇ ord then Γ ⊢ a = a′ : ord. 2 If Γ ⊢ a ≤^{+} a′ ⇇ ord then Γ ⊢ a ≤ a : ord. 3 If Γ ⊢ a ≤^{−} a′ ⇇ ord then Γ ⊢ a′ ≤ a : ord

Proof. For part 1, use soundness of weak head evaluation. Part 2 uses leq-∞ in case a′ ↘ ∞, and soundness of size comparison otherwise. Part 3 analogously.

Lemma 5.4 (Completeness of algorithmic subtyping for ord). 1 If Γ ⊢ a : ord then Γ ⊢ a ≤^{q} a ⇇ ord. 2 If Γ ⊢ a = a′ : ord then Γ ⊢ a ≤^{∘} a′ ⇇ ord. 3 If Γ ⊢ a ≤ a′ : ord then Γ ⊢ a ≤^{+} a′ ⇇ ord.

Proof. For part 1, we have a ↘ w by Lemma 5.1. In case q = ∘ or w = ∞, we are done, for q ∈ {+, −} use reflexivity of size comparison for neutral w. Part 2 is an instance of Lemma 5.1, and part 3 of Lemma 5.2.

Theorem 5.5. Algorithmic subtyping for the extended system is still sound and complete.

Proof. In case κ̂ = ord use the previous lemmata, otherwise, we can replay the soundness and completeness proof of the previous chapters almost literally.

6. Conclusion and Related Work

We have presented algorithmic subtyping for polarized F^{ω}, without bounded quantification, but with rules for η-equality and subkinding. The algorithm is economic since it computes the βnormal form incrementally, at each step just enough to continue with the subtyping test. Its completeness proof is quite short compared to completeness proofs of related systems in the literature (Steffen, 1998; Compagnoni and Goguen, 2003). However, it is unclear whether the proof scales to bounded quantification—this is worthwhile investigating in the future. From the perspective of proof theory, it should work, but the technical details have to be sorted out.

Related work. The inspiration for the algorithmic subtyping judgement presented here came from Coquand’s βη-conversion algorithm (Coquand, 1991) and the idea for the crucial substitution and application lemma (4.9) from Joachimski and Matthes’ proof of weak normalization for the simply-typed λ-calculus (Joachimski and Matthes, 2003). Both Coquand’s algorithm and Joachimski and Matthes’ characterization of weakly normalizing terms, originally due to van Raamsdonk et. al. (1999), bear strong resemblances to Goguen’s typed operational semantics (Goguen, 1995, 1999).

Our algorithmic subtyping is closely related to Compagnoni and Goguen’s weak-head subtyping (1999; 2003; 2006), but they are additionally dealing with bounded quantification and require neutral constructors to be fully β-normalized. They do not, however, treat η-equality and polarities.

Pierce and Steffen (1997) show decidability of higher-order subtyping with bounded quantification. Their calculus of strong cut-free subtyping is similar to our subtyping algorithm, only that they fully β-normalize the compared constructors and do not treat η. Steffen (1998) extends this work to polarities; in his first formulation, kinding and subtyping are mutually dependent. He resolves this issue by introducing a judgement for variable occurrence. Matthes and I (Abel and Matthes, 2004) have independently of Steffen developed a polarized version of F^{ω} which unifies variable occurrence and kinding through polarized contexts. Duggan and Compagnoni (1999) investigate subtyping for polarized object type constructors. Their system is similar to Steffen’s, albeit without constructor-level λ-abstraction, hence there is no need to care for η.

Watkins et. al. (2003) and Adams (2005) construct logical frameworks solely based on normal terms. This could also be carried out for System F_{≤}^{ω}. Application of two normal terms is immediately normalized, requiring also normalization of substitution. Termination of application and substitution could then also be proven by a lexicographic induction on kind and term. A subtyping algorithm for normal terms can be defined analogously to the one in this article, only that weak head evaluation could be omitted.

Acknowledgments. Thanks to Thierry Coquand and Ralph Matthes for inspiring discussions and to my former colleagues at Chalmers, especially the bosses of my project, for giving me time to work on my PhD thesis. Thanks to Healfdene Goguen and the anonymous referees for reading draft versions of this article and giving helpful and encouraging comments.

References

Abel, A. (2004). Weak normalization for the simply-typed lambda-calculus in Twelf, Logical

Frameworks and Metalanguages (LFM 04), IJCAR, Cork, Ireland. Abel, A. and Matthes, R. (2004). Fixed points of type constructors and primitive recursion, in

J. Marcinkowski and A. Tarlecki (eds), Computer Science Logic, 18th Int. Workshop, CSL 2004, 13th Annual Conf. of the EACSL, Vol. 3210 of Lect. Notes in Comput. Sci., Springer-Verlag, pp. 190–204.

Abel, A., Matthes, R. and Uustalu, T. (2005). Iteration schemes for higher-order and nested

datatypes, Theoretical Computer Science 333(1–2): 3–66. Adams, R. (2005). A Modular Hierarchy of Logical Frameworks, PhD thesis, University of

Manchester. Altenkirch, T. and Reus, B. (1999). Monadic presentations of lambda terms using generalized

inductive types, in J. Flum and M. Rodríguez-Artalejo (eds), Computer Science Logic, 13th Int. Workshop, CSL ’99, 8th Annual Conf. of the EACSL, Vol. 1683 of Lect. Notes in Comput. Sci., Springer-Verlag, pp. 453–468.

Barthe, G., Frade, M. J., Giménez, E., Pinto, L. and Uustalu, T. (2004). Type-based termination

of recursive definitions, Math. Struct. in Comput. Sci. 14(1): 1–45. Bird, R. S. and Paterson, R. (1999). De Bruijn notation as a nested datatype, J. Func. Program.

9(1): 77–91. Compagnoni, A. B. and Goguen, H. (1999). Anti-symmetry of higher-order subtyping, in J. Flum

and M. Rodríguez-Artalejo (eds), Computer Science Logic, 13th Int. Workshop, CSL ’99, 8th Annual Conf. of the EACSL, Vol. 1683 of Lect. Notes in Comput. Sci., Springer-Verlag, pp. 420–438.

Compagnoni, A. B. and Goguen, H. (2003). Typed operational semantics for higher-order sub-

typing, Inf. Comput. 184(2): 242–297. Compagnoni, A. and Goguen, H. (2006). Anti-symmetry of higher-order subtyping and equality

by subtyping, Math. Struct. in Comput. Sci. 16: 41–65. Coquand, T. (1991). An algorithm for testing conversion in type theory, in G. Huet and G. Plotkin

(eds), Logical Frameworks, Cambridge University Press, pp. 255–279. Davies, R. and Pfenning, F. (2000). Intersection types and computational effects, Proc. of the 5th

ACM SIGPLAN Int. Conf. on Functional Programming (ICFP 2000), pp. 198–208. Duggan, D. and Compagnoni, A. (1999). Subtyping for object type constructors. Presented at

FOOL 6. Girard, J.-Y., Lafont, Y. and Taylor, P. (1989). Proofs and Types, Vol. 7 of Cambridge Tracts in

Theoretical Computer Science, Cambridge University Press. Goguen, H. (1995). Typed operational semantics, in M. Deziani-Ciancaglini and G. D. Plotkin

(eds), Proc. of the 2nd Int. Conf. on Typed Lambda Calculi and Applications, TLCA ’95, Vol. 902 of Lect. Notes in Comput. Sci., Springer-Verlag, pp. 186–200.

Goguen, H. (1999). Soundness of the logical framework for its typed operational semantics, in J.-Y. Girard (ed.), Proc. of the 4th Int. Conf. on Typed Lambda Calculi and Applications, TLCA’99, Vol. 1581 of Lect. Notes in Comput. Sci., Springer-Verlag.

Goguen, H. (2005). Justifying algorithms for βη conversion, in V. Sassone (ed.), Foundations of Software Science and Computational Structures, FOSSACS 2005, Edinburgh, UK, Vol. 3441 of Lect. Notes in Comput. Sci., Springer-Verlag, pp. 410–424.

Harper, R. and Pfenning, F. (2005). On equivalence and canonical forms in the LF type theory,

ACM Transactions on Computational Logic 6(1): 61–101. Hinze, R. (2000). Generalizing generalized tries, J. Func. Program. 10(4): 327–351. Hughes, J., Pareto, L. and Sabry, A. (1996). Proving the correctness of reactive systems us-

ing sized types, Proc. of the 23rd ACM Symp. on Principles of Programming Languages, POPL’96, pp. 410–423.

Joachimski, F. and Matthes, R. (2003). Short proofs of normalization, Archive of Mathematical

Logic 42(1): 59–87. Mendler, N. P. (1987). Recursive types and type constraints in second-order lambda calculus,

Proc. of the 2nd IEEE Symp. on Logic in Computer Science (LICS’87), IEEE Computer Soc. Press, pp. 30–36.

Okasaki, C. (1999). From fast exponentiation to square matrices: An adventure in types, Proc.

of the 4th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP ’99), pp. 28–35. Pierce, B. C. (2002). Types and Programming Languages, MIT Press. Pierce, B. C. and Steffen, M. (1997). Higher order subtyping, Theor. Comput. Sci. 176(1,2): 235–

282. Steffen, M. (1998). Polarized Higher-Order Subtyping, PhD thesis, Technische Fakultät, Uni-

versität Erlangen. van Raamsdonk, F., Severi, P., Sørensen, M. H. and Xi, H. (1999). Perpetual reductions in lambda

calculus, Inf. Comput. 149(2): 173–225. Watkins, K., Cervesato, I., Pfenning, F. and Walker, D. (2003). A concurrent logical framework

I: Judgements and properties, Technical report, School of Computer Science, Carnegie Mellon University, Pittsburgh.