B-trees with GADTs
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.