Type-guided development and garden paths

“Types help you reason about effects”, we declare. And they do! Except when they don’t. “Just follow the types!” we insist. But sometimes the types take you down a garden path.

When the type checker is happy but the behaviour is all wrong, it can be hard to find where you took the wrong turn. In this post I’ll share real-world examples of this phenomenon, and offer some tips on how to avoid it.

Random generation of applicatives §

The Applicative type class provides a function for lifting a “pure” value into the applicative data type:

class Applicative (k :: * -> *) where
  pure :: a -> k a
  (<*>) :: k (a -> b) -> k a -> k b

Assume we have a random generator of values of type a, and wish to generate random applicatives. The shape of this problem is:

genAp :: (Applicative t) => Gen a -> Gen (t a)

We can generalise Gen to any effect f:

effAp :: (Applicative t) => f a -> f (t a)

How can implement this? Follow the types! t has an Applicative instance, so if we introduce a Functor constraint on f we can write:

effAp :: (Functor f, Applicative t) => f a -> f (t a)
effAp = fmap pure

Now we have a nice, general function that runs an effect and lifts the result into an applicative. Let’s test it by generating single-value lists of Word8:

λ> effAp randomIO :: IO [Word8]
[120]
λ> effAp randomIO :: IO [Word8]
[33]

OK! Now let’s use it for the following vector type:

data V3 a = V3 a a a

-- boring
instance Functor V3
instance Applicative V3
instance Foldable V3
instance Traversable V3

The random V3 values generated are:

λ> effAp randomIO :: IO (V3 Word8)
V3 186 186 186
λ> effAp randomIO :: IO (V3 Word8)
V3 215 215 215

Oh dear. We followed the types to implement effAp, but the implementation is not correct! Instead of running the effect 3 times to generate 3 random vector components, it ran the effect once and used the result 3 times.

effAp should first lift the effect into the applicative type using pure, giving a value of the type (Applicative t) => t (f a). The shape of the hole is now t (f a) -> f (t a). That is exactly the shape of sequenceA:

sequenceA
    :: (Traversable t, Applicative f)
    => t (f a) -> f (t a)

Accepting the tighter constraints, the implementation of effAp becomes:

effAp
    :: (Traversable t, Applicative f, Applicative t)
    => f a -> f (t a)
effAp = sequenceA . pure

Now effAp has the expected behaviour:

λ> effAp randomIO :: IO (V3 Word8)
V3 251 198 213

Composing effects (by ignoring them) §

In Purebred we have an input validation system that checks inputs as the user types. It dispatches the validation work to a background thread, so the UI stays responsive. Each time the user edits the input, the program kills the outstanding validation thread (if any) and spawns a new one. The program code (simplified for this article) is:

dispatchValidation = do
  let spawn = forkIO doValidation
  oldId <- getValidationThread
  newId <- maybe spawn (killThread $> spawn) oldId
  _ <- setValidationThread (Just newId)

The outstanding validation thread is stored in a Maybe ThreadId. In the Just case the program kills the old thread, spawns a new thread and returns the new ThreadId:

(killThread $> spawn) :: ThreadId -> IO ThreadId

Except, it does not. At a glance, we see the actions occurring in the correct order. But there was a bug. Input validation had unexpected and nondeterministic results. For example, a valid input might (or might not) result in an error being shown.

We can apprehend the error by equational reasoning:

  killThread $> spawn
= const spawn <$> killThread       -- definition of ($>)
= const spawn . killThread         -- fmap for ((->) r)
= \x -> const spawn (killThread x) -- definition of (.)
= \x -> spawn                      -- definition of const

The expression discards the old ThreadId and never executes killThread. As a consequence, validation threads run wild, finishing their work in a nondeterminstic order.

When we finally understood the problem, the fix was straightforward. We replaced the expression:

killThread $> spawn  -- broken

with:

\t -> killThread t *> spawn  -- fixed

Lessons learned §

I discussed two bugs where the type checker was happy and the code seemed superficially reasonable. Both had implementations guided by “type tetris” (what fits here?) that turned out to be fundamentally wrong. What strategies can help avoid such traps?

The first bug involved use of the wrong abstraction; Functor instead of Applicative. Making an effort to test generic functions with a greater diversity of instances might have helped discover this bug sooner. In the case of applicatives, don’t just test with [], Maybe and other “common” types where pure constructs a “singleton” value. Test with Proxy a (which has zero a values), Join (,) a (two a values), and so on.

As for the second bug, my advice is don’t try to be clever when writing effectful code. do notation and explicit binds are fine. Using underscore binds to ignore values may result in more readable code than const and related functions. If you have a hole with a function type, start by writing the lambda, and work step by step to complete the definition. Make sure it’s correct first, and only then tidy it up (if you want to).

In the case of the Purebred bug, we had a hole with the type ThreadId -> IO ThreadId, and filled it with an expression that subtly ignored the ThreadId argument. Our next step, when faced with this hole, should have been to write the expression (\threadId -> _). Critically, this binds the ThreadId argument, making it hard to ignore.

The final takeaway is: don’t be smug about the power of the type system. Type-guided development is indeed wonderful and powerful, but let’s be honest that in many cases, reasoning from the types alone won’t get you all the way to a correct solution. On the contrary, you may find yourself at the end of a garden path!