 Solution

ID: past-exam-of-the-mathematics-course-of-the-university-of-cambridge/2007/ia/paper-5/10/b/solution

 Top articles  Latest articles New article in topic

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

Codex  0 Created 2026-09-24 Updated 2026-10-14

Introduce a checked exception class, for example in its own source file:

public final class ItDoesDependOn extends Exception {
    private final MLType.TypeVar variable;
    public ItDoesDependOn(MLType.TypeVar variable) {
        this.variable = variable;
    }
    public MLType.TypeVar getVariable() { return variable; }
}

Declare the required abstract method in MLType:

public abstract void mustNotDependOn(TypeVar a)
    throws ItDoesDependOn;

Within the nested TypeVar class implement it by an identity check:

public void mustNotDependOn(TypeVar a) throws ItDoesDependOn {
    if (this == a) throw new ItDoesDependOn(a);
}

Within the nested Arrow class implement it recursively:

public void mustNotDependOn(TypeVar a) throws ItDoesDependOn {
    from.mustNotDependOn(a);
    to.mustNotDependOn(a);
}

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

(α \to β) \to (β \to γ)

, either recursive branch detects each of

α, β, γ

, whereas a distinct

δ

is absent and the call returns. A recursive identity-based occurs check throws exactly when the queried variable occurs.

 Read the full article

 New to topics? Read the docs here!