TOP CONCEPTS optics type Abstracting getters/setters across product and sum types (lens, prism, traversal).
du variant A named constituent of a discriminated union, pairing a du_tag with a du_payload type. Each variant represents
lens optic An optic pairing a getter with a setter over a product type's field, enabling focused access to one du_payload
type inference Compiler or runtime deducing types from context without explicit annotation.
discriminated union Tagged union enabling compiler-verified exhaustive pattern matching over variants.
du tag A value-level or type-level label that uniquely identifies which variant of a discriminated union is active in
constraint solving The phase that processes the generated constraints via unification, producing the principal substitution.
instantiation Operation that replaces quantified variables in a type scheme with fresh type variables.
type variable Placeholder symbol ranging over types, awaiting instantiation (alpha in Hindley-Milner).
algorithm w The classic Hindley-Milner type_inference algorithm combining constraint_generation, most_general_unifier comp
constraint An atomic equational condition of the form type_A = type_B produced during constraint_generation, awaiting res
du payload The data value carried by a specific variant of a discriminated union. Only one payload is live at a time; the
generalization Operation that abstracts free type variables into quantified variables, forming a type scheme.
prism optic An optic pairing a matcher with a builder over a sum type's du_variant, enabling partial projection into one d
pt02 type_inference: the algorithmic process of deriving types for expressions by propagating constraints from know
pt09 instantiation: replacing quantified variables in a type scheme with fresh type variables, yielding a less-gene
substitution A total function from type_variable to monotype; a mapping recording how each type_variable was solved during
unification The algorithm that, given two monotypes, computes a substitution that makes them syntactically identical, or r
algebraic data type Type formed by sum (union) and product (record) of other types.
du match The elimination form: a function that, given a discriminated union value, dispatches on its du_tag to apply th