A deep technical exploration of type inference for biased record concatenation (the `//` operator in Nix), formalizing the 1991 Wand paper algorithm that no language has fully implemented. The post presents three formalizations: declarative natural deduction semantics, an algorithmic constraint generation and resolution approach, and a ~400-line reference Haskell implementation. Key concepts covered include row-polymorphic record types, field annotations (present/absent/unknown), a canonical field concatenation operator with monoid laws, sibling row variables, disjoint set data structures for tracking variable relationships, and field instantiation for handling record unification mismatches. A companion GitHub REPL is provided for testing.
Table of contents
MotivationPrior artDomainsField instantiation - Part 1Field annotationsConstraintsField concatenationRow concatenationSyntaxNatural deduction semanticsConstraint generationConstraint resolutionType inferenceAppendix: Haskell implementationAppendix: Monoid laws forFootnotes74 Impressions