/u2/csfaculty/wand/types/partial/sn.tex 14:14 May 11, 1994

Partially Typed Terms are Strongly Normalizing

Mitchell Wand^{∗}

College of Computer Science Northeastern University 360 Huntington Avenue, 161CN Boston, MA 02115, USA wand@corwin.ccs.northeastern.edu

May 11, 1994

Abstract

Thatte [4] introduced the discipline of partial types. This is a type discipline using a subtype relation with a largest element Ω (or untyped) and closed under the usual antimonotonic rule for function types. This discipline types pure lambda-terms that are not typable under the usual strong typing rules. We show that any term typable under partial typing is strongly normalizing. The proof extends to other subtyping relations as well.

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 strongly-typed 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 [1, 4, 6]. 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 [6]. Thatte [4] called this partial type inference.

∗Work supported by the National Science Foundation and DARPA under grants CCR-9002253 and CCR-9014603.

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 [6]; it allows for heterogeneous lists and persistent data [4]; and it can also be used to facilitate binding-time analysis or analysis of type errors [1]. It also serves as a basis for dealing with the “don’t care” types for records in [3].

Here we consider a question originally posed by Thatte [4]: are all partiallytypable terms strongly normalizing? We show that the answer is positive, both for the partial-type discipline and for a wider class of subtyping disciplines.

2 The Formal System

2.1 Types

The set of types is defined by the following grammar:

⟨type⟩ ::= ⟨atomic type⟩ | Ω | ⟨type⟩ → ⟨type⟩

The inclusions between types are defined by the rules:

t ≤ Ω
b ≤ b

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

where b ranges over atomic types and s, t, etc., range over types. We will refer to the second rule as the congruence rule for arrow types.

Thus, typical inclusions are Ω → Ω ≤ Ω, Ω → Ω ≤ (Ω → Ω) → Ω, etc.

While our coercions are not atomic in the sense of [2], they have the property that for any t and u there is at most one proof of t ≤ u, and this proof follows the structure of u. This makes it easier to reason about these inequalities. For example, we do not include the reflexive or transitive rules, because these are admissible:

Theorem 1 The relation ≤ is a partial order.

Proof: It is easy to show that for all types t, t ≤ t is provable from these rules. For the transitive property, assume t ≤ t′ and t′ ≤ t′′ are provable. We need to show that t ≤ t′′ is provable as well. We proceed by induction on the structure of t′′. If t′′ is an atomic type b, then t′ and t must be b as well. If t′′ = Ω, then t ≤ t′′. If t′ = Ω, then t′′ = Ω, so t ≤ t′′. Otherwise all of t, t′, and t′′ are arrow types, and both proofs must have the congruence rule as their last step. Then the result follows by induction on the components.

For the asymmetry property, assume that t ≤ t′ and t′ ≤ t. If either t or t′ is b or Ω, then the other must be Ω also. If neither is b or Ω, then both proofs must have the congruence rule as their last step, and the result follows by induction. □

2.2 Programs

Programs are ordinary untyped lambda-terms with typed constants. Polymorphic let can be treated by using the equivalence let x = M in N as N[M/x]. We use the usual typing rules plus the subsumption rule

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

The details are routine.

Reduction in this system is as usual; [2] shows that subject reduction holds. We write M ⇒ N for reduction.

This system types terms which are not typable in the simply-typed lambdacalculus without coercions. 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. For example:

Proposition 1 (λx.xx)(λx.xx) is not typable in this system.

Proof: The types of (λx.xx) are those types which are bounded below by a type of the form (t_{1} → t_{2}) → t_{2} where t_{1} → t_{2} ≤ t_{1}. In order to type (λx.xx)(λx.xx), we need to find two such types, one for each occurrence of (λx.xx), such that the type of the second coerces to the argument type of the first. By a standard argument, we need consider only the case in which the types are actually of the lower-bound types; all the coercion can be incorporated into the coercion of the argument. That is, we need to find two types of the form (t_{1} → t_{2}) → t_{2} and (u_{1} → u_{2}) → u_{2}, where (u_{1} → u_{2}) → u_{2} ≤ (t_{1} → t_{2}). After splitting the last equation, we are left with four inequalities to solve:

\begin{matrix}t_{1} → t_{2} ≤ t_{1} \\ u_{1} → u_{2} ≤ u_{1} \\ t_{1} ≤ u_{1} → u_{2} \\ u_{2} ≤ t_{2} \end{matrix}

From these a short deduction leads to u_{1} → u_{2} ≤ u_{1} ≤ u_{1} → u_{2}. Since ≤ is a partial order, we have u_{1} = u_{1} → u_{2}, which has no solution in our system. □

3 Witnesses

Let us begin by writing down the standard rules for type inference with subtypes:

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′}

where, in the last rule, ≤ is the subtype relation. We will occasionally consider the ordinary simple-typing discipline, in which the last rule is omitted; we will use ⊢_{ST} for this relation.

We wish to consider a class of subtype relations. We assume that we have a set of basic subtype relations t ≤ t′, and that these relations are closed under the usual rule for function spaces

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

To formalize these rules, let us define the notion of a witness for a type or subtype derivation. Consider the language of λ-terms over a language with constants c_{t,t′} : t → t′ for every basic subtype relation. A witness for a derivation will be a λ-term in this language. Witnesses are defined inductively:

1. The constant c_{t,t′} is a witness for t ≤ t′.

2. If C_{s′,s} is a witness for s′ ≤ s and C_{t,t′} is a witness for t ≤ t′, then λf : s → t.λx : s′.C_{t,t′}(f(C_{s′,s}x)) is a witness for s → t ≤ s′ → t′.

3. x is a witness for A ⊢ x: t, provided A(x) = t.

4. If M′ is a witness for A[x ← t_{1}] ⊢ M: t_{2}, then λx : t_{1}.M′ is a witness for A ⊢ (λx.M): t_{1} → t_{2}

5. If M′ is a witness for A ⊢ M: t_{1} → t_{2} and N′ is a witness for A ⊢ N: t_{1}, then M′N′ is a witness for A ⊢ (M N): t_{2}.

6. If M′ is a witness for A ⊢ M : t and C_{t,t′} is a witness for t ≤ t′, then C_{t,t′}M′ is a witness for A ⊢ M : t′

Thus the witness of a type derivation is the strongly-typed term which is obtained by “inserting the necessary coercions”. This is formalized as follows:

label{lemma1}

Lemma 1 (1) If C_{s′,s} is a witness for s′ ≤ s, then s′ ≤ s, and furthermore ⊢_{ST} C_{s′,s} : s′ → s

(2) If M′ is a witness for A ⊢ M : t, then A ⊢ M : t, and furthermore A ⊢_{ST} M′ : t.

Proof: Trivial □

label{lemma2}

Lemma 2 If M′ is a witness for A[x ← t_{1}] ⊢ M : t_{2} and N′ is a witness for A ⊢ N : t_{1}, then M′[N′/x] is a witness for A ⊢ M[N/x] : t_{2}.

Proof: By induction on the definition of the witness M′. The only interesting case is the one for subsumption. Then we have C_{u,t_{2}}M′′ is a witness for A[x ← t_{1}] ⊢ M : t_{2}, where C_{u,t_{2}} is a witness for u ≤ t_{2} and M′′ is a witness for A[x ← t_{1}] ⊢ M : u. By induction, M′′[N′/x] is a witness for A ⊢ M[N/x] : u, so M′[N′/x] ≡ (C_{u,t_{2}}M′)[N′/x] ≡ C_{u,t_{2}}(M′[N′/x]) is a witness for A ⊢ M[N/x] : t_{2}. □

4 The Main Theorem

Let us say that a set of basic subtype relations creates no functions iff whenever t ≤ t′ is a basic relation, t′ is an atomic type. For example, the partial type discipline of [4] creates no functions, nor do atomic coercions as considered in [2] or [5].

Theorem 2 If a set of basic subtype relations creates no functions, then every term typable from those relations is strongly normalizing.

Proof: We will show that if M′ is a witness for A ⊢ M : t, and M reduces to N, then there is a witness N′ for A ⊢ N : t such that M′ reduces to N′. To see that this claim is enough to prove the theorem, 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, so this is impossible.

We proceed by induction on the size of M′, or equivalently on the size of the derivation of A ⊢ M : t. If M′ is a variable, an abstraction, a subsumption, or an application that is not the redex of the reduction of M, then the claim is easy. The only case that is interesting is the case when M is the redex of the reduction, that is, we have M ≡ (λx.M_{1})M_{2} ⇒ M_{1}[M_{2}/x]. Then M′ ≡ W_{1}W_{2}, where W_{1} is a witness for A ⊢ (λx.M_{1}) : t_{1} → t and W_{2} is a witness for A ⊢ M_{2} : t_{1}. There are only two possibilities for W_{1}: it is either an abstraction or a subsumption.

1. W_{1} can be an abstraction (λx.M′_{1}), where M′_{1} is a witness for A[x ← t_{1}] ⊢ M_{1} : t. Then W_{1}W_{2} ≡ (λx.M′_{1})W_{2} ⇒ M′_{1}[W_{2}/x], which is a witness for A ⊢ M_{1}[M_{2}/x] : t, by Lemma 2.

2. W_{1} can be a subsumption C_{u,t_{1}→t}W′, where C_{u,t_{1}→t} is a witness for u ≤ t_{1} → t and W′ is a witness for A ⊢ λx.M_{1} : u. Since our coercions do not create functions, we must have u = u_{1} → u_{2}, and C_{u,t_{1}→t} ≡ C_{u_{1}→u_{2},t_{1}→t} ≡

λf : u_{1} → u_{2}.λx : t_{1}.C_{u_{2},t}(f(C_{t_{1},u_{1}}x))

So we have

M′ ≡ W_{1}W_{2}
≡ C_{u_{1}→u_{2},t_{1}→t}W′W_{2}
⇒ C_{u_{2},t}(W′(C_{t_{1},u_{1}}W_{2}))

Now W′ is a witness for A ⊢ λx.M_{1} : u_{1} → u_{2}, and C_{t_{1},u_{1}}W_{2} is a witness for A ⊢ M_{2} : u_{1}, so W′(C_{t_{1},u_{1}}W_{2}) is a witness for A ⊢ (λx.M_{1})M_{2} : u_{2}. The term W′(C_{t_{1},u_{1}}W_{2}) is smaller than M′, so we can apply the induction hypothesis to get a witness W′′ for A ⊢ M_{1}[M_{2}/x] : u_{2} such that W′(C_{t_{1},u_{1}}W_{2}) ⇒ W′′. So C_{u_{2},t}W′′ is a witness for A ⊢ M_{1}[M_{2}/x] : t and furthermore

M′ ⇒ C_{u_{2},t}(W′(C_{t_{1},u_{1}}W_{2})) ⇒ C_{u_{2},t}W′′

So C_{u_{2},t}W′′ is the desired witness, completing the proof of the claim. □

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

5 Conclusions

Acknowledgements

[[ Don’t forget these!! ]]

References

[1] Gomard, C.K. “Partial Type Inference for Untyped Functional Programs,” Proc. 1990 ACM Conf. on Lisp and Functional Programming, 282–287.

[2] Mitchell, J.C. “Type Inference with Simple Subtypes,” J. of Functional Programming 1 (1991), 245–285.

[3] Rémy, D. “Typechecking records and variants in a natural extension of ML,” Conf. Rec. 16th Ann. ACM Symp. on Principles of Programming Languages (1989), 77–88.

[4] Thatte, S. “Type Inference with Partial Types,” Proc. ICALP ’88 (1988), 615–629.

[5] Wand, M., and O’Keefe, P. “On the Complexity of Type Inference with Coercion,” Conf. on Functional Programming Languages and Computer Architecture (London, September, 1989).

[6] Wand, M. “A Semantic Prototyping System,” Proc. ACM SIGPLAN ’84 Compiler Construction Conference (1984) 213–221.