Haskell Language Typed holes Using typed holes to define a class instance


Typed holes can make it easier to define functions, through an interactive process.

Say you want to define a class instance Foo Bar (for your custom Bar type, in order to use it with some polymorphic library function that requires a Foo instance). You would now traditionally look up the documentation of Foo, figure out which methods you need to define, scrutinise their types etc. – but with typed holes, you can actually skip that!

First just define a dummy instance:

instance Foo Bar where

The compiler will now complain

Bar.hs:13:10: Warning:
No explicit implementation for
  ‘foom’ and ‘quun’
In the instance declaration for ‘Foo Bar’

Ok, so we need to define foom for Bar. But what is that even supposed to be? Again we're too lazy to look in the documentation, and just ask the compiler:

instance Foo Bar where
  foom = _

Here we've used a typed hole as a simple “documentation query”. The compiler outputs

    Found hole ‘_’ with type: Bar -> Gronk Bar
    Relevant bindings include
      foom :: Bar -> Gronk Bar (bound at Foo.hs:4:28)
    In the expression: _
    In an equation for ‘foom’: foom = _
    In the instance declaration for ‘Foo Bar’

Note how the compiler has already filled the class type variable with the concrete type Bar that we want to instantiate it for. This can make the signature a lot easier to understand than the polymorphic one found in the class documentation, especially if you're dealing with a more complicated method of e.g. a multi-parameter type class.

But what the hell is Gronk? At this point, it is probably a good idea to ask Hayoo. However we may still get away without that: as a blind guess, we assume that this is not only a type constructor but also the single value constructor, i.e. it can be used as a function that will somehow produce a Gronk a value. So we try

instance Foo Bar where
  foom bar = _ Gronk

If we're lucky, Gronk is actually a value, and the compiler will now say

    Found hole ‘_’
      with type: (Int -> [(Int, b0)] -> Gronk b0) -> Gronk Bar
    Where: ‘b0’ is an ambiguous type variable

Ok, that's ugly – at first just note that Gronk has two arguments, so we can refine our attempt:

instance Foo Bar where
  foom bar = Gronk _ _

And this now is pretty clear:

    Found hole ‘_’ with type: [(Int, Bar)]
    Relevant bindings include
      bar :: Bar (bound at Bar.hs:14:29)
      foom :: Bar -> Gronk Bar (bound at Foo.hs:15:24)
    In the second argument of ‘Gronk’, namely ‘_’
    In the expression: Gronk _ _
    In an equation for ‘foom’: foom bar = Gronk _ _

You can now further progress by e.g. deconstructing the bar value (the components will then show up, with types, in the Relevant bindings section). Often, it is at some point completely obvious what the correct definition will be, because you you see all avaliable arguments and the types fit together like a jigsaw puzzle. Or alternatively, you may see that the definition is impossible and why.

All of this works best in an editor with interactive compilation, e.g. Emacs with haskell-mode. You can then use typed holes much like mouse-over value queries in an IDE for an interpreted dynamic imperative language, but without all the limitations.