# Difference between revisions of "GHC/Typed holes"

(→Notes on parametricity, free theorems and Agda) |
(→Notes on parametricity, free theorems and Agda) |
||

Line 144: | Line 144: | ||

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. |
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!]' |
+ | 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!) |
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!) |

## Revision as of 16:22, 12 October 2012

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

## Contents

## 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 resulting instance is:

instance Monad ... where
return = Pure
Pure a >>= f = f a
Free f >>= g = Free (fmap (>>= g) f)

## 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* `Monad` instance for `Free`!

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 `f :: Int -> Double` could have many possible definitions, but we can always be sure for example, that `f :: a -> a` only has one valid definition, or that if `f :: [a] -> [a]`, then 'trivially' we can see that `f [] = []` 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 '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 `f :: [a] -> [a]` as we said earlier, then we get the free theorem `f [] = []` 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 in the correct places. This 'forces' few definitions to exist.

Holes for GHC were inspired by the equivalent feature in its (twice removed) sister language, Agda. Holes are considerably more powerful in Agda, mostly due to the fact it is total, and the compiler infers less, but as a result can derive more code for you. In particular, Agda can literally *write* 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 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
`let x = x in x`, and the type of this expression is`forall a. a`, meaning I can prove*anything*with it. In the domain of Haskell semantics, this expression is in fact equivalent to undefined 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, "Fast and Loose reasoning is morally correct.")