Agda-like Interaction Mode for Emacs

by Alejandro Serrano for haskell.org

In dependently typed languages (like Agda or Idris), it’s usual for the environment to help you writing the code, as a sort of dialog. The main idea is that the developer can include “holes” in the source code. Emacs interprets those holes specially and allows some special commands inside them. Since Agda and Idris are dependently-typed variations of Haskell, I think that there’s the possibility of implementing a similar features for the Haskell mode. The aim is to produce such piece of code.