Type safety back and forth

Taken from the brilliant post of Matt Parsons.

Types are a powerful construct for improving program safety. Haskell has a few notable ways of handling potential failure, the most famous being the venerable Maybe type:

data Maybe a
    = Nothing
    | Just a

We can use Maybe as the result of a function to indicate:

Hey, friend! This function might fail. You’ll need to handle the Nothing case.

This allows us to write functions like a safe division function:

safeDivide :: Int -> Int -> Maybe Int
safeDivide i 0 = Nothing
safeDivide i j = Just (i `div` j)

I like to think of this as pushing the responsibility for failure forward. I’m telling the caller of the code that they can provide whatever =Int=s they want, but that some condition might cause them to fail. And the caller of the code has to handle that failure later on.

This is the easiest technique to show and tell, because it’s one-size-fits-all. If your function can fail, just slap Maybe or Either on the result type and you’ve got safety. I can write a 35 line blog post to show off the technique, and if I were feeling frisky, I could use it as an introduction to Functor, Monad, and all that jazz.

Instead, I’d like to share another technique. Rather than push theresponsibility for failure forward, let’s explore pushing it back. This technique is a little harder to show, because it depends on the individual cases you might use.

If pushing responsibility forward means accepting whatever parameters and having the caller of the code handle possibility of failure, then pushing it back is going to mean we accept stricter parameters that we can’t fail with. Let’s consider safeDivide, but with a more lax type signature:

safeDivide :: String -> String -> Maybe Int
safeDivide iStr jStr = do
    i <- readMay iStr
    j <- readMay jStr
    guard (j /= 0)
    pure (i `div` j)

This function takes two strings, and then tries to parse Int=s out of them. Then, if the =j parameter isn’t 0, we return the result of division. This function is safe, but we have a much larger space of calls to safeDivide that fail and return Nothing. We’ve accepted more parameters, but we’ve pushed a lot of responsibility forward for handling possible failure.

Let’s push the failure back.

safeDivide :: Int -> NonZero Int -> Int
safeDivide i (NonZero j) = i `div` j

We’ve required that users provide us a NonZero Int rather than any old Int. We’ve pushed back against the callers of our function:

No! You must provide a NonZero Int. I refuse to work with just any Int, because then I might fail, and that’s annoying.

So speaks our valiant little function, standing up for itself!

Let’s implement NonZero. We’ll take advantage of Haskell’s PatternSynonyms language extension to allow people to pattern match on a “constructor” without exposing a way to unsafely construct values.

{-# LANGUAGE PatternSynonyms #-}

module NonZero
  ( NonZero()
  , pattern NonZero
  , unNonZero
  , nonZero
  ) where

newtype NonZero a = UnsafeNonZero a

pattern NonZero a <- UnsafeNonZero a

unNonZero :: NonZero a -> a
unNonZero (UnsafeNonZero a) = a

nonZero :: (Num a, Eq a) => a -> Maybe (NonZero a)
nonZero 0 = Nothing
nonZero i = Just (UnsafeNonZero i)

This module allows us to push the responsibility for type safety backwards onto callers.

As another example, consider head. Here’s the unsafe, convenient variety:

head :: [a] -> a
head (x:xs) = x
head []     = error "oh no"

This code is making a promise that it can’t keep. Given the empty list, it will fail at runtime. Let’s push the responsibility for safety forward:

headMay :: [a] -> Maybe a
headMay (x:xs) = Just x
headMay []     = Nothing

Now, we won’t fail at runtime. We’ve required the caller to handle a Nothing case. Let’s try pushing it back now:

headOr :: a -> [a] -> a
headOr def (x:xs) = x
headOr def []     = def

Now, we’re requiring that the caller of the function handle possible failure before they ever call this. There’s no way to get it wrong. Alternatively, we can use a type for nonempty lists!

data NonEmpty a = a :| [a]

safeHead :: NonEmpty a -> a
safeHead (x :| xs) = x

This one works just as well. We’re requiring that the calling code handle failure ahead of time.

A more complicated example of this technique is the justified-containers library. The library uses the type system to prove that a given key exists in the underlying Map. From that point on, lookups using those keys are total: they are guaranteed to return a value, and they don’t return a Maybe.

This works even if you map over the Map with a function, transforming values. You can also use it to ensure that two maps share related information. It’s a powerful feature, beyond just having type safety.

¶The Ripple Effect

data Order = Order  { items :: [Item] }

data Order = Order { items :: NonEmpty Item }

¶Ask Only What You Need

foobar :: ByteString -> IO ByteString