Type-Level Abstraction: System Fω

In System F, types got a quantifier: forall α. α -> α, one term typed at every type at once. It bought polymorphism, parametricity, theorems for free, and Girard's normalization proof. It also left a small dishonesty in place, and this is where we make it honest.

Every time we wrote List α, we were abbreviating a type expression: the Church encoding forall β. (α -> β -> β) -> β -> β. We called the abbreviation List and treated it as a function on types: feed it α, get a type back. But that function lived in the prose around the calculus. F can write the expansion for any specific α; F cannot name List itself, as a thing separate from its argument. Pair, Tree, Maybe, Either. Every parameterized type is the same story: an abbreviation in the meta-language, a function on types we had no way to write down. The fix is one missing rule.

Kinds#

Add the rule by going up a level. Types classify values: 0 : Nat, true : Bool. Ask the same question one floor up: what classifies types? Nat is a type. Bool is a type. List on its own is not a type; List of something is.

So introduce a second grammar. A kind is what a type has. Nat and Bool have kind Type. List takes a type and returns a type, so it has kind Type -> Type. Pair takes two, Type -> Type -> Type. A type whose kind is Type -> … is a type constructor, the word you'll hear for List, Pair, Maybe, anything parameterized. The grammar of kinds is tiny: a kind is either Type or one kind arrow another. Every piece of infrastructure we built for types (a grammar, a judgement, formation rules) we now build once more, one level up.

A lambda for the type level#

Once types have kinds, let types be abstracted. Write a type-level lambda: λα::Type. τ: a binder that takes a type, and a body that uses it. A function from types to types, written out. (In the F video, capital Λ was a term taking a type; this lowercase λ lives entirely at the type level, taking a type and returning a type. Same shape, different floor.)

List is exactly this: λα. forall β. (α -> β -> β) -> β -> β. The Church encoding, parametrized by the element type, now an honest type-level function. The definitions were there all along; F just couldn't talk about them. And now List Nat is not an abbreviation. The lambda, applied to Nat, beta-reduces: substitute Nat for α and out comes the Church list of naturals in full. To type-check a program using List Nat, the checker beta-reduces the application before comparing types for equality; two types are equal when they reduce to the same normal form. The name is definitional equality. Every typed language with parameterized data does this quietly. F-omega just makes the evaluator explicit.

The type level is a lambda calculus#

Step back. The kinding rules (one judgement Γ ⊢ τ :: κ, "τ has kind κ") are exactly the rules of the simply typed lambda calculus, with Type playing the role of a base type. Kinds are the STLC's types; type expressions are its terms; kinding is its type-checking; beta reduction on types is the same reduction we had on terms back in the lambda calculus video.

So F-omega is two lambda calculi stacked: a simply typed lambda calculus on top, classifying type expressions by their kinds; System F below, classifying terms by their types, with the forall now able to range over any kind, not just Type. One calculus per level, the same structural shape on both. And a real STLC has higher-order functions, so kinds do too: a type operator can take another type operator. StateT S takes a monad (an F of kind Type -> Type) and hands back another. List and Pair were only the first-order case.

Pause and try: what kind does λα. λβ. α -> β have, and is List List well-kinded?

The first takes two proper types and returns a proper type: Type -> Type -> Type. The second is a kind error: List expects a Type, but you handed it something of kind Type -> Type. Kinding catches at the type level exactly the mistakes typing catches at the term level. Same judgement, one floor up.

The binder F couldn't write#

Here is the payoff: a binder F has no name for. Try to write fmap, the map shared by lists, trees, and options. Its signature has to mention an F that turns types into types: forall α β. (α -> β) -> F α -> F β. The new piece is that F. It ranges over functions from types to types, kind Type -> Type, and System F cannot bind one. F-omega can: forall (F::Type -> Type). …. The quantifier now ranges over type constructors, and Functor F becomes a type you can actually write.

Once you can quantify over type constructors, the standard interfaces become writable. Functor F is a record with one field, fmap. Applicative F adds pure and ap; Monad F adds return and bind. All three require F :: Type -> Type; none can be stated in plain F. And F need not be a container: State s = λα. s -> Pair α s has kind Type -> Type, exactly what Monad asks for. List, Maybe, State: all the same shape.

Naturality, for free#

Take two type constructors F and G and write forall α. F α -> G α. That is a natural transformation, a uniform map from one constructor to another, a type we couldn't even state in F. And its naturality square commutes for free. A term η : forall α. F α -> G α has to work at every α and has no way to ask what α is, so whatever it does (drop, duplicate, rearrange) is uniform in the element. Map f then η, or η then map f: η treats the values as opaque, so the two paths land on the same answer.

This isn't intuition; it's Reynolds's abstraction theorem from the System F video, at higher kind. Relate α to β by the graph of f and parametricity becomes the naturality square: Wadler's theorems for free, again. reverse : forall α. List α -> List α only permutes positions, so map f . reverse = reverse . map f. head : forall α. List α -> Maybe α only picks first-or-nothing, and the square commutes even though the functors differ. If you saw the category-theory video, this is where the vocabulary becomes syntax.

Church encodings, one level up#

The System F encodings generalize once you have kinds to talk with. A Church numeral folds the shape of a natural number: each layer is either zero, or a successor carrying something. Name that shape: F = λα. 1 + α, a functor of kind Type -> Type. Replace the step-and-start with a single F-algebra, a function F α -> α that collapses one layer into a target, and the encoding lifts to forall α. (F α -> α) -> α. That is μF, the Church encoding of the least fixed point of F. For a fixed F the encoding is plain System F; it is the generic μ, abstracted over F, that lives in F-omega, the calculus that can bind such an F in the first place.

Pick the layer functor, get the datatype: Nat = μ(λα. 1 + α), List a = μ(λα. 1 + a × α), Tree a = μ(λα. a + α × α). The unique map out of μF that an algebra induces has a name too: the catamorphism. foldr f z is the catamorphism on lists, with the pair (f, z) as its algebra. Flip the construction and you get νF, the greatest fixed point: streams and processes that keep unfolding instead of bottoming out. Inductive types and coinductive types, two corners of one construction, both expressible without adding general recursion.

Normalization, the third time#

We have now asked this three times. STLC normalized (Tait). F normalized (reducibility candidates). Does F-omega? It does: every well-typed term and every well-kinded type reduces to a normal form. Girard again, in his 1972 thesis, the same argument carried one level up and stratified through the kinds. The type half is the one you feel in practice: the checker beta-reduces types before comparing them, so if type-level reduction could loop, type-checking could loop. Because every well-kinded type normalizes, type equality in F-omega is decidable: reduce both sides, check they match. Every compiler whose type system rests on definitional equality rests on that fact.

There's a fence, and Girard found it too. Let Type itself have type Type, one universe containing itself, and you can encode a paradox and derive false. That is Girard's paradox. F-omega stays on the safe side; so do the kernels of Rocq, Agda, and Lean, each carrying a hierarchy of universes precisely to keep Type out of itself.

Inference gets worse, and the languages you use#

Type checking F-omega is decidable; inference (guessing the types you didn't write) is not. F's inference was already undecidable (Joe Wells, 1994). F-omega adds a second source: inferring the type-level function that would make two types match is higher-order unification, which Gérard Huet showed undecidable back in 1973. Real languages cope by restricting the fragment. Haskell lets you bind a type-constructor variable, but only at predictable spots: the head of a type class, a datatype parameter, an explicit signature. The hard questions stay syntactically pinned. You get the expressive power; you skip the undecidable corner.

You have been living in this. Barendregt's lambda cube turns on three dependencies: terms on types gives System F; types on types is the axis we just built, which stacked on F's quantifier gives F-omega; types on terms gives dependent types, the last axis and a later video. Haskell's higher-kinded classes, Scala's higher-kinded parameters, PureScript wholesale: all F-omega. Rust and Java stop short: their type parameters are always proper types, with no way to say F α for an unknown F. Every language in this neighborhood picks a fragment of F-omega and calls it the type system, usually drawing the line where inference stops being manageable.

F gave the type level a quantifier. F-omega gave it a lambda. Together the type level became a small typed functional language of its own, running at compile time to decide which programs below it are well-formed.

If you remember three things#

1. A kind classifies a type the way a type classifies a value, and a type-level lambda turns List from an abbreviation into an honest function Type -> Type, so F-omega's type level is a simply typed lambda calculus, stacked on System F.
2. Quantifying over type constructors is what lets you write Functor, Monad, and natural transformations at all, and their naturality laws hold for free, by parametricity at higher kinds.
3. μF and νF encode inductive and coinductive types with no new recursion, Girard's normalization makes type equality decidable, and your language's higher-kinded generics are an inferable slice of F-omega, one corner over from the calculus of constructions on Barendregt's cube.