Re-inventing the Monad wheel

Lately, I spent some time working on one of my Haskell projects: hoare-imp. It is basically an implementation of propositional calculus+first-order logic+number theory (Peano)+Hoare logic, and allows one to reason about computer programs, producing Hoare triples. The source code of this implementation is at around 600 LoC at this moment.

I will explain how I re-implemented a monad, and even used it without knowing about it. And I am sure you have done the same, at some point, too!

Let’s start with the famous question: What is a Monad?

I’ll try to use as little mathematical definitions as possible, though at some point we’ll definitely need them.

For now, all we need to know, in terms of programming, is that a Monad is all about being explicit over some piece of code and the result it produces, by “grouping” different types of “calculations” in such a way that composing these calculations “makes sense”. Because being explicit is important, as it tells a lot about our program structure.

Simple DSL

To show one example, let’s start by considering the following DSL:

data Expr =
  Val Float
  | Mul Expr Expr
  | Div Expr Expr
  deriving (Show)

Perfect, a small little language that can represent float division and multiplication. How would an eval function look like? Here’s one possibility:

eval :: Expr -> Float
eval (Val x) = x
eval (Mul x y) = eval x * eval y
eval (Div x y) = eval x / eval y

Cool, we give it an Expr and we always end up with a number. Or do we?

> eval (Mul (Val 1) (Val 3))
3.0
> eval (Mul (Val 1) (Val 0))
0.0
> eval (Div (Val 1) (Val 0))
Infinity

Run-time error handling

No worries. We will slightly modify our eval function:

eval :: Expr -> Float
eval (Val x) = x
eval (Mul x y) = eval x * eval y
eval (Div x y) =
  let x' = eval x in let y' = eval y in
  if y' == 0
  then error "Division by zero!"
  else x' / y'

Now we get:

> eval (Div (Val 1) (Val 0))
*** Exception: Division by zero!

But, this error halts the program completely, and we have no way to catch it and respond to it.

Either to the rescue! We have to rewrite our function… again…

Graceful error handling

When we get a value that is not erroneous, we will use Right, otherwise, use Left.

eval :: Expr -> Either String Float
eval (Val x) = Right x
eval (Mul x y) =
  let x' = eval x
      y' = eval y in go x' y' where
  go (Right x) (Right y) = Right $ x * y
  go (Left x) _ = Left x
  go _ (Left x) = Left x
eval (Div x y) =
  let x' = eval x
      y' = eval y in go x' y' where
  go (Right x) (Right 0) = Left "Division by zero!"
  go (Right x) (Right y) = Right $ x / y
  go (Left x) _ = Left x
  go _ (Left x) = Left x

Perfect little function. We can now use it as follows:

> eval (Div (Val 1) (Val 0))
Left "Division by zero!"
> eval (Div (Val 1) (Val 5))
Right 0.2

Great, it works! But…

Abstracting error handling

Having to add all those gos for each pattern matching case is a bit tedious… can we somehow make it better? What is common between the first go and the second go?

  go (Right x) (Right y) = Right $ x * y
  go (Left x) _ = Left x
  go _ (Left x) = Left x
--
  go (Right x) (Right y) = Right $ x / y
  go (Left x) _ = Left x
  go _ (Left x) = Left x

Let’s try to come up with a more generic go. Instead of accepting a value as the second parameter, let’s make it accept a function so that we can either multiply, or divide, or whatever:

go (Right x) f = f x
go (Left x)  _ = Left x

And that’s it. We just implemented a monad for the Either data type. Something similar to this is what I had in my code:

whenRight :: Either a t -> (t -> Either a b) -> Either a b
whenRight (Right x) f = f x
whenRight (Left x)  _ = Left x
eval :: Expr -> Either String Float
eval (Val x) = Right x
eval (Mul x y) =
  let x' = eval x
      y' = eval y in whenRight x' (\x'' -> whenRight y' (\y'' -> Right $ x'' * y''))
eval (Div x y) =
  let x' = eval x
      y' = eval y in whenRight x' (\x'' -> whenRight y' (\y'' -> if y'' == 0 then Left "Division by zero!" else Right $ x'' / y''))

Then, the great community at #haskell@libera.chat told me that whenRight is basically Monad’s bind function (>>=):

eval :: Expr -> Either String Float
eval (Val x) = Right x
eval (Mul x y) =
  let x' = eval x
      y' = eval y in x' >>= (\x'' -> y' >>= (\y'' -> Right $ x'' * y''))
eval (Div x y) =
  let x' = eval x
      y' = eval y in x' >>= (\x'' -> y' >>= (\y'' -> if y'' == 0 then Left "Division by zero!" else Right $ x'' / y''))

We can further improve it by using the do notation, even though it’s really just syntactic sugar; <- is >>= and return is Right. In any case, it does help with readability.

eval :: Expr -> Either String Float
eval (Val x) = Right x
eval (Mul x y) = do
  x' <- eval x
  y' <- eval y
  Right $ x' * y'
eval (Div x y) = do
  x' <- eval x
  y' <- eval y
  if y' == 0
  then Left "Division by zero!"
  else Right $ x' / y'

Conclusion

Let’s do a quick recap.

We started with a function of type signature Expr -> Float, and then we changed it to Either String Float. This change made things more explicit at the type level, that is, it tells much more what’s going on inside the function, whereas, for Expr -> Float, we didn’t even know that error was being used. By adding this graceful error handling, whoever uses our code can choose how to handle the return value of Either, and they have the option to choose, whereas simply using error does not give them that option.

So, we first took a piece of functionality (in this case, simple error handling) and abstracted it using a monad (whenRight). This abstraction helped us make this specific calculation more explicit.

In any case, Either is just one monad. There are many other monads. One interesting bit is how you can combine these monads, say, IO with Either. Monad’s bind function is not commutative so (io >>= either) :: IO (Either x ()) is different from, e.g. (either >>= io) :: Either x (IO ()). In any case, whatever way they are combined, the explicitness is preserved.