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
Parameters:
m
Methods:
(>>=) : Monad m => m a -> (a -> m b) -> m b
infixl 5
Instances:
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
3
4 instance Monad Maybe where
5 (Just x) >>= k = k x
6 Nothing >>= _ = Nothing
7
8 (Just _) >> k = k
9 Nothing >> _ = Nothing
10
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
3
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
```