Reference

Static Semantics and Type Representation

Look up syntax, contracts, layouts, algorithms, and exact behavior.

OJaml uses a Hindley-Milner-style constraint system. Types are primitives, type variables, applications for tuples/records/arrays/lists/sets/maps, nominal variants with type arguments, and function types. Record type declarations add named record shapes to the checker environment; algebraic data type declarations add nominal variant type constructors and constructor bindings. Module-local types and constructors are stored under qualified names; declarations inside the same module receive short-name aliases for sibling and enclosing module types, and open declarations add short-name aliases for immediate exported values, types, and constructors. Value, function parameter, and higher-order function annotations resolve those names and unify the annotated position with the declared shape. Module signature ascription first verifies required abstract type entries against the module's local type declarations, then resolves each val type in that local type namespace and unifies it with the exported member's inferred type. Checking walks the AST, creates fresh type variables where information is not known yet, and unifies constraints as expressions demand relationships between values.

In plain terms, inference means type annotations are not required everywhere. The checker invents placeholders, then replaces or links those placeholders as it learns facts from literals, operators, branches, function calls, annotations, and standard-library signatures. If two facts disagree, such as a branch being both int and string or an annotated record missing a declared field, the program is rejected before code generation.

Type
  prim("int" | "float" | "bool" | "string" | "unit")
  var(id, instance?, numeric?)
  app("array", [elem])
  app("list", [elem])
  app("set", [elem])
  app("tuple", [item0, item1, ...])
  app("record", {field: type, ...})
  app("map", [key, value])
  variant("option", [item])
  fn(params[], result)

Type constructors. Heap-backed compound values are not erased during checking; tuple positions, record labels, collection elements, map keys, map values, and variant type arguments remain visible to unification.

let main =
  if true then 1 else "no"

Rejected branch mismatch. The condition is bool, but the branches try to unify int with string, so the checker rejects the program.

\frac{x:\tau \in \Gamma}{\Gamma \vdash x : \tau}\quad\quad\frac{x:\sigma \in \Delta}{\Gamma,\Delta \vdash x : \operatorname{fresh}(\sigma)}

Variable lookup. Local values are used directly, while global declarations and builtins are freshly instantiated when referenced.

Top-level declarations are installed into the global environment before their bodies are checked. A zero-parameter declaration receives a fresh type variable. A parameterized declaration receives a function stub whose parameter and result types are fresh variables. This permits recursive references because the name is available before the body is checked. Local let rec follows the same idea on a smaller scope: the checker inserts the local function name before checking its body, unifies that placeholder with the function type, and rejects recursive local bindings that are not functions.

\frac{\Gamma \vdash f : \tau_f\quad \Gamma \vdash a_i : \tau_i\quad \operatorname{unify}(\tau_f,\;\tau_1 \rightarrow \cdots \rightarrow \tau_n \rightarrow \alpha)}{\Gamma \vdash f\;a_1\ldots a_n : \alpha}

Application. Function application creates a fresh result type and unifies the callee against a function from argument types to that result.

The checker rejects duplicate top-level bindings, undefined names, arity errors, branch disagreement, sequence expressions whose left side is not unit, pipeline targets that are not one-argument functions, tuple/record/list/array arity, label, or element mismatches in expressions and patterns, non-exhaustive matches without wildcard, variable, structurally exhaustive tuple/record arms, or complete list empty/cons coverage, invalid tuple projection, invalid pair helpers, missing record fields, duplicate record labels, invalid print/println arguments, and main values that cannot be returned directly from the runtime. main may return int, float, bool, or unit; strings and heap values should be printed, converted with to_string, or reduced to one of those result types.

\frac{\Gamma \vdash c:bool\quad \Gamma \vdash t:\tau\quad \Gamma \vdash e:\tau}{\Gamma \vdash \texttt{if}\;c\;\texttt{then}\;t\;\texttt{else}\;e : \tau}

Branch agreement. Both branches of a conditional must unify to one result type.

Pruning follows instantiated type variables until it reaches a concrete representative.
Occurs checks prevent infinite types such as a = a -> b.
Freshening copies polymorphic variables so one builtin use cannot constrain another unrelated use.
Polymorphic functions whose bodies use numeric operators display constrained variables as number when they can be instantiated at either int or float call sites.
showType formats resolved types for diagnostics, completion details, and hover output.

Static Semantics and Type Representation

Continue exploring