GHC/Typed holes

Type holes in GHC.

Type holes are a powerful feature in GHC that is inspired by Agda. But what are type holes, and how do they help us write code?

(This page was taken from a 'tutorial' I wrote of this feature on Reddit.)

Introduction

Sometimes, when writing programs, we tend to use lots of polymorphic types. That's good! We can reuse those pieces, thanks to the types. But it can be difficult sometimes, when writing a program, to see how the polymorphic types should exactly fit together, given the things in scope.

Would it not be nice if we could have the compiler tell us the types of everything in scope? It'd be much easier to see how we can 'fit' them together like puzzle pieces.

This is the purpose of a hole: it has similar semantics to undefined, in that evaluating it is an error (you can replace all holes with undefined, and vice versa, and nothing has changed: you may even say undefined is just a really crappy, useless hole!) But it's special in that, when GHC encounters a hole during compilation, it will tell you what type needs to be there in place of the hole, for the type-checker to be OK with the definition.

This feature was implemented by Simon Peyton Jones, Sean Leather and Thijs Alkemade, and is scheduled to be released with GHC 7.8.1 (likely released sometime mid-2013.)

Motivating example

Let us consider the definition of a Free monad:

data Free f a
  = Pure a
  | Free (f (Free f a))

A free monad coupled with an underlying Functor f. We would like to write the Monad instance for Free f.

We begin by writing the trivial cases:

instance Functor f => Monad (Free f) where
  return a     = Pure a
  Pure a >>= f = f a
  Free f >>= g = ... -- I'm confused!

... but we're a little stumped on how to write the final case. Let's have the compiler help us do this.

Writing 'instance Monad (Free f)'

Let's go ahead and shove all of this in a file:

{-# LANGUAGE TypeHoles #-}
module FreeMonad where

data Free f a
  = Pure a
  | Free (f (Free f a))

instance Functor f => Monad (Free f) where
  return       = Pure
  Pure a >>= f = f a
  Free f >>= g = Free _

Now let's load that into GHCi:

$ ghci FreeMonad.hs

[1 of 1] Compiling Main ( holes.hs, interpreted )


holes.hs:29:23: Warning:

   Found hole `_' with type f (Free f b)
   Where: `f' is a rigid type variable bound by
              the instance declaration at holes.hs:26:10
          `b' is a rigid type variable bound by
              the type signature for
                >>= :: Free f a -> (a -> Free f b) -> Free f b
              at holes.hs:28:10
   Relevant bindings include
     >>= :: Free f a -> (a -> Free f b) -> Free f b
       (bound at holes.hs:28:3)
     f :: f (Free f a) (bound at holes.hs:29:8)
     g :: a -> Free f b (bound at holes.hs:29:14)
   In the first argument of `Free', namely `_'
   In the expression: Free (_)
   In an equation for `>>=': (Free f) >>= g = Free (_)

Ok, modules loaded: Main.

• Main>

Notes on parametricity and Agda

TODO FIXME