Simon Meier - Test-Driven Development of a Unification Algorithm

This is a past event

21 people went

Location image of event venue


"If it type checks, then it works." is a phrase that is true more often for Haskell code than for code written in other languages. Tests are though still needed! In particular for code which depends on conditions not captured by the type system. An example of such code is (first-order) unification [1], a classic algorithm used for example in type checkers, Prolog interpreters, and theorem provers.

In this interactive live-coding talk, we'll together
- revisit the theory of first-order terms, substitutions, and unification;
- explore how to use hedgehog [2] to implement unification in a test-driven fashion; and
- learn how to use ghcid [3] to get live test feedback.

PS: In case you wonder: why unification? Blinded by the ease of writing (mostly) correct Haskell code, past-me was not very big into testing. During my PhD, I've learned the hard way that unification is one of the algorithms that has ample room for subtle mistakes -- and tests are absolutely a must! Back then, I've written a number of regression tests to capture the problems after the fact. This talk is the result of present-me exploring how TDD combined with modern property-based testing fares in detecting these subtle mistakes up-front.