HM Type Inference: Constants and Names | OCaml Programming

Unification is an algorithm for solving equations between terms by finding substitutions that make them equal. In type inference, unification collects local type constraints and combines them into a global solution. When unifying two function types, we recursively unify their left and right components. If unification fails (such as when a type variable occurs within itself), we encounter an 'occurs check' failure, indicating an infinite type.

Unification is the core algorithm used in type inference to solve type constraints. When encountering an application like `reverse X`, the type checker introduces a meta-type variable (alpha) for X and another (beta) for the instantiation of reverse. The constraint alpha ~ list beta is generated, meaning these two types must be equal. Solving this constraint produces a substitution that replaces meta-variables with concrete types. This process, developed by Alan Robinson, transforms the problem of finding a consistent type assignment into a logical puzzle of satisfying equality constraints between types.

Robinson's unification algorithm processes equations one at a time. For equations with function symbols (arrow types), the only way to unify is to unify corresponding subterms. The algorithm handles variables by substituting them with non-variable terms, removes trivial equations, and recursively unifies arguments for function symbols. It terminates because it reduces the number of variables, function symbols, or equations at each step. The algorithm correctly finds the most general unifier when one exists.

The unification algorithm solves systems of type constraints by iteratively applying substitutions to make both sides of each constraint identical, similar to solving algebraic equations through variable elimination; the solution is a sequence of substitutions that transforms each constraint into a tautology (e.g., int = int), and different processing orders may yield different valid substitution sequences.

Unification is the core algorithm for solving type equations. It recursively compares type structures: when a type parameter first matches a concrete type, it gets assigned that value; when two type parameters match each other, they are unified to represent the same type. The algorithm handles failures when types cannot be made identical. This process works for identity relations but requires modifications for assignability and constraints. After unification, instantiation checks whether inferred types actually satisfy constraints and whether function parameters are assignable to their declared types.

The ML type system distinguishes monotypes (τ, no polymorphism) from type schemes (Σ, with polymorphic quantifiers). A fundamental restriction prohibits polymorphic values on function left sides. Two core rules enable polymorphism: generalization (quantifying unused type variables) and instantiation (substituting specific types). These rules alone don't form an algorithm. Two simplifying principles make ML implementable: prenex polymorphism (quantifiers only at top level) and let polymorphism (generalize only at let bindings, instantiate at uses). Together, they define Algorithm W, making type inference practical while preserving expressivity.

Algorithm W is a type reconstruction algorithm for implicit polymorphism. It takes typing context gamma and expression e, returning substitution s and monotype a. The language has monotypes (function types, type variables) and polytypes (for all alpha, monotype). Expressions include variables, lambda abstraction, application, and let binding. The typing context extends with type bindings but lacks explicit type variable declarations. The generalization rule converts monotypes to polytypes when type variables are not free in the context. The specialization rule instantiates polytypes to concrete types. For variables, we check for type bindings and apply specialization by introducing fresh type variables. For lambda abstraction, we introduce a fresh type variable and recursively type the body. For application, we recursively type both expressions, then unify the function type with the argument type using the unification algorithm. The unification algorithm solves type equations by recursively handling variable assignments and function type matching.

Three essential helper functions support Algorithm W: substitution composition applies substitutions sequentially, instance generates fresh type variables for type scheme instantiation, and generalization identifies free type variables not bound in the environment to promote polymorphism. The MGU algorithm performs type unification recursively: variables unify by substitution, basics must match, and function types require unifying inputs then outputs. The result is composed substitutions. This systematic approach enables automated type inference while preserving type safety and polymorphism.

Parametric polymorphism enables code to operate uniformly across all data types through type variables that range over types. An expression with polymorphic type α → α can have many concrete instantiations like int → int or string → string. However, let polymorphism imposes a crucial restriction: functions are only generalized as polymorphic after their binding site. During definition, using a function with a specific type (like id 5) constrains it to that type rather than allowing polymorphism. This explains why defining fun id x = id 5 results in int → int instead of α → α—the use during definition prevents generalization.

Let polymorphism maintains the two-layer type system of monotypes and polytypes from predicative polymorphism while introducing let binding as a new construct. The typing context now has two variable sources: lambda abstractions (monotypes) and let bindings (polymorphic types). The typing rule for let binding requires verifying the bound expression matches the specified polymorphic type, then augmenting the context. This explicit typing eliminates the need for complex reconstruction algorithms while enabling polymorphic variable introduction.

The value restriction is a type system rule that prevents polymorphic mutable values from changing type, ensuring type safety by guaranteeing that once a polymorphic mutable value is instantiated with a specific type, it can never be changed to hold a different type; this rule is implemented in OCaml using weak type variables and similarly appears in Java through array store exceptions, which prevent storing incompatible types in mutable polymorphic collections.

Pure programming avoids side effects and state changes. In OCaml, variables are immutable - defining a new variable with the same name shadows rather than changes the original. To enable mutable data, OCaml uses references, which are memory blocks that can be changed. References have types based on stored values (int ref, string ref). The ref constructor creates references, the exclamation point dereferences to access values, and the colon-equal operator updates values. Memory can be visualized as boxes pointing to locations storing values. Two variables can reference different memory blocks storing the same value (structural equality) or the same memory block (physical equality). OCaml provides operators for both: = checks structural equality, == checks physical equality. The semicolon operator evaluates two expressions, ignoring the first and returning the second - useful for side effects where you care about the update but not the return value. This enables implementing counters and other stateful operations where the side effect matters more than the computed value.

OCaml is a functional programming language where variables are immutable by default (using 'let' binding), and mutable state requires explicit 'ref' types; the language uses 'let name = value in expression' syntax for scoping, semicolons for sequencing expressions with side effects, and 'Array.init' for creating arrays with fixed sizes. Pure functions (no side effects) are a cornerstone of functional programming, enabling predictable behavior and easier reasoning about code.

This extensive section covers pure functions, state management, and OCaml language fundamentals. A pure function has two key properties: determinism (same inputs produce same outputs) and no side effects (no modification of external state). Pure functions are predictable, testable, and reusable. Functions with side effects are problematic because they make code harder to reason about and maintain. The section addresses state management challenges in concurrent programming. As computers moved to multi-core processors, shared mutable state caused race conditions and concurrency bugs. The critical section problem occurs when multiple threads access shared resources simultaneously. Functional programming solves this by using immutable state and avoiding shared mutable state. Instead of modifying state in place, functional programs create new state based on the current state. This approach eliminates race conditions and makes concurrent programming safer. The section then introduces OCaml, a functional programming language with strong type inference. The compiler automatically determines types without explicit declarations. Expressions evaluate to values, and all values have types (int, float, string, bool). Lists are homogeneous sequences of elements of the same type. The empty list is represented as []. The cons operator (::) adds elements to the front of lists. Pattern matching allows matching values against patterns and executing different code for each match. The 'if' expression returns a value rather than executing a block. The 'let' expression binds names to values. Functions are defined using 'let function_name parameters = body'. Functions are first-class citizens, meaning they can be passed as arguments and returned as values. Higher-order functions like List.map apply a function to each element of a list. List.fold_left reduces a list to a single value by applying a function to an accumulator and each element. List.filter keeps only elements that satisfy a predicate function. The type system ensures type safety at compile time. The option type ('a option = None | Some of 'a') represents values that may or may not be present. The result type ('a result = Ok of 'a | Error of 'a') represents computations that may succeed or fail. Pattern matching on these types allows handling different cases safely. This type safety prevents runtime errors and makes code more robust.

The ML type system distinguishes monotypes (τ, no polymorphism) from type schemes (Σ, with polymorphic quantifiers), prohibiting polymorphic values on function left sides. Two core rules enable polymorphism: generalization (quantifying unused type variables) and instantiation (substituting specific types). Two simplifying principles make ML implementable: prenex polymorphism (quantifiers only at top level) and let polymorphism (generalize only at let bindings, instantiate at uses). These principles define Algorithm W. However, adding mutable references breaks soundness because different uses of the same value can share type-dependent resources invisible to the context. The value restriction solves this by limiting generalization to syntactic values (expressions that don't allocate references or create new types), though this introduces complexity requiring programmers to understand syntactic value definitions.