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]