In this talk I will demonstrate HoleFitPlugins, a recent (on HEAD) extension of GHC’s plugin framework that enables end-users to write their own hole-fit suggestion synthesizers, and show examples of how this can enable users to use tools such as Djinn or QuickCheck to synthesize and filter by type and properties. These HoleFitPlugins would enable more expressive editor functionality (such as filtering by modules for specific DSLs or to incorporate Hoogle suggestions). The grand future vision is to enable human guided intelligent synthesis of program snippets using a learned model that would be too expensive to ship with GHC (e.g. since it might add too many dependencies beyond those that are already required by GHC, such as Hoogle, TensorFlow or Z3). In contrast, HoleFitPlugins are installed from Hackage or other sources, and developers would be free to experiment with different models and bundled blobs that which advanced users could install at will.

Additionally, I will relate a crazy idea on how we could extend GHCi to enable more interactive development by adding an interactive compilation model. It is often the case that the developer knows what behavior they want, but that they have a hard time relating said behavior to the compiler, for example with instance resolution and how to fill holes. By adding interactive compilation, the compiler can ask the the user to provide the information it needs to make a decision, by e.g. adding more types, providing a property, or an example, from which the compiler can determine the correct behavior. This would in conjunction with an editor plugin enable a style of development like that of Agda, where GHCi acts as a “compilation assistant” that guides the implementation of programs, and allow programmers to have a greater understanding of the process.

Matthías Páll Gissurarson is a PhD student in the Functional Programming division of Chalmers. His interests include functional programming, building tools, Magic: The Gathering and being an armchair philosopher. He’s currently working on the programming model for the Octopi project, a platform to program secure IoT applications.