Even Normal Forms Can be Hard to Type

John C. Reynolds^{1} Carnegie Mellon University Pittsburgh, Pennslyvania 15213 U.S.A.

Extended Abstract — December 1, 1989

1. Introduction

Although type inference, in the form of the Hindley-Milner algorithm, has been successfully applied to languages with a simple type discipline, and even with a limited form of polymorphism [3], it has proved to be a refractory problem for richer type disciplines; it has been shown to be undecidable for the intersection type discipline [2, 1], and its status for the polymorphic lambda calculus [6, 5, 9] is a long-standing open question.

This circumstance has raised interest in the possibility of “partial type inference”, in which programs are required to contain some type information but less than in conventional “explicitly typed” formalisms. One plausible approach is based on the observation that programmers normally write β-redices in their “sugared” form as let definitions, and that such definitions are a natural context for providing type information. This suggests that one might require type information only in let definitions or, in terms of an unsugared language, in redices.

For example, the expression

(λH. H(λk. k × k))(λf. f(1) + f(2))

would normally be written as

let H ≡ λf. f(1) + f(2) in H(λk. k × k) ,

whose partially typed form might be

let H: (int → int) → int ≡ λf. f(1) + f(2) in H(λk. k × k) ,

1Research supported by NSF Grant CCR-8620191. A portion of the research was also sponsored by the Defense Advanced Research Projects Agency (DOD), ARPA Order No. 4976, under contract number F33615-87-C-1499, monitored by the Air Force Wright Aeronautical Laboratories, Wright-Patterson AFB, Ohio. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of any agency of the US Government.

whose desugared from is

(λH: (int → int) → int . H(λk. k × k))(λf. f(1) + f(2)) .

(This brief description is oversimplified. Actually, one requires type information in a kind of generalized redex, called a cut by Statman [11], that is the desugaring of a multiple let definition.)

However, this approach implies that no type information is needed when an expression contains no redices. Thus its feasibility requires that full type inference be feasible for normal forms. (Throughout this paper, we use “redex” and “normal form” to mean “β-redex” and “β-normal form”.) The importance of type inference for normal forms is also suggested by recent work in [10, 4].

The problem of type inference for normal forms will be examined in this paper for the intersection type discipline and for the polymorphic lambda calculus. In the first case we will show that the problem is PSPACE-hard, in the second case we will show that it is just as hard as the type inference problem for arbitrary expressions.

2. Intersection Types

In the intersection type discipline [2, 1], the set of types can be defined by the abstract grammar

θ ::= ρ | ω | θ → θ | θ & θ

where ρ ranges over some set of primitive types and ω is a particular “nonsense” type.

A type assignment is a function from a finite set of variables into types. A typing is a formula π ⊢ e : θ, where π is a type assignment, e is an expression of the untyped lambda calculus, and θ is a type. Intuitively, π ⊢ e : θ asserts that the expression e has the type θ when its free variables are assigned types by π.

A typing is valid if and only if it can be proved from the following inference rules:

• Variables

\overline{π ⊢ x : π(x)} when x ^{∈} dom π

• Arrow Introduction

\frac{[ π | x: θ] ⊢ e : θ′}{π ⊢ (λx. e) : θ → θ′}

• Arrow Elimination

π ⊢ e_{1} : θ → θ′
π ⊢ e_{2} : θ
π ⊢ e_{1} e_{2} : θ′

• Nonsense

\overline{π ⊢ e : ω}

• Intersection Introduction

\begin{matrix}π ⊢ e : θ_{1} \\ π ⊢ e : θ_{2} \\ π ⊢ e : θ_{1} & θ_{2} \end{matrix}

• Intersection Elimination

\frac{π ⊢ e : θ_{1} & θ_{2}}{π ⊢ e : θ_{1}}  \frac{π ⊢ e : θ_{1} & θ_{2}}{π ⊢ e : θ_{2}}

In the rule for arrow introduction, [ π | x: θ] denotes the type assignment whose domain is dom π ∪ {x}, such that [ π | x: θ]x = θ and [ π | x: θ]x′ = πx′ when x′ ≠ x.

Proposition 1 For the intersection type discipline, deciding the validity of π ⊢ e : θ, where e is in normal form, is PSPACE-hard.

The proof is obtained by reducing the problem of evaluating quantified Boolean expressions, which is known to be PSPACE-complete [7], to the type inference problem. The reduction is obtained by translating a quantified Boolean expression B into a lambda expression B^{∗} as follows:

(B_{1} ∧ B_{2})^{∗} = and B_{1}^{∗} B_{2}^{∗}
(B_{1} ∨ B_{2})^{∗} = or B_{1}^{∗} B_{2}^{∗}
(¬B)^{∗} = not B^{∗}
((∀x)B)^{∗} = forall(λx. B^{∗})
((∃x)B)^{∗} = exists(λx. B^{∗})
x^{∗} = x ,

where and, or, not, forall, and exists are variables not occurring in the original expression. In addition a truth value b is translated into a type b^{∗} by

true^{∗} = t false^{∗} = f ,

where t and f are distinct types, each of which is either primitive or of the form θ_{1} → θ_{2}. Then B evaluates to b under a truth-value assignment β if and only if π ⊢ B^{∗} : b^{∗} is valid, where π is the type assignment that maps each variable x occurring free in B into (βx)^{∗} and maps the additional variables of B^{∗} as follows:

π(and) = (f → (f → f)) & (f → (t → f)) & (t → (f → f)) & (t → (t → t))
π(or) = (f → (f → f)) & (f → (t → t)) & (t → (f → t)) & (t → (t → t))

π(not) = (f → t) & (t → f)

π(forall) = (((f → f) & (t → f)) → f) & (((f → f) & (t → t)) → f)

&(((f → t) & (t → f)) → f) & (((f → t) & (t → t)) → t)

π(exists) = (((f → f) & (t → f)) → f) & (((f → f) & (t → t)) → t)

&(((f → t) & (t → f)) → t) & (((f → t) & (t → t)) → t) .

Although Proposition 1 deals with the problem of type inference, a similar result holds for type checking, at least for one view of what constitutes explicit typing. In [8], an explicitly typed version of the lambda calculus with intersection types is obtained by replacing the rule for arrow introduction by

• Explicitly Typed Arrow Introduction

\frac{[ π | x: θ_{i}] ⊢ e : θ′}{π ⊢ (λx: θ_{1},…, θ_{n}. e) : θ_{i} → θ′}

which limits the types assigned to a bound variable to members of a list stated explicitly in the binding expression. It is easily seen that Proposition 1 continues to hold for this variant of the lambda calculus; one simply replaces λx. by λx: f, t. in the translations of quantified Boolean expressions.

3. The Polymorphic Lambda Calculus

In the polymorphic lambda calculus [6, 5, 9], the set of types is defined by

θ ::= ρ | τ | θ → θ | ∀τ. θ

where ρ ranges over some set of primitive types and τ ranges over a denumerably infinite set of type variables. Type assignments and typings are defined as before.

A typing is valid if and only if it can be proved from the following inference rules:

• Variables

\overline{π ⊢ x : π(x)} when x ^{∈} dom π

• Arrow Introduction

\frac{[ π | x: θ] ⊢ e : θ′}{π ⊢ (λx. e) : θ → θ′}

• Arrow Elimination

π ⊢ e_{1} : θ → θ′
π ⊢ e_{2} : θ
π ⊢ e_{1} e_{2} : θ′

• Quantifier Introduction

\frac{π ⊢ e : θ}{π ⊢ e : ∀τ. θ} when τ not free in πx for any x ^{∈} dom π

• Quantifier Elimination

\frac{π ⊢ e : ∀τ. θ}{π ⊢ e : (θ/τ → θ′)}

In the last rule, (θ/τ → θ′) denotes the result of substituting θ′ for the free occurrences of τ in θ, with renaming of type variables when necessary. Note that, since the expressions e contain no type information, we are dealing with the implicitly typed polymorphic lambda calculus.

Proposition 2 For the implicitly typed polymorphic lambda calculus, deciding the validity of π ⊢ e : θ, where e is in normal form, is just as hard as deciding the validity of π ⊢ e : θ for arbitrary e.

The proof is obtained by reducing the type inference problem for arbitrary expressions to the type inference problem for normal forms. Suppose e is an arbitrary expression, i is an identifier not occurring in e, and e^{∗} is obtained from e by replacing each redex (λx. e_{1})e_{2} by (i(λx. e_{1}))e_{2}. Then e^{∗} is in normal form, and π ⊢ e : θ is valid if and only if

[ π | i: ∀τ. (τ → τ) ] ⊢ e^{∗} : θ

is valid.

Acknowledgements The author wishes to thank Mark Lillibridge for pointing out that the evaluation of quantified Boolean expressions is PSPACE-complete.

References

[1] Coppo, M., Dezani-Ciancaglini, M., Honsell, F., and Longo, G. Extended Type Structures and Filter Lambda Models. in: Logic Colloquium ’82, Florence, Italy, August 23–28, 1982, edited by G. Lolli, G. Longo, and A. Marcja. Studies in Logic and the Foundations of Mathematics, vol. 112, North-Holland, Amsterdam, 1984, pp. 241– 262.

[2] Coppo, M., Dezani-Ciancaglini, M., and Venneri, B. Functional Characters of Solvable Terms. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 27 (1981), pp. 45–58.

[3] Damas, L. and Milner, R. Principal Type-Schemes for Functional Programs. in: Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico, January 25–27. 1982, pp. 207–212.

[4] Giannini, P. and Ronchi Della Rocca, S. Characterization of Typings in Polymorphic Type Discipline. in: Proceedings Third Annual Symposium on Logic in Computer Science, Edinburgh, Scotland, July 5–8. 1988, pp. 61–70.

[5] Girard, J.-Y. Interprétation Fonctionnelle et Élimination des Coupures de l’Arithmétique d’Ordre Supérieur, Thèse de doctorat d’état. Université Paris VII, June 1972.

[6] Girard, J.-Y. Une Extension de l’Interprétation de Gödel à l’Analyse, et son Application à l’Élimination des Coupures dans l’Analyse et la Théorie des Types. in: Proceedings of the Second Scandinavian Logic Symposium, University of Oslo, June 18– 20, 1970, edited by J. E. Fenstad. Studies in Logic and the Foundations of Mathematics, vol. 63, North-Holland, Amsterdam, 1971, pp. 63–92.

[7] Hopcroft, J. E. and Ullman, J. D. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading, Massachusetts, 1979, x+418 pp.

[8] Reynolds, J. C. Preliminary Design of the Programming Language Forsythe. Report, no. CMU–CS–88–159, Carnegie Mellon University, Computer Science Department, June 21, 1988.

[9] Reynolds, J. C. Towards a Theory of Type Structure. in: Programming Symposium, Proceedings, Colloque sur la Programmation, Paris, April 9–11, edited by B. Robinet. Lecture Notes in Computer Science, vol. 19, Springer-Verlag, Berlin, 1974, pp. 408– 425.

[10] Ronchi Della Rocca, S. Principal Type Scheme and Unification for Intersection Type Discipline. Theoretical Computer Science, vol. 59 (1988), pp. 181–209.

[11] Statman, R. Normal Varieties of Combinators. Report, no. 89–61, Carnegie Mellon University, Department of Mathematics, October 1989.