Type Systems

A type system specifies how program components can be legally combined. Type checking validates rules, while type inference fills in omitted type information. Which errors they exclude depends on the specific rules and their soundness; they cannot guarantee the absence of all runtime errors or business logic errors.

Formal proofs of type safety typically discuss how well-typed programs avoid getting stuck in certain rule-less executable states; whether null pointer dereferences, array out-of-bounds, or division by zero are statically excluded depends on how the language models these operations.

Type Rules: Connecting Local Judgments

Γ ⊢ e : T denotes that expression e has type T in environment Γ. Simple integer addition rules require both sides to be Int, resulting in Int; if requires the condition to be Bool, and both branches must satisfy the language-defined common result type.

Function calls first check callability and argument count, then check parameter types and other constraints item by item. Simply zipping pairs would miss extra or missing arguments. Real languages may also involve default arguments, variadic arguments, overloading, and coercions.

Checking is not necessarily bottom-up. Bidirectional type checking combines "synthesizing types from expressions" and "checking expressions under expected types," leveraging context to reduce ambiguity and improve error locations.

Type Representation and Identity

Internal representations typically distinguish basic types, functions, type constructor applications, type variables, and declaration identities. Recursive types can be linked via IDs or indirect references and should not infinitely copy the entire structure.

Nominal type identity comes from declarations, not simple string name comparison: two modules both declaring Point may still be different types. Structural rules, on the other hand, determine specific relationships based on constituent parts. Type equality, assignment compatibility, subtyping, and explicit casting are distinct problems.

Languages can also mix rules. Go's named type identity differs from its unnamed structural type rules, and interface implementation relies on method sets; it cannot be generalized as "all structurally identical structs in Go are the same type." Go Type Identity Rules

Unification: Finding Substitutions That Make Type Expressions Equal

Introduce variables α, β for unknown types. For the function application f(3), it can produce type(f)=Int→α. If the context requires the result to be Bool, add α=Bool.

Unification recursively compares constructors: List<α> and List<Int> yield α=Int; function types compare parameters and results item by item; Int and Bool fail. Substitutions must propagate consistently, not just modify the current type name in one place.

The occurs check prevents establishing disallowed infinite types, such as α=α→β. If α appears in the type to be bound, it should be rejected under standard HM type syntax. Ignoring this step may cause the solver to loop or accept types beyond the model.

A Minimal Unifier: Apply Old Substitutions First, Then Establish New Constraints

Strings starting with ? represent type variables, ordinary strings represent base types, and tuples represent constructor applications, e.g., ("List", "?a"). Function types are uniformly represented as binary constructors Fn; this is a finite first-order type term model that does not handle subtyping, overloading, recursive types, or full HM generalization.

def variable(t):
    return isinstance(t, str) and t.startswith("?")


def resolve(t, substitution):
    if variable(t) and t in substitution:
        return resolve(substitution[t], substitution)
    if isinstance(t, tuple):
        return (t[0], *(resolve(x, substitution) for x in t[1:]))
    return t


def occurs(v, t):
    return v == t or (isinstance(t, tuple) and any(occurs(v, x) for x in t[1:]))


def unify(a, b, substitution):
    a, b = resolve(a, substitution), resolve(b, substitution)
    if a == b:
        return
    if variable(a):
        if occurs(a, b):
            raise TypeError("infinite type")
        substitution[a] = b
        return
    if variable(b):
        unify(b, a, substitution)
        return
    if (isinstance(a, tuple) and isinstance(b, tuple)
            and a[0] == b[0] and len(a) == len(b)):
        for x, y in zip(a[1:], b[1:]):
            unify(x, y, substitution)
        return
    raise TypeError("type constructor mismatch")


subst = {}
unify(("Fn", "?a", "?b"), ("Fn", "Int", ("List", "?c")), subst)
unify("?c", "Bool", subst)
assert resolve(("Fn", "?a", "?b"), subst) == ("Fn", "Int", ("List", "Bool"))
for a, b in [("Int", "Bool"), ("?a", ("Fn", "?a", "?b")),
             (("Pair", "Int"), ("Pair", "Int", "Bool"))]:
    try:
        unify(a, b, {})
    except TypeError:
        pass
    else:
        raise AssertionError("incompatible types accepted")
# Indirect self-references must also be rejected: after ?a = ?b, ?b = List<?a>.
indirect = {}
unify("?a", "?b", indirect)
try:
    unify("?b", ("List", "?a"), indirect)
except TypeError:
    pass
else:
    raise AssertionError("indirect occurs check missed")

The first constraint yields ?a=Int, ?b=List<?c>, followed by ?c=Bool. When reading the function type, substitutions must be applied recursively to obtain Int→List; modifying only the current node would leave ?c unupdated. The indirect self-reference test shows that the occurs check must be performed after existing substitutions are interpreted.

Failures here terminate the current solving process immediately. If used for overload candidate probing, previous recursive steps may have already modified substitution; upon failure, that branch should be discarded or rolled back, rather than continuing with a half-successful substitution to try the next candidate. Input construction of type terms should be guaranteed valid by the frontend; real implementations need additional depth and workload limits.

Where must a substitution propagate to solve a type?

Every occurrence of a variable must mean the same substitution. Select compatible constraints or build constructor conflicts and indirect cycles. Failure invalidates the entire solve; its trace explains where it failed, not a partial substitution to reuse in another candidate.

Hindley–Milner: Generalization and Instantiation Are Both Essential

In a simplified pure HM language, let id = fun x -> x can be inferred as α→α, and at the let binding, type variables not free in the outer environment are generalized into a type scheme ∀α. α→α.

Each use of id re-instantiates it with fresh type variables. Thus, id 1 and id true can use Int→Int and Bool→Bool respectively, rather than sharing the same unbound variable across two calls.

Lambda parameters do not undergo such let generalization in basic HM. If fun f -> (f 1, f true) were to treat f as a polymorphic function callable on two types, it would exceed this simple rule; one cannot claim that arbitrary higher-order polymorphism of function parameters is automatically inferred by HM.

Languages with effects like mutable references need to restrict generalization, such as the value restriction in ML-family languages, to avoid incorrectly treating shared mutable cells as multiple types. Actual languages may go beyond pure HM, adding type classes, subtyping, or local annotations, changing the inference algorithms and guarantees accordingly.

Generalization Cannot Turn Unknowns From the Outer Environment Into Arbitrary Types

Suppose the environment already has x:?a, and let keep = fun u -> x has type ?b→?a. ?b can be generalized, but ?a comes from the environment and remains constrained by the actual type of x. Therefore, the scheme is ∀β. β→?a, not ∀αβ. β→α. The latter scheme incorrectly allows callers to arbitrarily choose the return type, as if the same x could be both Int and Bool.

The set of generalized variables is typically written as free(type) − free(environment); instantiation only refreshes scheme-quantified variables, preserving associations with environment unknowns. The unifier above only resolves equality constraints and does not implement this step, so it cannot be directly called a complete Algorithm W.

Shared mutable cells make the problem more obvious: if a storage location is incorrectly generalized, each access re-instantiates it to an arbitrary element type, potentially writing as Int first and then reading the same content as a function type. OCaml uses weak type variables and rules like the value restriction to constrain this, with specific relaxation rules leveraging variance. OCaml Polymorphism and Mutable State

Which unknowns may be fresh at each use?

The set difference in generalization has a concrete purpose: an unknown inherited from the environment cannot be chosen independently by every caller. id has no such dependency; keep returns the same outer x, so different argument types still share its result type. Two instances expose both fresh quantified variables and preserved environment variables.

$$Q=\mathrm{FTV}(\tau )\setminus \mathrm{FTV}(\Gamma ),\sigma =\forall Q.\tau$$

Subtyping and Variance: Which Substitutions Are Safe

If Dog<:Animal, a position requiring only Animal capabilities can accept Dog. For functions, a function that can handle any Animal can be used by a caller that only passes Dog; input positions exhibit contravariance, while output positions typically exhibit covariance.

Read-write containers that allow Box<Dog> to be directly used as Box<Animal> could allow users to write a Cat and then read it from the original Dog view, so they usually need to be invariant, or use other designs like runtime checks or restricted interfaces.

Covariance for read-only interfaces presupposes that there is indeed no capability to write incompatible values through that interface. Variance is determined by how type parameters are used in each position; you cannot draw a blanket conclusion just by seeing the names List or Array.

Rust's subtyping mainly revolves around lifetimes and higher-rank lifetime types, and type constructors have their own variance; it cannot be simplified to "everything else is only compared by name." Trait implementation and type coercions are also not equivalent to ordinary inheritance subtyping. Rust Subtyping and Variance

Why does function input variance run backward?

Read function types as set contracts. Possible caller inputs must be contained in the candidate’s accepted inputs; possible candidate outputs must fit the caller’s permitted results. Caller input is Dog, while candidate input/output and required output vary. Gold values exhibit an uncovered input or an out-of-contract result.

$$(A_c\to R_c)<:(A_e\to R_e)\text{if}{A}_e<:A_c\wedge R_c<:R_e$$

Generic Semantics and Machine Code Strategies Are Separate

Languages and compilers can combine strategies. One cannot assert that all generics in Swift or other languages are only monomorphized, nor can one say that all type information in Java becomes literal List<Object>; erasure rules, bounds, and retained metadata have specific specifications.

Specialization reduces certain indirect calls, but it does not mean generic programs have "zero runtime overhead" overall. Allocation, actual algorithms, and code caching still exist; compilers may also merge equivalent instances.

Traits / Typeclasses: Solving Capability Constraints

The constraint T supports a certain operation means checking conditions such as required implementations and associated types. Solving may recursively generate new obligations, involving consistency, ambiguity, and termination strategies. Static generic calls and dynamic interface objects have different dispatch mechanisms.

Not every trait can be directly written as a valid dyn Trait; object compatibility, associated types, and method signatures have requirements. Understanding requires first distinguishing between "checking that T has the capability" and "how to find the implementation at runtime."

Error Messages Are Also Part of Type System Implementation

Preserve sources for constraints: which argument, which return position, which declaration produced the expected type. Error recovery can use tagged unknowns or error types to reduce cascading errors, but it must not treat them as proven correct during successful code generation.

Actual inference also requires resource limits and clear annotation entry points to avoid extremely long compilations caused by complex instances. Whether adding language features remains decidable depends on analyzing the combined rules, not just judging by feature names.

References

• Go Specification: Type Identity.
• Rust: Subtyping and Variance.
• Symbol Tables and Scopes, Compile-Time Metaprogramming.

Keywords: type checking, inference, unification, occurs check, Hindley-Milner, generalization, subtyping, variance, monomorphization