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. We should see something that looks like this:

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

FreeMonad.hs:11: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 FreeMonad.hs:10:10
    Relevant bindings include
      >>= :: Free f a -> (a -> Free f b) -> Free f b
        (bound at FreeMonad.hs:11:3)
      f :: f (Free f a) (bound at FreeMonad.hs:11:8)
      g :: a -> Free f b (bound at FreeMonad.hs:11: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> 

Let's look at the error, and what the hole should look like (first line of the error):

Found hole `_' with type f (Free f b)

OK, so I need some value of type f (Free f b) to put there. I don't know how to get that. But let's look at what's in scope:

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 `_'

OK, so I have 3 values directly surrounding me at my disposal: f, g, and (>>=). I have a f :: f (Free f a) in scope, and that's almost what I need. I just need to turn the inner Free f a into a Free f b. And that's what fmap does for functors! And I don't know what the functor f is anyway, so clearly I need to fmap the value before anything else. Let's do that and use a hole to tell us where to go next:

instance Monad ... where
  ...
  Free f >>= g = Free (fmap _ f)

Now we get from the compiler:

Found hole `_' with type Free f a -> Free f b

OK, so now we just need some function with type Free f a -> Free f b. Let's look at what's in scope. We can quickly see that (>>=) has the type we want if we partially apply it. And g has just the type we need for that partial application! Equationally:

(>>=) :: Free f a -> (a -> Free f b) -> Free f b g :: a -> Free f b

Ergo:

(\x -> x >>= g) :: Free f a -> Free f b

So the result is:

instance Monad ... where

 ...
 Free f >>= g = Free (fmap (>>= g) f)

Notes on parametricity and Agda

TODO FIXME