Getting better type errors by typing literally everything

August 09, 2020
« Previous post   Next post »

This is going to be a bit of shorter post.

You probably already know that you can (and should) give top-level signatures to your functions, to improve your type errors. And though intra-function type inference is nice, sometimes we would prefer even better type errors.

By default, if you try to add a type signature to intermediate data (say, within a case expression or a let binding), the compiler will yell at you:

foo :: Maybe Int -> Int
foo m = case m of
  Just (x :: Int) -> x  -- this won't compile!

But you actually can write code like this — you just need to prod the compiler a bit, by enabling the ScopedTypeVariables language extension.

{-# LANGUAGE ScopedTypeVariables #-}

foo :: Maybe Int -> Int
foo m = case m of
  Just (x :: Int) -> x  -- now it compiles!
  Nothing         -> 0

This harmless extension now gives you the ability to write type signatures in a whole bunch of different places. The identfiers you bind in a case expression, the identifiers you bind in a let, the identifiers you bind inside a do-block, and even function parameters are all fair game now.

interactiveHandleResult :: Either String a -> IO a
interactiveHandleResult (result :: Either String a) = do
  switch :: String <- getLine
  case (result, switch) of
    (_, "override")             -> fail "exiting due to interactive interrupt"
    (Left (error :: String), _) -> fail error
    (Right (val :: a), _)       -> pure val

Adding signatures like this can let the compiler give you much better type errors, since it no longer has to do type inference and knows exactly what type you're looking for, rather than having to guess. Thus, it can tell you how you're a flawed, fleshy human, and how the code you've written could never produce something of that type, in much more detail.

You could even forgo adding the top-level signature for your functions entirely, and just type the parameters individually. Doing this would probably cross the line from "mere preference" to something that would be somewhat bad Haskell style in many people's eyes, myself included, as the top-level signatures are very useful for skimming code and getting a sense for how everything fits together.

One small hiccup to keep in mind is when adding types for intermediate data that's generic. let bindings and where bindings specifically will require an explicit forall keyword if you're using type variables from the function's type signature. For instance, even with ScopedTypeVariables enabled, this won't compile:

reverse' :: [a] -> [a]
reverse' l =
  let revL :: [a] = reverse l
  in revL

You'll need to add a forall to the function's signature:

reverse' :: forall a. [a] -> [a]
reverse' l =
  let revL :: [a] = reverse l
  in revL

The short version: just like normal parameters, where you can't use an undefined name inside a function body, you can't use undefined or unbound type parameters either. Without the forall, "a" isn't bound anywhere in the first definition, so you have to explicitly bring it into scope.1

Like practically every other choice of code style in Haskell, whether you choose to do this is basically a matter of preference or not. Is it a common thing to do? No, absolutely not; in fact, I don't know of any Haskell codebases that are written this way. But Haskell is, as ever, an exercise in making your own decisions, weighing the pros and cons yourself. If you find it useful, and find that it helps you understand the types that are going on in your program, use it. If not, don't.

Found this useful, or otherwise have comments or questions? Talk to me!

« Previous post   Next post »

Before you close that tab...


↥1 We’re heavily glossing over a lot of different aspects with this explanation. The topic of type parameters, existential types, and usage of explicit foralls could honestly fill a whole series of posts. What we’ve shown here covers the most common issue.

If you want (some of) the gory details, check out the section in the GHC User’s Guide on lexically scoped type variables.