I interactively build a simple B-tree data structure in Haskell, implementing insertion and deletion, using a GADT to ensure that I maintain the structural invariant.

You can also download the MP4 video, as well as the slides I used for my YOW! Lambda Jam 2013 talk, in PDF or Keynote. There’s some code on GitHub.

For those who have trouble with my Aussie accent, you can read along with this script. Sorry, I haven’t yet got around to figuring out how to embed a captions track in the video.

A demonstration of a technique for using types to guide the construction of Haskell programs, based on natural deduction. Includes some tricks for getting help from GHC.

Thanks to Tony Morris, Greg Davis and Clinton Freeman for giving me the idea. Thanks to everyone else for not giving me too much shit about my noisy hole.