I implemented the Idris Monad Interface by hand because I didn’t see a better way.

First one needs a “type” to hold our data. This just needs to be generic, so I’m using Mo a

data Mo: Type -> Type where
    Free: a -> Mo a

This isn’t very interesting - I’m reluctant to say it, but, it’s just a “box” for a piece of data.

To me a Monad one must implement “bind” with is done via the >>= operator. The >>= operator takes a “chunk” of logic that computes a (new) box’ed value (Mo b) from the existing value (a in Mo a) and returns a Mo b that will be that value. This is also useful for representing effects in purely functional programs. I care because it’s needed for the do-notation which implicitly uses it to separate stuff around the a <- b.

To make Mo a an implementation of`Monad we can implement it like this …

Monad Mo where
    -- (>>=): Mo a -> (f: a -> Mo b) -> Mo b
    (>>=) (Free a) f = f a

… where a is a value, and f would be f: a -> Mo b.

You’ll get an error stating that …

Can’t find implementation for Applicative Mo

… because Monad extends Applicative and one needs an implementation of Applicative.

… and Functor but that just looks like this …

Functor Mo where
    -- map: (a -> b) -> Mo a -> Mo b
    map f (Free a) = Free $ f a

… and gives you another way to bind. Applicative needs pure to create an instance and <*> to invoke a function in one instance on a value from another instance.

Applicative Mo where

    -- pure: a -> Mo a
    pure a = Free a

    -- (<*>): Mo (a -> b) -> Mo a -> Mo b
    (<*>) (Free f) (Free a) = Free (f a)

The implementations need to be in the specific order Functor, Applicative, Monad.

Finished

We now have something that looks like this …

data Mo: Type -> Type where
    Free: a -> Mo a

Functor Mo where
    -- map: (a -> b) -> Mo a -> Mo b
    map f (Free a) = Free $ f a

Applicative Mo where

    -- pure: a -> Mo a
    pure a = Free a

    -- (<*>): Mo (a -> b) -> Mo a -> Mo b
    (<*>) (Free f) (Free a) = Free (f a)

Monad Mo where
    -- (>>=): Mo a -> (f: a -> Mo b) -> Mo b
    (>>=) (Free a) f = f a

… and we can simplify it …

data Mo: Type -> Type where
    Free: a -> Mo a

Functor Mo where
    map f (Free a) = Free $ f a

Applicative Mo where
    pure = Free
    (Free f) <*> (Free a) = Free $ f a

Monad Mo where
    (>>=) (Free a) f = f a

… and that’s all I feel like saying for now.