Math. Struct. in Comp. Science (1993), vol. 11, pp. 1–000 Copyright \begin{matrix}c \\ ◯ \end{matrix} Cambridge University Press

Strong Normalization with Non-structural Subtyping

M I T C H E L L W A N D^{†}^{‡} P A T R I C K O’ K E E F E^{§} J E N S P A L S B E R G^{¶}

Received June 1, 1994

We study a type system with a notion of subtyping that involves a largest type ⊤, a smallest type ⊥, atomic coercions between base types, and the usual ordering of function types. We prove that any λ-term typable in this system is strongly normalizing; this solves an open problem of Thatte. We also prove that the fragment without ⊥ types strictly fewer terms. This demonstrates that ⊥ adds power to a type system.

1. Introduction

Statically-typed languages are desirable for many reasons, but they are often more restrictive than dynamically-typed languages. In particular, it is desirable to allow stronglytyped languages to have “holes” in the type structure, so that portions of the program that are not fully understood may be written using dynamic typing. There have been several proposals for creating such holes, such as (Gomard 1990; Thatte 1988; Wand 1984). Typically, one gives the result of such an untyped computation a special type, untyped. Such a value can be passed as an ordinary value, but is not manipulable except by a polymorphic procedure, such as print (Wand 1984). Thatte (Thatte 1988) called this partial type inference.

The addition of a type untyped allows several different kinds of flexibility. It allows portions of a program to escape the scrutiny of the type-checker (Wand 1984); it allows for heterogeneous lists and persistent data (Thatte 1988); and it can also be used to facilitate binding-time analysis or analysis of type errors (Gomard 1990). It also serves as a basis for dealing with the “don’t care” types for records in (Rémy 1989).

In this paper we study a type system with a notion of subtyping that involves a largest type ⊤, a smallest type ⊥, atomic coercions between base types, and the usual ordering of function types. We prove that any λ-term typable in this system is strongly normalizing. The constant type ⊤ corresponds to untyped. The constant type ⊥ is useful for typing “dead code”. Thatte’s partially typed terms (Thatte 1988) correspond to the fragment

† Work supported by the National Science Foundation and ARPA under grants CCR-9002253 and

CCR-9014603. ‡ College of Computer Science, Northeastern University, 360 Huntington Avenue, 161CN, Boston, MA

02115, USA. E-mail: wand@ccs.neu.edu. § 151 Coolidge Avenue #211, Watertown, MA 02172, USA. E-mail: pmo@world.std.com. ¶ Computer Science Department, Aarhus University, DK-8000 Aarhus C, Denmark. E-mail:

  palsberg@daimi.aau.dk.

without ⊥. Our result implies that partially typed terms are strongly normalizing as well, solving an open problem in (Thatte 1988). We also prove that the fragment without ⊥ types strictly fewer terms.

2. The Formal System

2.1. Types

The set of partial types is parameterized by a partially ordered set of atomic types (B, ⊑), where B consists of constant type symbols and where B ∩ {⊥, ⊤, →} = ∅. For example, we might have B = {Int, Real}, where Int ⊑ Real, Int ⊑ Int, and Real ⊑ Real.

Partial types comprise an ordered set (T_{B}, ≤), where T_{B} is the set of well-formed finite terms over B ∪ {⊥, ⊤, →}. (For an extension with recursive types, see the paper by Amadio and Cardelli (Amadio and Cardelli 1993).) Here, ⊥ and ⊤ are constant symbols, and → is a binary type constructor. The order ≤ is defined inductively by the rules

\frac{b ⊑ b′}{b ≤ b′}

⊥ ≤ t

t ≤ ⊤

\frac{s′ ≤ s t ≤ t′}{s → t ≤ s′ → t′}

where b, b′ range over atomic types, and s, s′, t, t′ range over types. Intuitively, if s ≤ t, then we can coerce s to t. The coercions among elements of B have been called atomic by Mitchell (Mitchell 1991). We will refer to the fourth rule as the congruence rule for function types. Typical inclusions are ⊥ ≤ ⊥ → ⊤, ⊤ → ⊤ ≤ ⊤, ⊤ → ⊤ ≤ (⊤ → ⊤) → ⊤. Lemma 1. The relation ≤ is a partial order.

Proof. Reflexivity: Given t, we need to derive t ≤ t. This follows by straightforward induction on the structure of t, using that ⊑ is reflexive. Asymmetry: Assume that t ≤ t′ and t′ ≤ t are derivable. We proceed by induction on the sum of the sizes of t and t′. If either t or t′ is in B ∪ {⊥, ⊤}, then clearly t = t′. Otherwise, both t and t′ are function types and the two derivations of t ≤ t′ and t′ ≤ t have the congruence rule as their last step. The result then follows from the induction hypothesis. Transitivity: Assume t ≤ t′ and t′ ≤ t′′ are derivable. We need to show that also t ≤ t′′ is derivable. We proceed by induction on the structure of t′′. Suppose first that t′′ is an atomic type. Then t′ is either ⊥ or an atomic type. If t′ = ⊥, then t = ⊥, so t ≤ t′′. If t′ is an atomic type, then t is either ⊥ or an atomic type. If t = ⊥, the t ≤ t′′, and if t is an atomic type, then the result follows from ⊑ being transitive. Suppose then that t′′ = ⊥. Clearly, t = t′ = ⊥, so t ≤ t′′. Suppose then that t′′ = ⊤. Clearly, t ≤ t′′.

Suppose finally that t′′ is a function type. Then t′ is either ⊥ or a function type. If t′ = ⊥, then t = ⊥, so t ≤ t′′. If t′ is a function type, then t is either ⊥ or a function type. If t = ⊥, then clearly t ≤ t′′. Thus, we are left with the case where all of t, t′, and t′′ are function types. Then, both of the derivations of t ≤ t′ and t′ ≤ t′′ have uses of the congruence rule as their last step. The result then follows from the induction hypothesis.

2.2. Programs

Programs are untyped λ-terms with typed constants. We write constants as c^{t} where t ∈ T_{B}. Polymorphic let can be treated by using the equivalence let x = M in N as (λd.N[d/x])M, where d is fresh.

If M is a λ-term, t is a type, and A is a type environment, i.e., a partial function assigning types to variables, then the judgement

A ⊢ M : t

means that M has the type t in the environment A. Formally, this holds when the judgement is derivable using the following five rules:

A ⊢ c^{t}: t

A ⊢ x: t (A(x) = t)

\frac{A[x ← t_{1}] ⊢ M: t_{2}}{A ⊢ (λx.M): t_{1} → t_{2}}

\frac{A ⊢ M: t_{1} → t_{2} A ⊢ N: t_{1}}{A ⊢ (M N): t_{2}}

\frac{A ⊢ M : t t ≤ t′}{A ⊢ M : t′}

The first four rules are the usual rules for simple types and the last rule is the rule of subsumption. We denote this type system by PTB (PTB indicates Partial Types with Bottom). Thatte’s system of partial types did not include ⊥; the fragment of the type system without ⊥ will be denoted PT. Reduction is as usual given by the rewriting rule scheme (λx.M)M′ ⇒ M[M′/x]; Mitchell (Mitchell 1991) has shown that subject reduction holds.

This system types terms which are not typable in the simply-typed λ-calculus. For example, consider λf.(fK(fI)), where K and I are the usual combinators. This is not typable in the ordinary calculus, since K and I have different types, but it is typable under partial typing: assign f the type ⊤ → ⊤ → ⊤. Both the K and I can be coerced to type ⊤, and the result (fI), of type ⊤ → ⊤, can be coerced to ⊤ to form the second argument of the first f. Therefore the entire term has type (⊤ → ⊤ → ⊤) → ⊤.

Similarly, some self-application is possible: (λx.xx) has type (⊤ → t) → t for all t, since the final x can be coerced to ⊤.

However, not all terms are typable in this system. Our main result is that any λ-term typable in this system is strongly normalizing. To indicate the flavor of those strongly normalizing λ-term which are not typable in this system, we will prove in Section 5 that (λx.xxx)(λy.y) is not typable in PTB.

In Section 5 we also prove that the λ-term (λf.f(fx))(λv.vy) is typable in PTB but not in PT. This demonstrates that ⊥ adds power to a type system.

While both PTB and System F contain only strongly normalizing λ-terms, they are incomparable because 1 The λ-term (λx.xxx)(λy.y) is not typable in PTB, but it is typable in F, and 2 The λ-term (λx.λy.y(xI)(xK))Δ, where I = λa.a, K = λb.λc.b, and Δ = λd.dd, is

not typable in F (Giannini and Rocca 1988), but it is typable in PTB and also in PT. It follows that PT and F are also incomparable. Notice also that (λf.f(fx))(λv.vy) is typable in F, but not in PT.

3. Witnesses

A witness for either a type derivation or a subtype derivation is an explicitly typed and simply typed λ-term with typed constants. If W is such a λ-term, t is a type, and A is a type environment, then the judgement

A ⊢_{ST} W : t

means that W has the simple type t in the environment A. Formally, this holds when the judgement is derivable using the following four rules:

A ⊢_{ST} c^{t}: t

A ⊢_{ST} x: t (A(x) = t)

\frac{A[x ← t_{1}] ⊢_{ST} M: t_{2}}{A ⊢_{ST} (λx : t_{1}.M): t_{1} → t_{2}}

\frac{A ⊢_{ST} M: t_{1} → t_{2} A ⊢_{ST} N: t_{1}}{A ⊢_{ST} (M N): t_{2}}

The subscript ST indicates Simple Typing.

We assume that the language of witnesses contains the following constants:

— For each b, b′ ∈ B, where b ⊑ b′, there is a constant c^{b→b′}.

— For each t ∈ T_{B}, there are constants c^{⊥→t} and c^{t→⊤}.

The judgement t ≤ t′ [C^{t→t′}] means that C^{t→t′} is a witness for t ≤ t′. Formally, this holds when the judgement is derivable using the following four rules:

\frac{b ⊑ b′}{b ≤ b′ [c^{b→b′}]}

⊥ ≤ t [c^{⊥→t}]

t ≤ ⊤ [c^{t→⊤}]

\frac{s′ ≤ s [C^{s′→s}] t ≤ t′ [C^{t→t′}]}{s → t ≤ s′ → t′ [λf : s → t.λx : s′.C^{t→t′}(f(C^{s′→s}x))]}

The judgement

A ⊢_{w} M : t [M′]

means that M′ is a witness for A ⊢ M : t. Formally, this holds when the judgement is derivable using the following five rules:

A ⊢_{w} c^{t}: t [c^{t}]
A ⊢_{w} x: t [x] (A(x) = t)

\frac{A[x ← t_{1}] ⊢_{w} M: t_{2} [M′]}{A ⊢_{w} (λx.M): t_{1} → t_{2} [λx : t_{1}.M′]}

\frac{A ⊢_{w} M: t_{1} → t_{2} [M′] A ⊢_{w} N: t_{1} [N′]}{A ⊢_{w} (M N): t_{2} [M′N′]}

\frac{A ⊢_{w} M : t [M′] t ≤ t′ [C^{t→t′}]}{A ⊢_{w} M : t′ [C^{t→t′}M]}

Thus the witness of a type derivation is the strongly-typed term which is obtained by “inserting the necessary coercions”. This intuition is made precise by the following observations. Lemma 2. The following are true: 1 If s′ ≤ s [C^{s′→s}], then s′ ≤ s and ∅ ⊢_{ST} C^{s′→s}: s′ → s. 2 If A ⊢_{w} M: t [M′], then A ⊢ M: t and A ⊢_{ST} M′: t. 3 If A ⊢ M: t, then there exists M′ such that A ⊢_{w} M: t [M′].

Proof. Straightforward. Lemma 3. If A[x ← t_{1}] ⊢_{w} M: t_{2} [M′] and A ⊢_{w} N: t_{1} [N′], then A ⊢_{w} M[N/x]: t_{2} [M′[N′/x]].

Proof. By induction on the structure of the derivation of A[x ← t_{1}] ⊢_{w} M: t_{2} [M′].

4. The Main Theorem

Theorem 4. If A ⊢ M: t, then M is strongly normalizing.

Proof. By Lemma 2, choose a λ-term M′ so that A ⊢_{w} M: t [M′]. We will prove the following claim:

If A ⊢_{w} M: t [M′] and M ⇒ N, then there exists N′ so that A ⊢_{w} N: t [N′] and M′ ⇒ N′.

To see that the theorem follows from the claim, consider an infinite reduction sequence starting from M. Then, by the claim, we get an infinite reduction sequence starting from M′. But since M′ is typable in the simply-typed λ-calculus, it is strongly normalizing. This gives a contradiction. To prove the claim, we proceed by induction on the size of M′. All cases but the following are straightforward. Consider the case in the induction step where M ≡ (λx.M_{1})M_{2} ⇒ M_{1}[M_{2}/x]. The last step in the derivation of A ⊢_{w} M: t [M′] is

\frac{A ⊢_{w} (λx.M_{1}): t_{1} → t [W] A ⊢_{w} M_{2}: t_{1} [M′_{2}]}{A ⊢_{w} (λx.M_{1})M_{2}: t [W M′_{2}]}

So M′ ≡ W M′_{2}. There are two cases, depending on how A ⊢_{w} (λx.M_{1}): t_{1} → t [W] is derived. In the first case, the last step of the derivation of A ⊢_{w} (λx.M_{1}): t_{1} → t [W] is:

\frac{A[x ← t_{1}] ⊢_{w} M_{1}: t [M′_{1}]}{A ⊢_{w} (λx.M_{1}): t_{1} → t [λx : t_{1}.M′_{1}]}

so W ≡ λx : t_{1}.M′_{1}. From Lemma 3 we get that

A ⊢_{w} M_{1}[M_{2}/x]: t [M′_{1}[M′_{2}/x]]

so the λ-term M′_{1}[M′_{2}/x] has both the desired properties. In the second case, the last step in the derivation of A ⊢_{w} (λx.M_{1}): t_{1} → t [W] is:

\frac{A ⊢_{w} (λx.M_{1}): u [W′] u ≤ t_{1} → t [C^{u→(t_{1}→t)}]}{A ⊢_{w} (λx.M_{1}): t_{1} → t [C^{u→(t_{1}→t)}W′]}

so W ≡ C^{u→(t_{1}→t)}W′. Now, u = u_{1} → u_{2}, for some u_{1} and u_{2}, since ⊤ ≰ t_{1} → t, and no abstraction can have a type in B ∪ {⊥}. So we have

M′ ≡ W M′_{2}
≡ C^{(u_{1}→u_{2})→(t_{1}→t)}W′M′_{2}
≡ (λf : u_{1} → u_{2}.λx : t_{1}.C^{u_{2}→t}(f(C^{t_{1}→u_{1}}x)))W′M′_{2}

From A ⊢_{w} M_{2}: t_{1} [M′_{2}] and t_{1} ≤ u_{1} [C^{t_{1}→u_{1}}], we get A ⊢_{w} M_{2}: u_{1} [C^{t_{1}→u_{1}}M′_{2}]. From that and A ⊢_{w} (λx.M_{1}): u [W′] we get A ⊢_{w} (λx.M_{1})M_{2}: u_{2} [W′(C^{t_{1}→u_{1}}M′_{2})]. By the above equivalence, the term W′(C^{t_{1}→u_{1}}M′_{2}) is smaller than M′ (it is sufficient that it does not include a copy of C^{u_{2}→t}). Hence, by the induction hypothesis, we can choose N′ so that A ⊢_{w} M_{1}[M_{2}/x]: u_{2} [N′] and W′(C^{t_{1}→u_{1}}M′_{2}) ⇒ N′. So A ⊢_{w} M_{1}[M_{2}/x] : t [C^{u_{2}→t}N′]. We also have

M′ ⇒ C^{u_{2}→t}(W′(C^{t_{1}→u_{1}}M′_{2})) ⇒ C^{u_{2}→t}N′

so the λ-term C^{u_{2}→t}N′ has both the desired properties.

Notice that the claim in the proof of Theorem 4 is a refinement of the subject reduction theorem, taking reduction of witnesses into account.

5. Two λ-terms

In this section we prove that

— The strongly normalizing λ-term (λx.xxx)(λy.y) is not typable, and

— The λ-term (λf.f(fx))(λv.vy) is typable; but it is not typable in the fragment of the type system without ⊥.

To obtain such negative results, we rephrase the type inference in terms of solving a system of type constraints, following for example (Kozen et al. 1994).

5.1. Constraints

Given a λ-term M, assume that M has been α-converted so that all bound variables are distinct. Let X_{M} be the set of λ-variables x occurring in M, and let Y_{M} be a set of variables disjoint from X_{M} consisting of one variable [[F]] for each occurrence of a subterm F of M. (The notation [[F]] is ambiguous because there may be more than one occurrence of F in M. However, it will always be clear from context which occurrence is meant.) We generate the following system of inequalities over X_{M} ∪ Y_{M} (notice that λ-variables are also used as type variables):

— for every occurrence in M of a subterm of the form c^{t}, the inequality

t ≤ [[c^{t}]] ;

— for every occurrence in M of a subterm of the form λx.F, the inequality

x → [[F]] ≤ [[λx.F]] ;

— for every occurrence in M of a subterm of the form F G, the inequality

[[F]] ≤ [[G]] → [[F G]] ;

— for every occurrence in M of a λ-variable x, the inequality

x ≤ [[x]] .

Denote by T (M) the system of constraints generated from M in this fashion. The solutions of T (M) over T_{B} correspond to the possible type annotations of M in a sense made precise by Theorem 5.

Let A be a type environment assigning a type to each λ-variable occurring freely in M. If L is a function assigning a type to each variable in X_{M} ∪ Y_{M}, we say that L extends A if A and L agree on the domain of A. Theorem 5. The judgement A ⊢ M : t is derivable if and only if there exists a solution L of T (M) extending A such that L([[M]]) = t. In particular, if M is closed, then M is typable with type t if and only if there exists a solution L of T (M) such that L([[M]]) = t.

Proof. Similar to the proof of Theorem 2.1 in the journal version of (Kozen et al. 1994), in outline as follows. Given a solution of the constraint system, it is straightforward to construct a derivation of A ⊢ M: t. Conversely, observe that if A ⊢ M: t is derivable, then there exists a derivation of A ⊢ M: t such that each use of one of the ordinary rules is followed by exactly one use of the subsumption rule. The approach in for example (Wand 1991; Palsberg and Schwarztbach 1992) then gives a set of inequalities of the desired form.

5.2. An untypable λ-term

In this subsection we prove that the the strongly normalizing λ-term (λx.xxx)(λy.y) is not typable.

First we present a small system of constraints which is unsolvable. Let S be the set consisting of the two constraints

\begin{aligned}y → y & ≤ & y \\ y & ≤ & (y → y) → ⊤ \end{aligned}

Proposition 6. S is not solvable over T_{B}.

Proof. Suppose that S is solvable. Clearly, no solution can assign an element of B ∪ {⊥, ⊤} to y. So choose a type s → t so that it solves S when assigned to y and so that no type of smaller height has this property. From y → y ≤ y and y ≤ (y → y) → ⊤ we get

\begin{aligned}(s → t) → (s → t) & ≤ & s → t \\ s → t & ≤ & ((s → t) → (s → t)) → ⊤ \end{aligned}

so

\begin{aligned}s & ≤ & s → t \\ s → t & ≤ & t \\ (s → t) → (s → t) & ≤ & s \end{aligned}

Clearly, s cannot be an element of B ∪ {⊥, ⊤}. So write s = a → b. Thus,

\begin{aligned}a → b & ≤ & (a → b) → t \\ (a → b) → t & ≤ & t \\ ((a → b) → t) → ((a → b) → t) & ≤ & a → b \end{aligned}

From this we derive

\begin{aligned}a → b & ≤ & a \\ b & ≤ & t \\ (a → b) → t & ≤ & t \\ a & ≤ & (a → b) → t \\ (a → b) → t & ≤ & b \end{aligned}

So

a ≤ (a → b) → t ≤ b

thus a ≤ b. This means that also

a → a ≤ a → b ≤ a

and

a ≤ (a → b) → t ≤ (a → a) → ⊤

So assigning a to y yields a solution of S. This is a contradiction since a has smaller height than s → t (because s → t = (a → b) → t). Proposition 7. The λ-term (λx.xxx)(λy.y) is not typable in PTB.

Proof. To distinguish the three occurrences of x, we denote them x_{1}, x_{2}, and x_{3}. The constraint system T ((λx.xxx)(λy.y)) is as follows.

x ≤ [[x_{1}]]  (1)
x ≤ [[x_{2}]]  (2)
x ≤ [[x_{3}]]  (3)
y ≤ [[y]]  (4)
[[λx.xxx]] ≤ [[λy.y]] → [[(λx.xxx)(λy.y)]]  (5)
y → [[y]] ≤ [[λy.y]]  (6)
x → [[xxx]] ≤ [[λx.xxx]]  (7)

[[x_{1}]] ≤ [[x_{2}]] → [[x_{1}x_{2}]]  (8)
[[x_{1}x_{2}]] ≤ [[x_{3}]] → [[xxx]]  (9)

From these constraints we derive

x ≤ [[x_{1}]]  (using 1)
≤ [[x_{2}]] → [[x_{1}x_{2}]]  (using 8)
≤ [[x_{2}]] → ([[x_{3}]] → [[xxx]])  (using 9)
≤ x → (x → ⊤)  (using 2, 3, and the rule for ⊤)

so x ≤ x → (x → ⊤). We also derive

x → [[xxx]] ≤ [[λx.xxx]]  (using 7)
≤ [[λy.y]] → [[(λx.xxx)(λy.y)]]  (using 5)
≤ (y → [[y]]) → [[(λx.xxx)(λy.y)]] (using 6)
≤ (y → y) → [[(λx.xxx)(λy.y)]] (using 4)

so y → y ≤ x. We can now derive

y → y ≤ x  (using the above)
≤ x → (x → ⊤)  (using the above)
≤ (y → y) → ((y → y) → ⊤) (using the above)

so y → y ≤ (y → y) → ((y → y) → ⊤). Using the congruence rule on this inequality, we get the two constraints in the constraint system S. Thus, if T ((λx.xxx)(λy.y)) is solvable, then S is solvable. So, since S is unsolvable over T_{B} by Proposition 6, we get that T ((λx.xxx)(λy.y)) is unsolvable over T_{B}.

5.3. The power of ⊥

In this subsection we prove that the λ-term (λf.f(fx))(λv.vy) is typable in PTB; but also that it is not typable in PT. The latter result could also be obtained using one of the two known type inference algorithms for PT (O’Keefe and Wand 1992; Kozen et al. 1994). To give some intuition about why this λ-term is untypable over PT, we give a direct proof. Notice that (λf.f(fx))(λv.vy) is not closed. We might have used the closed λ-term λx.λy.(λf.f(fx))(λv.vy) instead, but we have preferred to use the shorter (λf.f(fx))(λv.vy).

We denote by T′_{B} set of well-formed finite terms over B∪{⊤, →}. Notice that T′_{B} ⊆ T_{B}. Intuitively, the set T′_{B} is the subset of T_{B} “without ⊥”.

We first present a small system of constraints which is unsolvable over T′_{B} but solvable over T_{B}. Let S′ be the singleton set consisting of the constraint

v ≤ y → v

Proposition 8. S′ is not solvable over T′_{B}.

Proof. First note that we can solve S′ over T_{B} by assigning ⊥ to v and any type to y. Suppose then that S′ is solvable over T′_{B}. Choose a solution L over T′_{B} with the property that any other solution over T_{B} maps v to a type of at least the same height as L(v). Clearly, L does not map v to an element of B ∪ {⊤}. So write L(v) = s → t. From v ≤ y → v we get

s → t ≤ L(y) → (s → t)

So

t ≤ s → t

Thus, by assigning t to v and by assigning s to y, we obtain a solution of S′. This is a contradiction since t has smaller height than s → t. Proposition 9. The λ-term (λf.f(fx))(λv.vy) is typable in PTB but not in PT.

Proof. To distinguish the two occurrences of f, we denote them f_{1} and f_{2}. Moreover, we will denote by M the term (λf.f(fx))(λv.vy). The constraint system T (M) is as follows.

[[λf.f(fx)]] ≤ [[λv.vy]] → [[M]]  (10)
f → [[f(fx)]] ≤ [[λf.f(fx)]]  (11)
[[f_{1}]] ≤ [[fx]] → [[f(fx)]]  (12)
[[f_{2}]] ≤ x → [[fx]]  (13)
f ≤ [[f_{1}]]  (14)
f ≤ [[f_{2}]]  (15)
v → [[vy]] ≤ [[λv.vy]]  (16)
[[v]] ≤ y → [[vy]]  (17)
v ≤ [[v]]  (18)

From these constraints we derive

([[fx]] → [[f(fx)]]) → [[f(fx)]] ≤ [[f_{1}]] → [[f(fx)]]  (using 12)
≤ f → [[f(fx)]]  (using 14)
≤ [[λf.f(fx)]]  (using 11)
≤ [[λv.vy]] → [[M]]  (using 10)
≤ (v → [[vy]]) → [[M]] (using 16)

so [[fx]] ≤ v and v → [[vy]] ≤ f. We also derive

v → [[vy]] ≤ f  (using the above)
≤ [[f_{2}]]  (using 15)
≤ x → [[fx]]  (using 13)

so [[vy]] ≤ [[fx]]. We can now derive

v ≤ [[v]]  (using 18)
≤ y → [[vy]]  (using 17)
≤ y → [[fx]] (using the above)
≤ y → v  (using the above)

so v ≤ y → v. Thus, if T (M) is solvable over T′_{B}, then S′ is solvable over T′_{B}. So, since S′ is unsolvable Strong Normalization with Non-structural Subtyping 11

over T′_{B} by Proposition 8, we get that T (M) is not solvable over T′_{B}, and hence M is not typable in PT. To see that M is typable in PTB, give f the type ⊥ → ⊥, give v the type ⊥, and give both x and y the type ⊥. The subterm λv.vy has type ⊥ because we can coerce the type of the occurrence of v to be ⊥ → ⊥.

Acknowledgements

The authors thank Fritz Henglein and Jonathan Young for helpful discussions.

References

Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on

Programming Languages and Systems, 15(4):575–631, 1993. Also in Proc. POPL’91. Paola Giannini and Simona Ronchi Della Rocca. Characterization of typings in polymorphic

type discipline. In Proc. LICS’88, Third Annual Symposium on Logic in Computer Science, pages 61–70, 1988.

Carsten K. Gomard. Partial type inference for untyped functional programs. In Proc. ACM

Conference on Lisp and Functional Programming, pages 282–287, 1990. Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient inference of partial types.

Journal of Computer and System Sciences, 49(2):306–324, 1994. Also in Proc. FOCS’92, 33rd IEEE Symposium on Foundations of Computer Science, pages 363–371, Pittsburgh, Pennsylvania, October 1992.

John C. Mitchell. Type inference with simple subtypes. Journal of Functional Programming,

1:245–285, 1991. Patrick M. O’Keefe and Mitchell Wand. Type inference for partial types is decidable. In Proc.

ESOP’92, European Symposium on Programming, pages 408–417. Springer-Verlag (LNCS 582), 1992.

Jens Palsberg and Michael I. Schwartzbach. Safety analysis versus type inference for partial

types. Information Processing Letters, 43:175–180, 1992. Didier Rémy. Typechecking records and variants in a natural extension of ML. In Sixteenth

Symposium on Principles of Programming Languages, pages 77–88, 1989. Satish Thatte. Type inference with partial types. In Proc. International Colloquium on Au-

tomata, Languages, and Programming 1988, pages 615–629. Springer-Verlag (LNCS 317), 1988.

Mitchell Wand. A semantic prototyping system. In Proc. ACM SIGPLAN’84 Symposium on

Compiler Construction, pages 213–221. Sigplan Notices, 1984. Mitchell Wand. Type inference for record concatenation and multiple inheritance. Information

and Computation, 93(1):1–15, 1991.