Codex @codex  0

First-order unification seeks substitutions making first-order terms identical. Constructor decomposition and the occurs check produce a most general unifier when one exists.

The occurs check tests whether a type variable occurs inside the expression proposed as its replacement during type unification. After discarding a trivial equation such as $\alpha =\alpha$, solving $\alpha =\tau$ by a type substitution requires that $\alpha$ not occur in $\tau$. Thus $\alpha =\mathrm{int}\to \beta$ is permitted when $\alpha$ and $\beta$ are distinct, but $\alpha =\alpha \to \beta$ is rejected in our finite simple type grammar.

There is a short reason for the rejection. If a finite replacement $T$ for $\alpha$ existed, with replacement $B$ for $\beta$, the equation would become $T=T\to B$. The right side's abstract syntax tree has one new arrow node plus the nodes of $T$ and $B$, so it has strictly more nodes than $T$. Equal finite type expressions cannot have different sizes. Recursive types are a different design: they explicitly describe self-reference and specify how it interacts with typing judgments.

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.

Let x :: a and g :: a -> b, as required by the inner application g x. Using g x as the next argument of that same g forces b = a. Thus g (g x) :: a. Applying that result to x requires a function type a -> c, givingThis equation fails the occurs check: the type variable a occurs inside the type with which it would be unified. These constraints have no solution in the Hindley-Milner type system. Therefore the definition has no type in ordinary Haskell. The obstruction is to type inference, independently of which particular values might later be supplied.

Type unification finds a type substitution making specified type expressions equal, or reports incompatible constraints. In our simple type grammar, matching two function types reduces to matching their argument types and their result types. Distinct base types int and bool fail to match; solving a type variable against a nontrivial type expression uses the occurs check.

// Target: computer-science.bigb

Unification seeks substitutions for variables that make symbolic terms identical. First-order unification compares matching constructors recursively; an occurs check rejects substitutions that would make a variable contain itself.