Tag
unification
- Sep 23, 2026 Elaboration: Filling in What the Program Did Not Say How metavariables, unification, and implicit arguments turn surface syntax into a fully explicit core term, and why the process can fail in ways the source does not explain. computation theory
- Mar 26, 2025 Bottom-Up Expression Typing with Inference Variables How a checker types an expression from its children, when it must defer a decision to a metavariable, and how unification and the occurs check close those holes. compilers
- Sep 17, 2024 Decision Procedures for Word Equations and Unification How Makanin’s algorithm decides whether two words with variables can be made equal, why the bound on solution length is enormous, and what unification gains from restricting to free function symbols. computation theory
- Aug 15, 2024 Unification and the Hindley–Milner Inference Algorithm How ML-family languages recover types without annotations: unification variables, the occurs check, and the level discipline that keeps generalization cheap. programming languages