Past exam of the mathematics course of the University of Cambridge / 2007 / ia / Paper 5 / 10 / b / Solution

Introduce a checked exception class, for example in its own source file:Declare the required abstract method in MLType:Within the nested TypeVar class implement it by an identity check:Within the nested Arrow class implement it recursively:The parameter denotes an actual non-null type variable returned by the factory; checking object identity distinguishes different variables without confusing their printed names. Structural induction on the abstract syntax tree proves the occurs check: a variable node contains the queried variable exactly when the identities match, and an arrow contains it exactly when either component does. The first detected occurrence throws and propagates the checked exception; normal return proves absence. Both subclass methods must declare the exception, and callers must catch or declare it.

For $(\alpha \to \beta )\to (\beta \to \gamma )$, either recursive branch detects each of $\alpha ,\beta ,\gamma$, whereas a distinct $\delta$ is absent and the call returns. A recursive identity-based occurs check throws exactly when the queried variable occurs.