View source for GHC/Typed holes

[[Category:GHC|Type system]]
<span style='font-size: x-large; font-weight: bold'>Typed holes in GHC.</span>

Typed holes are a powerful feature in GHC inspired by [http://wiki.portal.chalmers.se/agda/pmwiki.php Agda]. But what are typed holes, and how do they help us write code?

(This page was taken from a 'tutorial' I wrote of this feature [http://www.reddit.com/r/haskell/comments/10u7xr/ghc_head_now_features_agdalike_holes/c6gr9qe 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 <tt>undefined</tt>, in that evaluating it is an error (you can replace all holes with <tt>undefined</tt>, and vice versa, and nothing has changed: you may even say <tt>undefined</tt> 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. It will also show you the types of all the bindings in scope, to assist you in figuring out the problem.

This feature was implemented by Simon Peyton Jones, Sean Leather and Thijs Alkemade, and is introduced with GHC 7.8.1. It is enabled by default.

== Motivating example ==

Let us consider the definition of a Free monad:

<haskell>
data Free f a
  = Pure a
  | Free (f (Free f a))
</haskell>

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

We begin by writing the trivial cases:

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

... 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. For the final case of the <tt>Monad (Free f)</tt> instance, we will place a hole in the definition, which is designated by the same syntax for wildcard patterns, <tt>_</tt>

<haskell>
module FreeMonad where

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

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

Now let's load that into GHCi. We should see something that looks like this:

<code><pre>
$ 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> 
</pre></code>

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

<code><pre>
Found hole `_' with type f (Free f b)
</pre></code>

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

<code><pre>
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 `_'
</pre></code>

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

<code><pre>
instance Monad ... where
  ...
  Free f >>= g = Free (fmap _ f)
</pre></code>

Now we get from the compiler:

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

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

<code><pre>
(>>=) :: Free f a -> (a -> Free f b) -> Free f b
g     ::              a -> Free f b
</pre></code>

Ergo:

<code><pre>
(\x -> x >>= g) :: Free f a -> Free f b
</pre></code>

So the resulting instance is:

<code><pre>
instance Functor f => Monad (Free f) where
  return a     = Pure a
  Pure a >>= f = f a
  Free f >>= g = Free (fmap (>>= g) f)
</pre></code>

== Notes on parametricity, free theorems and Agda ==

These examples hint at what people mean when they say they use the type system to drive development: it can help write your code, too!

This is of course very powerful for general, polymorphic types like above, because a polymorphic function may only be written so many ways. In fact, the above definition is the only legitimate <tt>Monad</tt> instance for <tt>Free</tt>!

A polymorphic type variable says what you cannot do to it: touch! You can't break the parametric nature of it by scrutinizing the variable in any way. A useful implementation of a polymorphic function has a small 'design space', naturally. It is not so, when defining monomorphic functions. A function like <tt>f :: Int -> Double</tt> could have many possible definitions, but we can always be sure for example, that <tt>f :: a -> a</tt> only has one valid definition, or that if <tt>f :: [a] -> [a]</tt>, then 'trivially' we can see that <tt>f [] = []</tt> must hold as a law.

This notion of "what information may be calculated based on the type" like we're doing here can be formalized to what we call 'Free Theorems', pioneered by Philip Wadler in his paper '[http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf Theorems for Free!]'

Free theorems fall out of the parametricity theorem (also called Reynolds' abstraction theorem,) which essentially states how polymorphic types relate to each other. Free theorems just state that, given a polymorphic type, it's possible to derive useful theorems and laws, based only on that type alone (so if <tt>f :: [a] -> [a]</tt> as we said earlier, then we get the free theorem <tt>f [] = []</tt> by definition - try writing that case another way! You can't!)

At this point, you're getting into much deeper territory, but I say all this because you have probably intuitively thought some of these things, when writing polymorphic functions yourself - that you must write them in such a way that the terms are all properly abstracted over correctly. This kind of design 'forces' only a few definitions to be possible.

Holes for GHC were inspired by the equivalent feature in its (twice removed) sister language, [http://wiki.portal.chalmers.se/agda/pmwiki.php Agda]. Holes are considerably more powerful in Agda, mostly due to the fact it is total, the compiler infers less, and thus Agda programs are <i>rich</i> with evidence, giving witness to many facts the compiler can use. As a result, it can derive more code for you. In particular, Agda can literally <i>write</i> your code based on holes. It's able to do things like write case-analysis' for you, based only on type structure, and what's in scope, and discharge all the 'trivial' cases. You do this in emacs, in one or two keystrokes. It's essentially a semi-automated feedback loop for development, and it makes sense because the tool is really working with a meaningful model of your code, only in sensible ways that type-check. It's great.

There is not necessarily a reason why this could not exist for e.g. the Emacs mode for Haskell. Just because Haskell is not total, doesn't mean we couldn't calculate useful code based on the type - it is just much harder, especially considering the multitudes of features and extensions GHC supports.

* When I say 'legitimate' or 'useful', I mean, 'modulo divergent definitions.' Because Haskell is not total, it is possible to write divergent terms like <tt>let x = x in x</tt>, and the type of this expression is <tt>forall a. a</tt>, meaning I can prove <i>anything</i> with it. In the domain of Haskell semantics, this expression is in fact equivalent to <tt>undefined</tt> as well, because all bottoms are equal. I can prove that Blue is Green this way, or that Freedom is Slavery - I can inhabit any type, using these nonsensical terms. Logistically, you could say Haskell terms are complete, but not coherent/consistent. But divergent definitions here are not very legitimate, interesting, or useful, obviously, so ignore them (cue, [http://www.cse.chalmers.se/~nad/publications/danielsson-et-al-popl2006.html "Fast and Loose reasoning is morally correct."])