Personal tools

GHC/TypedHoles

From HaskellWiki

< GHC(Difference between revisions)
Jump to: navigation, search
(Writing 'instance Monad (Free f)')
(Writing 'instance Monad (Free f)')
Line 57: Line 57:
 
</haskell>
 
</haskell>
   
Now let's load that into GHCi:
+
Now let's load that into GHCi. We should see something that looks like this:
   
<code>
+
<code><pre>
 
$ ghci FreeMonad.hs
 
$ ghci FreeMonad.hs
</code>
 
 
<code>
 
 
[1 of 1] Compiling Main ( holes.hs, interpreted )
 
[1 of 1] Compiling Main ( holes.hs, interpreted )
   
+
FreeMonad.hs:11:23: Warning:
holes.hs:29:23: Warning:
 
 
Found hole `_' with type f (Free f b)
 
Found hole `_' with type f (Free f b)
 
Where: `f' is a rigid type variable bound by
 
Where: `f' is a rigid type variable bound by
Line 73: Line 70:
 
the type signature for
 
the type signature for
 
>>= :: Free f a -> (a -> Free f b) -> Free f b
 
>>= :: Free f a -> (a -> Free f b) -> Free f b
at holes.hs:28:10
+
at FreeMonad.hs:10:10
 
Relevant bindings include
 
Relevant bindings include
 
>>= :: Free f a -> (a -> Free f b) -> Free f b
 
>>= :: Free f a -> (a -> Free f b) -> Free f b
(bound at holes.hs:28:3)
+
(bound at FreeMonad.hs:11:3)
f :: f (Free f a) (bound at holes.hs:29:8)
+
f :: f (Free f a) (bound at FreeMonad.hs:11:8)
g :: a -> Free f b (bound at holes.hs:29:14)
+
g :: a -> Free f b (bound at FreeMonad.hs:11:14)
 
In the first argument of `Free', namely `_'
 
In the first argument of `Free', namely `_'
 
In the expression: Free (_)
 
In the expression: Free (_)
Line 84: Line 81:
 
Ok, modules loaded: Main.
 
Ok, modules loaded: Main.
 
*Main>
 
*Main>
</code>
+
</pre></code>
   
 
== Notes on parametricity and Agda ==
 
== Notes on parametricity and Agda ==

Revision as of 16:04, 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

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

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

3 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> 

4 Notes on parametricity and Agda

TODO FIXME