What terms type systems exclude?

Question

I understand type systems like the simply typed lambda calculus, system F and the calculus of constructions include a different subset of all lambda terms. But what, precisely, are the terms each of those systems include/exclude? Is it possible to express the intuition behind the criteria with words?

Answer 1

In the simply-typed lambda calculus, the type of a function must be fully specified, even when it's irrelevant. A trivial example is the identity function: in the lambda calculus, it's $\lambda x.x$; in the simply-typed lambda calculus, there isn't a single identity function but rather a family of identity functions $\lambda x:T. x$ for every type $T$. This means that the simply-typed lambda calculus has no polymorphism. If you think about data structures, more concrete examples come up — you can't write, say, a generic function like list reversal, you have to write it all over again for each type of list elements. You can't even write basic primitives like nil and cons, only typed-indexed primitives $\texttt{nil}_T$ and $\texttt{cons}_T$.

To give a concrete example in the pure lambda-calculus (without constants), natural numbers can be encoded as Church numerals in the untyped lambda calculus: $$\begin{align} 0 &= \lambda f. \lambda x. x \\ 1 &= \lambda f. \lambda x. f x \\ 2 &= \lambda f. \lambda x. f (f x) \\ &\ldots \end{align}$$ In the simply-typed lambda calculs, there is a separate family of Church numerals for each type: $$\begin{align} 0_T &= \lambda f : T\to T. \lambda x : T. x \\ 1_T &= \lambda f : T\to T. \lambda x : T. f x \\ 2_T &= \lambda f : T\to T. \lambda x : T. f (f x) \\ &\ldots \end{align}$$ You can't compose Church numerals of different types, which makes it difficult to use the same number for different things.

In the Hindley-Milner type system (which I'm including because it's an important step), polymorphic functions are possible, but with restrictions. Hindley-Milner requires a new syntactic form in addition to variables, application and abstraction: the let binding $\texttt{let } x = M \texttt{ in } N$. If all or part of the type of $M$ is irrelevant then it can be left as a variable, and the variable $x$ has not a type but a type scheme of the form $\forall \alpha_1,\ldots,\alpha_k, T$ where the $\alpha_i$ are type variables and the type expression $T$ can contain these variables. For example, it is possible to define the identity function once and for all: $$ \texttt{let } \texttt{id} : (\forall \alpha, \alpha\to\alpha) = (\lambda x:\alpha. x) \texttt{ in } \ldots $$ Similarly one can define Church numerals and (more practically) data structure manipulation (e.g. of lists, arrays, etc.) without having to duplicate the definitions for every type of element.

This form of polymorphism is known as parametric polymorphism; HM does not allow functions to behave differently depending on the types of their arguments. This allows proving properties of programs, such as “a function of type $\forall \alpha, \texttt{list}(\alpha) \to \texttt{int}$ only depends on the length of the list and not on the value of the elements”. This is known as “theorems for free” after the famous paper by Phil Wadler. An example of a practically useful function that cannot be expressed in HM is $\ge : \forall \alpha, \alpha \to \alpha \to \texttt{bool}$ which defines a total order — by parametricity, any such function is consant or non-terminating. More generally, HM cannot express ad hoc polymorphism (also known as generic programming in type theoretist circles, but beware that “generics” means parametric polymorphism in OOP circles).

In System F, functions can be parametrically polymorphic with no restrictions. Any lambda term can have universal quantifiers on types, which removes the distinction between $\lambda$ and $\texttt{let}$. Ad hoc polymorphism is still impossible (parametricity results still hold). System F allows more polymorphism than HM, at the expense of type inference (which is relatively easy for HM, and undecidable in System F).

Above I gave examples of programs that can't be expressed in HM and can't be expressed in System F either. Let me now give examples of programs that can be expressed in System F but not in HM. Simple examples are a bit more subtle. One simple example is the lambda term $\lambda x. x \, x$. What does it take to type it? In order for $\lambda x:T. x\,x$ to be well-typed, $T$ must satisfy the equations $T = T_1 \to T_2$ (for the occurrence of $x$ in function position) and $T_1 = T$ (for the occurrence of $x$ in application position). In Hindley-Milner, this is impossible, because types have a simple tree structure and a type satisfying these equations would have to be infinite. In System F, this term can be typed by breaking the recursion with a type abstraction: $$ \Delta_F = \lambda x: (\forall \alpha, \alpha\to\alpha). x \, (\forall \alpha, \alpha\to\alpha) \, x $$ While this may look of theoretical interest only, this is of highly practical interest when generalized to data structures. The term $\Delta$ condenses the wish for a single object to behave in a polymorphic way. System F, unlike HM, can express objects with polymorphic methods.

Besides ad hoc polymorphism, an important class of terms that still cannot be typed in System F is non-terminating functions. While $\Delta = \lambda x. x \, x$ can be typed in System F, the “utmost” non-terminating term $\Delta \Delta$ cannot be typed.

System F expands the simply-typed lambda calculus by adding terms depending on types. Other directions for expansion are types depending on types, and types depending on terms. These three dimensions for expansion are known as the Barendregt cube or lambda cube. (This should actually be a hypercube, but the lambda calculus itself is built on terms depending on terms, and the half of the hypercube that doesn't have terms depending on terms isn't studied often.)

Types depending on types allow generic data structures to be defined. For example, although HM is sufficient to write polymorphic functions on lists, defining a list type operator requires more than a basic Hindley-Milner or System F type system: it requires the ability to parametrize the types of lists by the type of their elements.

Types depending on terms are known as dependent types. Dependent types are very powerful, at the expense of making type checking more difficult and requiring often large annotations. An example of constraint that requires dependent types is tracking array lengths through a type family $\texttt{array} : \mathsf{Type} \to \mathbb{N} \to \mathsf{Type}$, allowing the typing of functions such as $$ \texttt{concatenate}_T : \forall n:\mathbb{N}, \forall m:\mathbb{N}, \texttt{array}\,T\,n \to \texttt{array}\,T\,m \to \texttt{array}\,T\,(n+m) $$

The calculus of constructions includes all possible abstractions (terms depending on terms or types, types depending on terms or types). Even in the calculus of constructions, neither ad hoc polymorphism nor non-terminating functions are possible.

Answer 2

One such excluded term is the $Y$ combinator: $ (\lambda f . (\lambda x . f (x x) (\lambda y . f (y y))$. Intuition says that that this has type $(a \rightarrow a) \rightarrow a$, but the intermediate terms can't be assigned proper type values using Hindley-Milner types (I'm not sure about more powerful systems).

The intuition I have for what terms are excluded is: terms which would result in a type-error, and terms which wouldn't result in a type error, but for which the proof that there is no error can't be expressed in the type system.

For example, the term $(\lambda f . (f \ 3) + (f\ False))(\lambda x . 5)$ can be evaluated without any type errors. With higher-rank types, we can give the first function the type $(\forall a \to Int ) \to Int$, and the second one type $\forall a \to Int$, and the program will typecheck. But in normal Hindley-Miller types, there's no way to express that that the parameter $f$ takes any type to an $Int$, so this term is excluded.

In general, it has to do with the expressiveness of the type system, and it's ability to prove whether a program is safe. I also suspect that Godel's results come into play here: there are statements which are true that cannot be proven. I'm willing to bet that in many cases, these correspond to untyped lambda terms which are type-safe, but for which no proof of safety exists in stronger type systems.