Hole-driven Haskell

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 the compiler, GHC.

Also on YouTube. MP4 downloads are available from Vimeo. There are subtitles.