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.