Haskell Language Typed holes Using typed holes to define a class instance
Example
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
Bar.hs:14:10:
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.
