By Matthías Páll Gissurarson

When developing non-trivial programs, there is often a lot of type complexity at play. We, as developers, are often quite good at keeping track of what it is that we’re working with while writing programs in Haskell. But often, there is a lot of polymorphism going on, meaning that we’re not quite sure what each “type variable” in the type represents and what the type of the current expression is.

One way to figure it out is to just write `blah`

(assuming that `blah`

is not in scope) and then trying to decipher the error message that the compiler outputs. However, there is a feature that is becoming increasingly common in strongly typed programming languages called “typed-holes”, which allow you to query the compiler more precisely and interactively, without going the round-about way of generating an error.

Typed-holes are especially useful when dealing with *Domain Specific Languages (DSLs)*. By encoding into the types properties about your domain (like the fact that phone numbers have to have a specific length, or that you can only call a function in a secure context), you can use typed-holes to see what the options are in each instance, and to remind yourself what invariants must hold at that specific point.

In this post, I will try to explain typed-holes in the context of GHC (everyone’s favorite compiler), and some cool new contributions that were adopted by GHC that I proposed and implemented, namely, *valid hole fits* and *refinement hole fits* to make them even more useful for developers.

But first, what these “typed-holes”?

## Typed-Holes

Typed-holes were introduced to GHC in version 7.8.1, which was first released in April 2014. In GHC, you write an underscore (`_`

) anywhere you would write an expression, and when you then compile the code, GHC will output a typed-hole error message. Let’s look at an example:

If you write (in GHC 8.6.1 or later)

```
f :: String
f = _ "hello, world"
```

GHC will respond and say:

```
F.hs:2:5: error:
• Found hole: _ :: [Char] -> String
• In the expression: _
In the expression: _ "hello, world"
In an equation for ‘f’: f = _ "hello, world"
• Relevant bindings include f :: String (bound at F.hs:2:1)
...
```

Which tells us the inferred type of the hole (`[Char] -> String`

), the location of the hole, and the “relevant bindings” (local functions whose type is relevant to the type of the hole).

Of course, this isn’t a very useful case, i.e. it is pretty clear what the type of the hole is in this case. A more interesting example is perhaps the `Free`

monad:

```
instance Functor f => Monad (Free f) where
return a = Pure a
Pure a >>= f = f a
Free f >>= g = Free (fmap _ f)
```

Here, the type of the hole involves a few things like `Functors`

, local functions and instance variables, but still the typed-hole can tell us:

```
Free.hs:6:29: error:
• Found hole: _ :: Free f a -> Free f b
Where: ‘a’, ‘b’ are rigid type variables bound by
the type signature for:
(>>=) :: forall a b.
Free f a -> (a -> Free f b) -> Free f b
at Free.hs:5:10-12
‘f’ is a rigid type variable bound by
the instance declaration
at Free.hs:3:10-36
• In the first argument of ‘fmap’, namely ‘_’
In the first argument of ‘Free’, namely ‘(fmap _ f)’
In the expression: Free (fmap _ f)
• Relevant bindings include
g :: a -> Free f b (bound at Free.hs:6:14)
f :: f (Free f a) (bound at Free.hs:6:8)
(>>=) :: Free f a -> (a -> Free f b) -> Free f b
(bound at Free.hs:5:10)
Constraints include Functor f (from Free.hs:3:10-36)
```

Which tells us a lot about the hole, and a lot about the inferred types of the arguments.

## Valid Hole Fits

See that `...`

in the first error message? That’s where my addition comes in. The idea is that, when you’re working with the standard library like the `Prelude`

, or even a more esoteric library like `lens`

, you might not always realize what the possibilities are. You might ask GHC for the type of the hole, but if it’s some weird type like `((Int -> f0 Int) -> T -> f0 T) -> Int -> State T a0`

(where `f0`

and `a0`

are ambiguous), the type might not help you out that much (even if you Hoogle it!). However, the compiler generates the error message, and the compiler knows perfectly well what would be a “valid fit” for the hole.

In GHC 8.6.1, compiling:

```
f :: String
f = _ "hello, world"
```

will now output the following:

```
F.hs:2:5: error:
• Found hole: _ :: [Char] -> String
• In the expression: _
In the expression: _ "hello, world"
In an equation for ‘f’: f = _ "hello, world"
• Relevant bindings include f :: String (bound at F.hs:2:1)
Valid hole fits include
cycle :: forall a. [a] -> [a]
init :: forall a. [a] -> [a]
reverse :: forall a. [a] -> [a]
tail :: forall a. [a] -> [a]
fail :: forall (m :: * -> *) a. Monad m => String -> m a
id :: forall a. a -> a
(Some hole fits suppressed;
use -fmax-valid-hole-fits=N
or -fno-max-valid-hole-fits)
```

Where the valid hole fits are those functions in scope which best fit the type of the hole! This means that by replacing the hole with e.g. `cycle`

or `init`

, you will have a valid program (in the sense that it is well-typed). Of course, this works better for more complex examples, like `lens`

. Consider the following:

```
import Control.Lens
import Control.Monad.State
newtype T = T { _v :: Int }
val :: Lens' T Int
val f (T i) = T <$> f i
updT :: T -> T
updT t = t &~ do
val `_` (1 :: Int)
```

Here, we’re defining a very simple data type `T`

which contains a single value `_v`

of type `Int`

. When we write `val `_` (1 :: Int)`

, we’re asking “what operator can I use here?”. With the new valid hole fits, GHC will tell you:

```
Lens.hs:13:7: error:
• Found hole:
_ :: ((Int -> f0 Int) -> T -> f0 T) -> Int -> State T a0
Where: ‘f0’ is an ambiguous type variable
‘a0’ is an ambiguous type variable
• In the expression: _
In a stmt of a 'do' block: val `_` (1 :: Int)
In the second argument of ‘(&~)’, namely ‘do val `_` (1 :: Int)’
• Relevant bindings include
t :: T (bound at Lens.hs:12:6)
updT :: T -> T (bound at Lens.hs:12:1)
Valid hole fits include
(#=) :: forall s (m :: * -> *) a b.
MonadState s m =>
ALens s s a b -> b -> m ()
with s ~ T, m ~ (StateT T Identity), a ~ Int, b ~ Int
(<#=) :: forall s (m :: * -> *) a b.
MonadState s m =>
ALens s s a b -> b -> m b
with s ~ T, m ~ (StateT T Identity), a ~ Int, b ~ Int
(<*=) :: forall s (m :: * -> *) a.
(MonadState s m, Num a) =>
LensLike' ((,) a) s a -> a -> m a
with s ~ T, m ~ (StateT T Identity), a ~ Int
(<+=) :: forall s (m :: * -> *) a.
(MonadState s m, Num a) =>
LensLike' ((,) a) s a -> a -> m a
with s ~ T, m ~ (StateT T Identity), a ~ Int
(<-=) :: forall s (m :: * -> *) a.
(MonadState s m, Num a) =>
LensLike' ((,) a) s a -> a -> m a
with s ~ T, m ~ (StateT T Identity), a ~ Int
(<<*=) :: forall s (m :: * -> *) a.
(MonadState s m, Num a) =>
LensLike' ((,) a) s a -> a -> m a
with s ~ T, m ~ (StateT T Identity), a ~ Int
(Some hole fits suppressed;
use -fmax-valid-hole-fits=N
or -fno-max-valid-hole-fits)
```

## Refinement Hole Fits

Of course, finding single functions is not always that useful. In Haskell (and with functional programming in general), we often find ourselves programming using higher-order functions and combinators. To facilitate this style, we introduce the `-frefinment-level-hole-fits`

.

Take for example a function of type `[Int] -> Int`

. Using GHCi, we can search the Prelude for any such function:

```
λ> _ :: [Int] -> Int
<interactive>:25:1: error:
• Found hole: _ :: [Int] -> Int
• In the expression: _ :: [Int] -> Int
In an equation for ‘it’: it = _ :: [Int] -> Int
• Relevant bindings include
it :: [Int] -> Int (bound at <interactive>:25:1)
Valid hole fits include
head :: forall a. [a] -> a
with a ~ Int
last :: forall a. [a] -> a
with a ~ Int
length :: forall (t :: * -> *) a. Foldable t => t a -> Int
with t ~ [], a ~ Int
maximum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
with t ~ [], a ~ Int
minimum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
with t ~ [], a ~ Int
product :: forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
with t ~ [], a ~ Int
(Some hole fits suppressed;
use -fmax-valid-hole-fits=N
or -fno-max-valid-hole-fits)
```

But maybe we want to do something different. By setting `-frefinement-level-hole-fits=1`

, we get the following:

```
λ> _ :: [Int] -> Int
<interactive>:33:1: error:
• Found hole: _ :: [Int] -> Int
• In the expression: _ :: [Int] -> Int
In an equation for ‘it’: it = _ :: [Int] -> Int
• Relevant bindings include
it :: [Int] -> Int (bound at <interactive>:33:1)
Valid hole fits include
head :: forall a. [a] -> a
with a ~ Int
last :: forall a. [a] -> a
with a ~ Int
length :: forall (t :: * -> *) a. Foldable t => t a -> Int
with t ~ [], a ~ Int
maximum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
with t ~ [], a ~ Int
minimum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
with t ~ [], a ~ Int
product :: forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
with t ~ [], a ~ Int
(Some hole fits suppressed;
use -fmax-valid-hole-fits=N
or -fno-max-valid-hole-fits)
Valid refinement hole fits include
foldl1 (_ :: Int -> Int -> Int)
where foldl1 :: forall (t :: * -> *) a.
Foldable t => (a -> a -> a) -> t a -> a
with t ~ [], a ~ Int
foldr1 (_ :: Int -> Int -> Int)
where foldr1 :: forall (t :: * -> *) a.
Foldable t => (a -> a -> a) -> t a -> a
with t ~ [], a ~ Int
const (_ :: Int)
where const :: forall a b. a -> b -> a
with a ~ Int, b ~ [Int]
($) (_ :: [Int] -> Int)
where ($) :: forall a b. (a -> b) -> a -> b
with r ~ 'GHC.Types.LiftedRep, a ~ [Int], b ~ Int
fail (_ :: String)
where fail :: forall (m :: * -> *) a. Monad m => String -> m a
with m ~ ((->) [Int]), a ~ Int
return (_ :: Int)
where return :: forall (m :: * -> *) a. Monad m => a -> m a
with m ~ ((->) [Int]), a ~ Int
(Some refinement hole fits suppressed;
use -fmax-refinement-hole-fits=N
or -fno-max-refinement-hole-fits)
```

Which correctly identifies that if we apply `foldl1`

to a function of the correct type, the type of the entire expression will be `[Int] -> Int`

.

# Conclusion

And there you have it! As we’ve seen from the various examples, valid hole fits and refinement hole fits can help developers work with the Prelude to find both simple functions (like `sum`

and `product`

) and complex functions (like `(=<<)`

), even more complex and hard to guess functions from `lens`

(like `(<<*=)`

). For more details (like using typed-holes in conjunction with `TypeInType`

to search by annotated complexity), check out the paper and the talk I gave at Haskell Symposium 2018:

Suggesting Valid Hole Fits for Typed-Holes (Experience Report) [Slides] [Demo Output]