begriffs

Filling Haskell's Type Holes Like It's Agda

February 7, 2015

Kirstin Rhys gives a live coding demo of interactively building Haskell functions by filling type holes. This allows her to write abstract things which would be quite a challenge for the unaided mind. Interactive type holes are used in provers like Agda and Idris and are now supported by GHC 7.8.

Summary

  • First a demo in Agda to show how that system feels
    • Building the filter function as a warm-up
  • Next doing it to Haskell with ghc-mod
    • Rewriting filter to compare
    • That was easy, so let’s try functions that are not intuitively clear
    • like deriving the Functor instance for the free monad
    • …and then the Applicative instance
    • Success! Look how hard that would have been without help