= Solution
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 $(\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. \b[A recursive identity-based occurs check throws exactly when the queried variable occurs.]
Back to article page
