(x→p)→q as a monad

From the post here.

Given F x = (x→p)→q for some fixed p and q, can we show that it is or isn't a monad?

---

We have to assume the existence of function k: p→q for pure to exist, and we have to assume the existence of function h: q→p for (>>=) to exist.

pure x = k . ($ x)

- there is no other way to construct a value of type q from a function of type x→p, you have to have a k: p→q.

Then:

m >>= f = m . (h .) . flip f

- there is no other way to construct a function of type (x→p) from a function of type x→(y→p)→q, you have to have an h: q→p.

Associativity of (>>=) follows from associativity of composition. How about the unit laws?

pure x >>= f = f x -- unit-1

pure x >>= f = k . ($ x) . (h .) . flip f = k . (h .) . f x = (k . h) . f x

- this should be f x if k . h = id.

So k is a surjection.

m >>= pure = m -- unit-2

m >>= pure = m . (h .) . (k .) $ flip ($) = m . ((h . k) .) $ id = m . (h . k)

- this should be m if h . k = id.

So k is an injection at the same time - p and q must be isomorphic.