B-trees with GADTs

15 May 2013

Haskell
data structures
dependent types
screencast

I interactively build a simple B-tree data structure in Haskell, implementing insertion and deletion, using a GADT to enforce the structural invariant. The GADT also guides us towards a correct implementation.

Also on YouTube. MP4 downloads are available from Vimeo. The slides I used for my YLJ13 talk are available in PDF or Keynote. There’s some code on GitHub, and a script.