JP Writes Code

I am an almost college student in the midwest who likes math, computers, and other interesting things

Let's Write a Monad in Idris!

24 Oct 2014

To preface this, I'm not writing another monad tutorial. There's a (not-too-far-from-the-truth) stereotype that every Haskell programmer writes their own terrible monad tutorial that I do not intend to perpetuate, and if you really want to learn monads, I would recommend first reading the excellent You Could Have Invented Monads and then writing a bunch of monadic code (Note: the second part of this is much more important than the first.) This instead assumes you have a basic idea of what a monad is, and want to get started using them in Idris.

Whenever I personally am getting started with a new topic in Idris (or most languages, really) I start by playing around with it in the REPL. :t Monad is the expression to get the type of Monad, and this returns Prelude.Monad.Monad : (Type -> Type) -> Type. :doc Monad is slightly more helpful, returning

Type class Monad


    (>>=) : Monad m => m a -> (a -> m b) -> m b

        infixl 5

    Monad id
    Monad PrimIO
    Monad IO
    Monad Maybe
    Monad (Either e)
    Monad List
    Monad (Vect n)
    Monad Stream

The most interesting thing that I personally found here is that Idris only requires one operator (>>=) to declare an instance of Monad. This is a far cry from the Haskell I learned about monads from, which requires >>=, >>, return, and fail to be defined on anything you want to make a monad. Curious, I went to the source code to learn a bit more about how exactly one can do the work of four functions with only one. The actual definition of Monad there is quite interesting:

class Applicative m => Monad (m : Type -> Type) where
(>>=) : m a -> (a -> m b) -> m b

In Idris, monads are a kind of applicatives! This actually makes a lot of sense from a category theory perspective, as monads are actually applicative, but is still slightly surprising. Since we're already looking around in Idris' source code, we may as well look at the source for Applicative which defines Applicative as:

class Functor f => Applicative (f : Type -> Type) where
pure : a -> f a
(<$>) : f (a -> b) -> f a -> f b

Notably, Applicative itself is a subclass of Functor, which also makes sense (an applicative is literally just a functor with application), and looking at one more bit of the source we can finally see all the stuff that goes into being a monad in Idris:

1 class Functor (f : Type -> Type) where
2 map : (m : a -> b) -> f a -> f b

A few things immediately become a bit clearer now that we can see how to declare a function from a type to a type a monad from start to finish. First, there actually are four operations that any monad has to have defined (map from Functor, pure and <$> from Applicative, and >>= from Monad). While those aren't the same four as Haskell, they're roughly equivalent.return is just pure, >> is quite easy to rewrite if you should want it (it's a specific case of $>, which is defined in Prelude.Applicative)(and not necessary for being a monad, technically speaking), and fail is actually not even part of the definition of a monad, and is just useful for graceful failure in pattern-matchy do expressions.

Just to ensure that I truly understood Monads in Idris, I decided to rewrite Maybe. In Haskell, for comparison:

 1 data Maybe a = Nothing
 2              | Just a
 4 instance Monad Maybe where
 5     (Just x) >>= k      = k x
 6     Nothing  >>= _      = Nothing
 8     (Just _) >>  k      = k
 9     Nothing  >>  _      = Nothing
11     return              = Just
12     fail _              = Nothing

First, Maybe is defined and then an instance of Monad is written for it. In Idris, we start the same way, by defining the type (or function to a type, really):

1 data Maybe a = Nothing
2              | Just a

So far, this is exactly the same. However, in Idris, before we can declare our instance of Monad we need an instance of Applicative, for which we need an instance of Functor.

1 instance Functor Maybe where
2     map f (Just x) = Just (f x)
3     map f Nothing = Nothing

Then we can define Applicative:

1 instance Applicative Maybe where
2     pure = Just
4     (Just f) <$> (Just a) = Just (f a)
5     _ <$> _ = Nothing

And finally Monad:

1 instance Monad Maybe where
2     Nothing >>= k = Nothing
3     (Just x) >>= k = k x