Represent the two constructors of the type grammar by subclasses of The nested classes are public for use by clients, while their fields are private;
MLType: a TypeVar node and an Arrow node containing two types. Use immutable fields so a completed type expression cannot acquire cycles through later mutation. The static factory allocates a fresh object and gives it a fresh identifier shared across the whole hierarchy:import java.math.BigInteger;
public abstract class MLType {
private MLType() { }
private static BigInteger next = BigInteger.ONE;
public static synchronized TypeVar createNewTypeVar() {
TypeVar answer = new TypeVar(next);
next = next.add(BigInteger.ONE);
return answer;
}
public static final class TypeVar extends MLType {
private final BigInteger id;
private TypeVar(BigInteger id) { this.id = id; }
}
public static final class Arrow extends MLType {
private final MLType from, to;
public Arrow(MLType from, MLType to) {
if (from == null || to == null)
throw new IllegalArgumentException();
this.from = from; this.to = to;
}
}
}TypeVar can be created only through the factory. Client code uses MLType.TypeVar and MLType.Arrow. A type variable is identified by its unique node, and a function type by its domain and codomain nodes; repeated occurrences of one logical variable share the same TypeVar object.The monotonically increasing
BigInteger identifier avoids fixed-width counter overflow, and synchronization prevents two simultaneous calls from receiving the same identifier. Actual allocation remains subject to available memory. This is an abstract syntax tree representation, possibly sharing subexpressions. Fresh variable nodes and recursive arrow nodes represent every type in the given grammar.Introduce a checked exception class, for example in its own source file:Declare the required abstract method in Within the nested Within the nested 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.
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; }
}MLType:public abstract void mustNotDependOn(TypeVar a)
throws ItDoesDependOn;TypeVar class implement it by an identity check:public void mustNotDependOn(TypeVar a) throws ItDoesDependOn {
if (this == a) throw new ItDoesDependOn(a);
}Arrow class implement it recursively:public void mustNotDependOn(TypeVar a) throws ItDoesDependOn {
from.mustNotDependOn(a);
to.mustNotDependOn(a);
}For , 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.
Add a public override of In Inherited dynamic dispatch selects the proper method at every node of the abstract syntax tree. Full parentheses distinguish the domain and codomain nesting without relying on a reader's precedence convention. Repeated occurrences of one type variable use the same identifier, and distinct factory variables have distinct identifiers. For example, with the first three factory variables, the type from part (b) prints as
toString in each concrete subclass. In TypeVar:public String toString() {
return "t" + id.toString();
}Arrow:public String toString() {
return "(" + from.toString() + " -> " + to.toString() + ")";
}((t1 -> t2) -> (t2 -> t3)). The recursive textual form preserves both arrow structure and variable identity. Articles by others on the same topic
There are currently no matching articles.