Search code examples
haskelltypesocamlexistential-typeparametric-polymorphism

What are type quantifiers?

Many statically typed languages have parametric polymorphism. For example in C# one can define:

T Foo<T>(T x){ return x; }

In a call site you can do:

int y = Foo<int>(3);

These types are also sometimes written like this:

Foo :: forall T. T -> T

I have heard people say "forall is like lambda-abstraction at the type level". So Foo is a function that takes a type (for example int), and produces a value (for example a function of type int -> int). Many languages infer the type parameter, so that you can write Foo(3) instead of Foo<int>(3).

Suppose we have an object f of type forall T. T -> T. What we can do with this object is first pass it a type Q by writing f<Q>. Then we get back a value with type Q -> Q. However, certain f's are invalid. For example this f:

f<int> = (x => x+1)
f<T> = (x => x)

So if we "call" f<int> then we get back a value with type int -> int, and in general if we "call" f<Q> then we get back a value with type Q -> Q, so that's good. However, it is generally understood that this f is not a valid thing of type forall T. T -> T, because it does something different depending on which type you pass it. The idea of forall is that this is explicitly not allowed. Also, if forall is lambda for the type level, then what is exists? (i.e. existential quantification). For these reasons it seems that forall and exists are not really "lambda at the type level". But then what are they? I realize this question is rather vague, but can somebody clear this up for me?

A possible explanation is the following:

If we look at logic, quantifiers and lambda are two different things. An example of a quantified expression is:

forall n in Integers: P(n)

So there are two parts to forall: a set to quantify over (e.g. Integers), and a predicate (e.g. P). Forall can be viewed as a higher order function:

forall n in Integers: P(n) == forall(Integers,P)

With type:

forall :: Set<T> -> (T -> bool) -> bool

Exists has the same type. Forall is like an infinite conjunction, where S[n] is the n-th elemen to of the set S:

forall(S,P) = P(S[0]) ∧ P(S[1]) ∧ P(S[2]) ...

Exists is like an infinite disjunction:

exists(S,P) = P(S[0]) ∨ P(S[1]) ∨ P(S[2]) ...

If we do an analogy with types, we could say that the type analogue of ∧ is computing the intersection type ∩, and the type analogue of ∨ computing the union type ∪. We could then define forall and exists on types as follows:

forall(S,P) = P(S[0]) ∩ P(S[1]) ∩ P(S[2]) ...
exists(S,P) = P(S[0]) ∪ P(S[1]) ∪ P(S[2]) ...

So forall is an infinite intersection, and exists is an infinite union. Their types would be:

forall, exists :: Set<T> -> (T -> Type) -> Type

For example the type of the polymorphic identity function. Here Types is the set of all types, and -> is the type constructor for functions and => is lambda abstraction:

forall(Types, t => (t -> t))

Now a thing of type forall T:Type. T -> T is a value, not a function from types to values. It is a value whose type is the intersection of all types T -> T where T ranges over all types. When we use such a value, we do not have to apply it to a type. Instead, we use a subtype judgement:

id :: forall T:Type. T -> T
id = (x => x)

id2 = id :: int -> int

This downcasts id to have type int -> int. This is valid because int -> int also appears in the infinite intersection.

This works out nicely I think, and it clearly explains what forall is and how it is different from lambda, but this model is incompatible with what I have seen in languages like ML, F#, C#, etc. For example in F# you do id<int> to get the identity function on ints, which does not make sense in this model: id is a function on values, not a function on types that returns a function on values.

Can somebody with knowledge of type theory explain what exactly are forall and exists? And to what extent is it true that "forall is lambda at the type level"?

Solution

  • Let me address your questions separately.

    • Calling forall "a lambda at the type level" is inaccurate for two reasons. First, it is the type of a lambda, not the lambda itself. Second, that lambda lives on the term level, even though it abstracts over types (lambdas on the type level exist as well, they provide what is often called generic types).

    • Universal quantification does not necessarily imply "same behaviour" for all instantiations. That is a particular property called "parametricity" that may or may not be present. The plain polymorphic lambda calculus is parametric, because you simply cannot express any non-parametric behaviour. But if you add constructs like typecase (a.k.a. intensional type analysis) or checked casts as a weaker form of that, then you loose parametricity. Parametricity implies nice properties, e.g. it allows a language to be implemented without any runtime representation of types. And it induces very strong reasoning principles, see e.g. Wadler's paper "Theorems for free!". But it's a trade-off, sometimes you want dispatch on types.

    • Existential types essentially denote pairs of a type (the so-called witness) and a term, sometimes called packages. One common way to view these is as implementation of abstract data types. Here is a simple example:

      pack (Int, (λx. x, λx. x)) : ∃ T. (Int → T) × (T → Int)

      This is a simple ADT whose representation is Int and that only provides two operations (as a nested tuple), for converting ints in and out of the abstract type T. This is the basis of type theories for modules, for example.

    • In summary, universal quantification provides client-side data abstraction, while existential types dually provides implementor-side data abstraction.

    • As an additional remark, in the so-called lambda cube, forall and arrow are generalised to the unified notion of Π-type (where T1→T2 = Π(x:T1).T2 and ∀A.T = Π(A:*).T) and likewise exists and tupling can be generalised to Σ-types (where T1×T2 = Σ(x:T1).T2 and ∃A.T = Σ(A:*).T). Here, the type * is the "type of types".