Parametricity and variants of Girard’s J operator

Robert Harper  John Mitchell

December 30, 1994

1 Introduction

The impredicative polymorphic lambda calculus, or System F [Gir71, Gir72, Rey74], is generally recognized as a calculus of parametric polymorphism [Rey74, Rey83, Rey84, BFSS89, FGSS88, MS93]. Intuitively, this means that the polymorphic functions definable in the language must use the same algorithm at all types. There are no non-parametric functions such as a single multiplication function that computes an inner product on vectors, ordinary product on natural numbers and similar or unrelated “products” on other types.

In his 1971 paper, Girard discusses parametricity in System F and gives an example showing that if we add a non-parametric operator to the calculus, normalization fails [Gir71]. This example has been interpreted as a demonstration that System F is inherently a calculus of parametric functions. Specifically, since adding a non-parametric operator alters a fundamental property of the system, we can conclude the System F is inherently parametric. However, this interpretation of the example relies on the implicit assumption that J is as simple a non-parametric operator as possible. If it is possible to add a simpler non-parametric operator to System F in a manner that preserves strong normalization, we could not really say that Girard’s example convincingly demonstrates the parametric nature of System F. In this short note, we give some variants of Girard’s example, hoping to more clearly identify the kind of non-parametric operations that invalidate normalization. In the concluding remarks, we observe that impredicativity appears essential.

One possible reservation regarding Girard’s example is that it combines non-parametric functions with a change in the typing properties of the language. More specifically, the type of J is ∀s.∀t.s → t, which is not the type of any pure closed term of System F since it is not a provable propositional formula. The non-normalizing term constructed using J also seems to require a term 0: ∀t.t. Again, there are no pure closed terms with type ∀t.t. This led us to formulate the following question:

Is there a simple non-parametric operator Op : σ such that

(i) there exist pure closed terms of type σ, and

(ii) adding Op to System F causes normalization to fail?

We settle this question affirmatively and give a simple example, J′. Our goal is to dispel the possible misconception that in impredicative systems, Girard’s example is simply a “typing trick” that could not be carried out with other non-parametric operations.

One consequence of replacing J by an operator whose type already contains pure closed terms is that we can easily show that the fixed-point operator is not definable. More specifically, suppose Op : σ and there exists a pure closed term of type σ. Then using the formulas-as-types analogy [How80], we can show that there exists a closed term of type τ containing Op iff there exists a pure closed term of type τ not containing Op. The argument is simply that if we add a new axiom for a formula that is already provable, we do not change the set of provable formulas. Since ∀t.(t → t) → t is not a provable formula of intuitionistic logic, there is no pure closed term of this type. It follows that when the type of Op contains pure closed terms, no closed term of type ∀t.(t → t) → t is definable from Op. In particular, since the fixed-point operator Y has this type, Y is not definable from J′. In light of various studies relating logical paradoxes and fixed-point operators [MR86, Coq86, CH94], it does not seem easy to establish that no fixed-point operator or “looping combinator” (see [MR86, CH94]) is definable from J.

2 Review of Girard’s J example

Girard’s example adds two constants to System F, each with associated reduction rules. The first is a constant 0: ∀t.t which allows us to choose an element of each type, by application. The intent is that 0 is a form of choice function that selects elements of different types “harmoniously.” Perhaps the simplest way of understanding this is to recall that in Girard’s realizability-like model, HEO_{2} [Tro73, Gir72], the natural number 0 codes the constant function 0 and therefore provides an element of all types. This explains the use of the symbol “0” and also the following associated reduction rules:

\begin{aligned}0 (σ → τ) M & → & 0 τ \\ 0 (∀t.σ) τ & → & 0 [τ/t]σ \end{aligned}

While Girard’s nonterminating term requires a constant with type ∀t.t, the reduction rules are not needed.

Intuitively, J produces a choice function by combining 0 with an element M: σ of some particular type. The resulting choice function λt. J t σ M selects element M of type σ and element 0 τ of any type τ different from σ. The constant J : ∀s.∀t.s → t has reduction rules

JστM → \{ \begin{matrix}M & if σ = τ \\ 0 τ & otherwise \end{matrix}

Girard does not specify whether types σ and τ in this reduction rule may contain free variables. However, the system becomes inconsistent and non-confluent if we allow arbitrary types in both forms of reduction, as illustrated below. We therefore restrict the reduction JστM → 0 τ to the case where σ and τ are distinct closed type expressions.

Intuitively, the problem with types that contain free variables is that these variables may be formal parameters of some function. If σ and τ are not syntactically identical, but have a common substitution instance, then application of the enclosing function may change the applicable J - reduction rule. For example, the term

(λt. J s t x) s

with x: s reduces to two normal forms, x and 0 s. The first reduction begins with the outermost β -reduction (substituting s for t):

(λt. J s t x) s → J s s x → x

The second reduction applies J -reduction first, while the type arguments are different:

(λt. J s t x) s → (λt. 0 t) s → 0 s

Clearly this is inconsistent, since x = (λt. J s t x) s = 0 s implies that all elements of type s (which is arbitrary) are equal to 0 s.

Using J, we can give a form of the self-application function λx. xx an unexpected type. More specifically, let D be the term

D =^{def} λx: ∀t.t. (x ∀t.t) x

and note that the term

X =^{def} λt. J ((∀t.t) →(∀t.t)) t D

has type ∀t.t. It is easy to check that Z =^{def} X ((∀t.t) →(∀t.t)) X reduces to itself, proving that the extension of System F with 0 and J is non-normalizing.

Although it is difficult to characterize the “main idea” behind the term Z with much accuracy, one explanation of the construction is that the type ∀s.∀t.s → t of J allows us to hide D inside a term of type ∀t.t. This unexpected type for D allows us to apply D to itself. In this sense, one might wonder whether the unusual types of 0 and J are partly responsible for the nontermination of reduction. After all, if we add a constant c: ∀t.t with reduction rule

c ((∀t.t) →(∀t.t)) → D

then it is clear that c ((∀t.t) →(∀t.t)) c does not normalize. While c has the essential reduction behavior of X above, c does not in any way seem to be “nonparametric.”

3 Alternative non-parametric primitives

A relatively natural non-parametric operation is an equality test on types. This might take the form of a term

EqTest : ∀s. ∀t. Bool

with EqTest σ τ = true if σ and τ are the same type, and false otherwise. If this test is going to be useful, however, we would want to write expressions such as

λx: s. λy: t. if EqTest s t then x else y

Intuitively this expression has type s → t → t. If types s and t are equal, then the result x has type s = t and otherwise the result y has type t. However, we cannot obtain this typing without using the equation s = t in typing the first arm of the conditional. If we focus on this combination of equality test and conditional expression, we are led to consider a type-conditional operation TypeCond with the slightly unusual typing rule

(TypeCond)  \frac{Γ, σ = τ ▷ M : ρ Γ ▷ N : ρ}{Γ ▷ TypeCond σ τ M N : ρ}

Intuitively, this rule says that if M has type ρ under the assumption that σ = τ, and N has type ρ without this assumption, then TypeCond σ τ M N has type ρ. Since we will only be interested in simple examples illustrating the main ideas, we will not need to formalize typing with equality assumptions in contexts. We show that normalization fails with TypeCond and then give a simpler but less intuitive primitive that does involve type equations.

The reduction rules for TypeCond are

TypeCond σ σ M N → M
TypeCond σ τ M N → N  σ τ distinct, closed

One way of understanding TypeCond is to consider writing a function that does multiplication on natural numbers and a component-wise multiplication on pairs of natural numbers. In other words, we would like to combine functions

mult_{N}  =^{def} λx: nat. λy: nat. x ∗ y
: nat → nat → nat
mult_{N,N} =^{def} λx: nat × nat. λy: nat × nat.⟨π_{1}x ∗ π_{1}y, π_{2}x ∗ π_{2}y⟩
: nat × nat → nat × nat → nat × nat

where π_{i}: nat × nat → nat are the projection functions on natural number pairs. We can do this with TypeCond by writing

mult =^{def} λs. λx: s. λy: s.

TypeCond s nat (mult_{N}xy)

TypeCond s (nat × nat) (mult_{N,N}xy)

x
: ∀t. t → t → t

The function mult takes arguments x and y of the same type. If the type is nat , the result is mult_{N}xy, else if the type is nat × nat , the result is mult_{N,N}xy, else the result is x. Since we obtain a result of the right type in any case, it is semantically sensible to give mult type ∀t. t → t → t. We cannot seem to define mult using J instead. The problem is that TypeCond provides an “if-then-else” test for type equality, while J is only an “if-then” test, with the “else” case defaulting to 0.

Using a variant of Girard’s example, we can show that TypeCond destroys strong normalization. Consider the term

X =^{def} λs. λx: s. TypeCond σ s (xσx) x

where σ = ∀t. t → t. It should be clear from the basic properties of TypeCond that X: σ. Using the first reduction associated with TypeCond, we have

XσX → → TypeCond σ σ (XσX) X → → XσX

This shows that strong normalization fails with this form of type conditional operation. A technical point is that in constructing X, we only need to vary the second type argument to TypeCond. Therefore, it would suffice to have a weaker primitive TypeCond_{σ} : ∀t. σ → t → t for the specific type σ identified above.

Intuitively, TypeCond seems to give us the expressive power of J, without requiring a “universal choice function” 0. We justify this intuition by showing that using polymorphic constant 0: ∀t.t, we can define Girard’s J operator from TypeCond as follows:

J =^{def} λs. λt. λx: s. TypeCond s t x (0 t)

A remaining reservation that one might have about TypeCond is the unusual typing rule using type equations. We therefore conclude with a variant of J that does not require 0 or type equations. Essentially, J′ is a restriction of J to function types, using the polymorphic identity in place of 0. More concretely, let J′: ∀s.∀t.(s → s) →(t → t) be a constant. We base the reduction rules for J′ on the term

λs. λt. TypeCond s t (λx: s → s. x) (λx: s → s. λy: t. y)

which could be taken as the definition of J′ from TypeCond. We can understand the type of J′ by noting that if s = t, then λx: s → s. x : (s → s) →(t → t). Since we have λx: s → s. λy: t. y : (s → s) →(t → t) in any case, J′ has the specified type.

The reduction rules for J′ are

J σ σ M → M
J σ τ M → Id τ  σ, τ distinct, closed

where Id =^{def} λt. λy: t. y. We can carry out Girard’s example by letting ρ =^{def} ∀t. t → t and letting X: ρ be the term

X =^{def} λt. J′ ρ t (λx: ρ. xρx)

Note that λx: ρ. xρx has type ρ → ρ and hence X has type ρ. Finally, XρX has type ρ and reduces to XρX. Therefore J′ causes normalization to fail.

4 Concluding remarks

Girard’s choice function 0: ∀t.t and non-parametric operator J: ∀s.∀t.s → t cause the strongly normalizing System F of impredicative polymorphic lambda calculus to become non-normalizing. This provides one form of evidence that System F is inherently parametric. In this note, we show that “weaker” forms of non-parametricity still cause the system to be non-normalizing. The technical difference between Girard’s original example and our TypeCond or J′ is that the latter do not change the set of types that contain closed terms. A consequence of this weak form of conservativity is an easy proof that no polymorphic fixed-point or looping combinator of type ∀t.(t → t) → t can be defined from TypeCond or J′. However, it is possible that a fixed-point combinator of type (Nat → Nat) → Nat , for example, where Nat =^{def} ∀t.(t → t) → t → t is the type of Church numerals, could be defined from TypeCond or J′.

The non-parametric operators discussed in this short note are related to two other non-parametric primitives in the literature. The first is the typecase construct, associated with the type Dynamic [ACPP91, ACP^{+} 92], which provides a multi-way conditional comparison on types. As pointed out by Abadi, et al. [ACPP91], a fixed point combinator of a specific type such as ((Nat → Nat) →(Nat → Nat)) →(Nat → Nat) is definable in the simply-typed λ-calculus enriched with the type Dynamic. Since we may regard the type Dynamic as an abbreviation for the quantified type ∃t.t (itself an abbreviation for a type involving only universal quantifiers), the existence of fixed point combinators may be traced to the combination of non-parametric polymorphism and impredicative quantified types. In particular, the definition of a fixed-point operator involves embedding functions of type Dynamic → T → U into type Dynamic, which would not be allowed if Dynamic were considered a different class of type from the types T and U where we wish to construct a fixed point.

In a second use of non-parametricity, Harper and Morrisett [HM95] consider a generalization of the typecase construct, called typerec, for performing “intensional analysis” of types at run-time and compile-time. The typerec operator generalizes typecase to a form of primitive recursion on type expressions, rather than simple case analysis. However, the surrounding language is limited to predicative polymorphism, restricting intensional analysis to unquantified types. Consequently, the strong normalization property for pure terms holds and it is impossible to define a fixed-point operator from typerec.

References

[ACP^{+} 92] M. Abadi, L. Cardelli, B. Pierce, G. Plotkin, and D. Rèmy. Dynamic typing in polymorphic languages. In Proceedings of the ACM SIGPLAN Workshop on ML and its Applications, San Francisco, June 1992. ACM.

[ACPP91] M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin. Dynamic typing in a statically typed language. ACM Transactions on Programming Languages and Systems, 13(2):237–268, April 1991.

[BFSS89] E.S. Bainbridge, P.J. Freyd, A. Scedrov, and P.J. Scott. Functorial polymorphism. Theoretical Computer Science, 70:35–64, 1989. Corrigendum ibid., 71:431, 1990. Preliminary report in Logical Foundations of Functional Programming, ed. G. Huet, Addison-Wesley (1990) 315–327.

[CH94] T. Coquand and H. Herbelin. A-translation and looping combinators in pure type systems. J. Functional Programming, 4(1):77–88, 1994.

[Coq86] T. Coquand. An analysis of Girard’s paradox. In Proc. IEEE Symp. on Logic in Computer Science, pages 227–236, June 1986.

[FGSS88] P. Freyd, J.-Y. Girard, A. Scedrov, and P.J. Scott. Semantic parametricity in polymorphic lambda calculus. In Proc. IEEE Symp. on Logic in Computer Science, pages 274–279, July 1988.

[Gir71] J.-Y. Girard. Une extension de l’interpretation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types. In J.E. Fenstad, editor, 2nd Scandinavian Logic Symposium, pages 63–92. North-Holland, Amsterdam, 1971.

[Gir72] J.-Y. Girard. Interpretation fonctionelle et elimination des coupures de l’arithmetique d’ordre superieur. These D’Etat, Universite Paris VII, 1972.

[HM95] R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In Proc. 22nd ACM Symp. on Principles of Programming Languages, page to appear, January 1995.

[How80] W. Howard. The formulas-as-types notion of construction. In To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pages 479–490. Academic Press, 1980.

[MR86] A.R. Meyer and M.B. Reinhold. Type is not a type. In Proc. 13th ACM Symp. on Principles of Programming Languages, pages 287–295, January 1986.

[MS93] J.C. Mitchell and A. Scedrov. Notes on sconing and relators. In E. Boerger et al., editor, Computer Science Logic ’92, Selected Papers, pages 352–378. Springer LNCS 702, 1993. Available by anonymous ftp from host ftp.cis.upenn.edu and the file pub/papers/scedrov/rel.dvi.

[Rey74] J.C. Reynolds. Towards a theory of type structure. In Paris Colloq. on Programming, pages 408–425, Berlin, 1974. Springer-Verlag LNCS 19.

[Rey83] J.C. Reynolds. Types, abstraction, and parametric polymorphism. In Information Processing ’83, pages 513–523. North-Holland, Amsterdam, 1983.

[Rey84] J.C. Reynolds. Polymorphism is not set-theoretic. In Proc. Int. Symp. on Semantics of Data Types, Sophia-Antipolis (France), pages 145–156, Berlin, 1984. Springer LNCS 173.

[Tro73] A.S. Troelstra. Mathematical Investigation of Intuitionistic Arithmetic and Analysis. Springer LNM 344, Berlin, 1973.