16. System F: Polymorphism and Minimal Type Checking

16. System F: Polymorphism and Minimal Type Checking#

Goal. Learn how forall-types enable parametric polymorphism, and experiment with a minimal System F type checker.

You will learn

The syntax of System F (types and terms)
The typing rules for \(\forall\) (type abstraction and instantiation)
Why full System F type inference is not something we can “just do” automatically
How to encode data structures (like pairs) using polymorphism (Church encodings)

Roadmap#

State the core grammar and typing rules.
Build polymorphic identity/const and type-check them.
Instantiate polymorphic terms and type-check applications.
Encode a pair type using \(\forall\) and derive fst/snd.

Formal Core#

Types:

\[ T ::= \alpha \mid \mathrm{Int} \mid \mathrm{Bool} \mid T \to T \mid \forall \alpha.\ T \]

Terms:

\[ t ::= x \mid \lambda x:T.\ t \mid t\ t \mid \Lambda \alpha.\ t \mid t\,[T] \mid \texttt{IntLit} \mid \texttt{BoolLit}. \]

Typing rules for \(\forall\)

Type abstraction:

\[ \frac{\Gamma \vdash t : T}{\Gamma \vdash \Lambda \alpha.\ t : \forall \alpha.\ T} \]

Type application:

\[ \frac{\Gamma \vdash t : \forall \alpha.\ T}{\Gamma \vdash t\,[U] : T[\alpha := U]} \]

The key point is that polymorphism is explicit: you must choose where to abstract and where to instantiate.

Inference Caveat#

In simply typed lambda calculus (Chapter 4), the system is small enough that type inference is practical.

In System F:

type checking (given annotations and instantiations) is straightforward,
type inference (discovering the instantiations/annotations automatically) is not.

So our code is a checker, not a general inference engine.

from pathlib import Path
import sys

book_root = Path.cwd()
if not (book_root / "advanced").exists():
    book_root = book_root.parent
if str(book_root) not in sys.path:
    sys.path.insert(0, str(book_root))

from advanced import systemf_core as sf

Polymorphic Identity#

The polymorphic identity is:

\[ \mathrm{id} := \Lambda a.\ \lambda x:a.\ x \]

It should have type \(\forall a.\ a \to a\).

id_term = sf.TyLam("a", sf.Lam("x", sf.TVar("a"), sf.Var("x")))
print("term:", sf.show_tm(id_term))
print("type:", sf.show_ty(sf.infer(id_term, {}, set())))

term: (/\\a. (lambda x:a. x))
type: (forall a. (a -> a))

Explicit Instantiation and Application#

To use id at Int, we instantiate:

\[ \mathrm{id}[\mathrm{Int}] : \mathrm{Int} \to \mathrm{Int} \]

and then apply to a value.

inst = sf.TyApp(id_term, sf.TInt())
full = sf.App(inst, sf.IntLit(7))

print("term:", sf.show_tm(full))
print("type:", sf.show_ty(sf.infer(full, {}, set())))

term: (((/\\a. (lambda x:a. x)) [Int]) 7)
type: Int

Another Polymorphic Shape: `const`#

The polymorphic constant function is:

\[ \mathrm{const} := \Lambda a.\ \Lambda b.\ \lambda x:a.\ \lambda y:b.\ x \]

Type:

\[ \forall a.\ \forall b.\ a \to b \to a. \]

This illustrates parametricity: const cannot inspect b (it has no operations on an abstract type), so it must ignore it.

const_term = sf.TyLam(
    "a",
    sf.TyLam(
        "b",
        sf.Lam("x", sf.TVar("a"), sf.Lam("y", sf.TVar("b"), sf.Var("x"))),
    ),
)

print("term:", sf.show_tm(const_term))
print("type:", sf.show_ty(sf.infer(const_term, {}, set())))

term: (/\\a. (/\\b. (lambda x:a. (lambda y:b. x))))
type: (forall a. (forall b. (a -> (b -> a))))

Reusable Local Inference for Applications#

Even though full inference is hard, there is a useful local operation:

if you already know the type of a function position (possibly polymorphic),
and you know the argument type,

then you can often infer the result type by instantiating/unifying.

systemf_core.py provides infer_app_local(fn_ty, arg_ty) for that pattern.

poly_id = sf.poly_id_type()

res_bool = sf.infer_app_local(poly_id, sf.TBool())
res_int = sf.infer_app_local(poly_id, sf.TInt())

print("local infer (id Bool):", sf.show_ty(res_bool))
print("local infer (id Int): ", sf.show_ty(res_int))

local infer (id Bool): Bool
local infer (id Int):  Int

Church Encoding: Pairs via Polymorphism#

System F can encode products without built-in pair types. Define the pair type:

\[ \mathrm{Pair}(a,b) := \forall r.\ (a \to b \to r) \to r. \]

An inhabitant of Pair(a,b) is a function that, given a result type r and a consumer f : a -> b -> r, produces an r by supplying its two components.

def Pair(a, b):
    r = sf.TVar("r")
    return sf.TForall("r", sf.TArrow(sf.TArrow(a, sf.TArrow(b, r)), r))

pair_term = sf.TyLam(
    "a",
    sf.TyLam(
        "b",
        sf.Lam(
            "x",
            sf.TVar("a"),
            sf.Lam(
                "y",
                sf.TVar("b"),
                sf.TyLam(
                    "r",
                    sf.Lam(
                        "f",
                        sf.TArrow(sf.TVar("a"), sf.TArrow(sf.TVar("b"), sf.TVar("r"))),
                        sf.App(sf.App(sf.Var("f"), sf.Var("x")), sf.Var("y")),
                    ),
                ),
            ),
        ),
    ),
)

print("pair type:", sf.show_ty(sf.infer(pair_term, {}, set())))

pair type: (forall a. (forall b. (a -> (b -> (forall r. ((a -> (b -> r)) -> r))))))

Projections: `fst` and `snd`#

To extract the first component:

instantiate the pair at result type a,
pass a consumer that returns its first argument.

Similarly for the second component.

a = sf.TVar("a")
b = sf.TVar("b")

fst_term = sf.TyLam(
    "a",
    sf.TyLam(
        "b",
        sf.Lam(
            "p",
            Pair(sf.TVar("a"), sf.TVar("b")),
            sf.App(
                sf.TyApp(sf.Var("p"), sf.TVar("a")),
                sf.Lam("x", sf.TVar("a"), sf.Lam("y", sf.TVar("b"), sf.Var("x"))),
            ),
        ),
    ),
)

snd_term = sf.TyLam(
    "a",
    sf.TyLam(
        "b",
        sf.Lam(
            "p",
            Pair(sf.TVar("a"), sf.TVar("b")),
            sf.App(
                sf.TyApp(sf.Var("p"), sf.TVar("b")),
                sf.Lam("x", sf.TVar("a"), sf.Lam("y", sf.TVar("b"), sf.Var("y"))),
            ),
        ),
    ),
)

print("fst type:", sf.show_ty(sf.infer(fst_term, {}, set())))
print("snd type:", sf.show_ty(sf.infer(snd_term, {}, set())))

fst type: (forall a. (forall b. ((forall r. ((a -> (b -> r)) -> r)) -> a)))
snd type: (forall a. (forall b. ((forall r. ((a -> (b -> r)) -> r)) -> b)))

Type-Checking a Concrete Pair Usage#

We can build pair[Int][Bool] 7 true and then type-check fst[Int][Bool] applied to it.

(We do not implement evaluation here; the focus is on typing and encodings.)

pair_Int_Bool = sf.TyApp(sf.TyApp(pair_term, sf.TInt()), sf.TBool())

p = sf.App(sf.App(pair_Int_Bool, sf.IntLit(7)), sf.BoolLit(True))
print("type(p):", sf.show_ty(sf.infer(p, {}, set())))

fst_Int_Bool = sf.TyApp(sf.TyApp(fst_term, sf.TInt()), sf.TBool())
use_fst = sf.App(fst_Int_Bool, p)
print("type(fst p):", sf.show_ty(sf.infer(use_fst, {}, set())))

type(p): (forall r. ((Int -> (Bool -> r)) -> r))
type(fst p): Int

Reuse Note

All core definitions are reusable from advanced/systemf_core.py:

types: TVar, TArrow, TForall, …
terms: Lam, App, TyLam, TyApp, …
type checking: infer(term, gamma, delta)
pretty printers: show_ty, show_tm
local polymorphic application helper: infer_app_local

Exercise

Define the polymorphic const term and confirm its type is \(\forall a.\forall b.\ a \to b \to a\).
Define a polymorphic pair type Pair(a,b) and implement pair (constructor) as above.
Implement fst and snd and confirm their types.
Use infer_app_local to infer the result type of applying id to Int and Bool arguments. See solutions: Exercise 16 (System F)

Summary#

System F adds explicit polymorphism via \(\forall\) types.
Type abstraction (\(\Lambda\)) and type application (\([T]\)) are the key new term forms.
Full System F type inference is not automatic; we rely on explicit annotations.
Polymorphism is expressive enough to Church-encode data structures like pairs.

This concludes the main arc of the book: from untyped lambda calculus, through STLC and logic, to advanced extensions.