This summer I've been participating in Google Summer of Code, as I did some years ago. My aim was the same: to make it easier for Haskell developers to interact with their code. But instead of Eclipse, I've focused on another very well-known editor: Emacs. In particular, I've been extending the already excellent ghc-mod.
During the last year I've turned increasingly jealous of the Emacs modes for Agda and Idris, two programming languages which resemble Haskell but add dependent types to the mix. Using those modes, you can work interactively with your code, write pattern matches automatically, refine certain parts of your code, ask the compiler what is the type that a certain code should have, and so on. Furthermore, since version 7.8 GHC includes support for typed holes, so it seemed like all the necessary infrastructure from the compiler was in place to do this.
Instead of a boring description of the outcome of the project, I have prepared a video demostration ;)
As a summary, here is the list of new key bindings that you can use since the release (just a few days ago) of ghc-mod 5.0:
- C-u M-t: create the skeleton of a function from its signature, or the skeleton of a type class instance from its declaration,
- M-t: perform case splitting on variables;
- C-c M-n and C-c M-p: navigate between typed holes in your program, to the next or the previous one, respectively;
- C-c C-f: refine a hole through an expression, including as much holes as needed to make it type check;
- C-c C-a: try automatic completion of a hole by calling Djinn.
I would like to thank eveybody who has helped me during this summer, especially my mentor David Raymond Christiansen (whose work in idris-mode is just amazing) and Kazu Yamamoto, the creator and maintainer of ghc-mod.
