Monad implies Applicative: pure needs to be implemented

[kaelte]

In order to prove that every Monad is an Applicative we cannot simply use pure to implement (<*>) because pure is a requirement of Applicative, see exercise 3.2:

idris2-tutorial/src/Tutorial/Functor.md

Lines 1238 to 1240 in b3264e0

	2. `Monad` extends `Applicative`, because every `Monad` is
	also an `Applicative`. Proof this by implementing
	`(<*>)` in terms of `(>>=)` and `pure`.

We could use pure if we also implemented pure in terms of (>>=) and join without (<*>).

[stefan-hoeck]

Agreed. This exercise should be reworded. Traditionally (in Haskell), Monad came with its own version of pure called return for historical reasons.

[kaelte]

Given that (<*>) can be implemented in terms of (>>=) and (<$>) without using pure
we can say that Monad + pure implies Applicative.
I have not figured out how to implement pure in terms of (>>=) and (<$>);
I have the feeling that this is not possible.

[kaelte]

Since Applicative is a constraint for Monad we would not need to prove that every Monad extends Applicative.
But for the sake of learning we could assume the Applicative were not a constraint.

This leads to an question:

Why is Functor a constraint for Applicative?
We can prove that every Applicative is a Functor
as we could add a default implementation to the interface Applicative
of map in terms of pure and (<*>):

idris2-tutorial/src/Tutorial/Functor.md

Lines 1237 to 1239 in b5d4246

	1. `Applicative` extends `Functor`, because every `Applicative`
	is also a `Functor`. Proof this by implementing `map` in
	terms of `pure` and `(<*>)`.

But maybe having Functor as constraint for Applicative simplifies the live of the compiler.