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)'

TODO FIXME

Notes on parametricity and Agda

TODO FIXME