{- proof of nonexistence of join for the composition of two monads
as discussed in http://web.cecs.pdx.edu/~mpj/pubs/RR-1004.pdf

The lemma in Appendix A turns out to be wrong.

map unit : M X → M (N X)
however "MX" is not a suffix of "MNX"!

This is an alternate approach to proving that join does not exist
for the composition of two monads.
-}
module _ where

-- Empty type
data  : Set where

-- Logical negation
¬_ : Set  Set
¬ x = x  


infixr 4 _∙_       -- type application
infix 0 _⟶_ _⟶ᵏ_   -- function arrows

-- The domain of types with kind (* → *) that we'll be considering
data *→* : Set where
  M N : *→*

-- The domain of types with kind * that we'll be considering
data * : Set where
  X   : *
  _∙_ : *→*  *  *  -- type application

-- Relation on types defined in the original paper.
-- An inhabitant of (a ⟶ b) indicates that a function
-- having this type can be formed using operations defined
-- on any monad.
data _⟶_ : *  *  Set where

  -- ⟶ is a category
  id      :  {a    }  (a  a)
  compose :  {a b c}  (b  c)  (a  b)  (a  c)

  -- primitive monad operations
  map     :  {f a b}  (a  b)  (f  a  f  b)
  unit    :  {f a  }  (a  f  a)
  join    :  {f a  }  (f  f  a  f  a)


-- Here we see that the lemma does not hold:
--
-- Lemma:
-- If |- (X -> Y) then (rd X) is a suffix of (rd Y)
--
-- However:
-- MX is not a suffix of MNX
lemma-counter-example : M  X  M  N  X
lemma-counter-example = map unit


-- Isomorphic relation on types, this representation
-- eliminates the very general 'compose' rule and will
-- be easier to reason about when we prove that there's no
-- join function for the composition of two monads.
--
-- Note how each time we case on a value of this datatype
-- one of the type parameters gets smaller.
data _⟶ᵏ_ : *  *  Set where
  pure  : X ⟶ᵏ X
  bind  :  {f a b}  (a ⟶ᵏ f  b)  (f  a ⟶ᵏ f  b)
  unitᵏ :  {f a b}  (a ⟶ᵏ     b)  (    a ⟶ᵏ f  b)


-- id can be implemented in terms of pure, bind and unitᵏ
idᵏ :  {a}  (a ⟶ᵏ a)
idᵏ {X    } = pure
idᵏ {_  _} = bind (unitᵏ idᵏ)

-- compose can be implemented in terms of bind and unitᵏ
composeᵏ :  {a b c}  (b ⟶ᵏ c)  (a ⟶ᵏ b)  (a ⟶ᵏ c)
composeᵏ pure             g  = g
composeᵏ (unitᵏ f)        g  = unitᵏ (composeᵏ f g)
composeᵏ (bind  f) (bind  g) = bind (composeᵏ (bind f) g)
composeᵏ (bind  f) (unitᵏ g) = composeᵏ f g

-- Half of the proof of the isomorphism between ⟶ and ⟶ᵏ
to-k :  {a b}  (a  b)  (a ⟶ᵏ b)
to-k id            = idᵏ
to-k (compose f g) = composeᵏ (to-k f) (to-k g)
to-k (map f)       = bind (unitᵏ (to-k f))
to-k unit          = unitᵏ idᵏ
to-k join          = bind idᵏ

-- Other half of the proof of the isomorphism between ⟶ and ⟶ᵏ
-- We won't actually rely on this, but it shows that these two categories
-- relate exactly the same objects.
from-k :  {a b}  (a ⟶ᵏ b)  (a  b)
from-k pure      = id
from-k (bind  k) = compose join (map (from-k k))
from-k (unitᵏ k) = compose unit (from-k k)

-- Counter-example to the existence of a generalized join function
-- for the composition of to monads in the ⟶ᵏ category.
impossibleᵏ : ¬ (M  N  M  N  X ⟶ᵏ M  N  X)
impossibleᵏ (bind  (unitᵏ (bind  (unitᵏ ()))))
impossibleᵏ (bind  (unitᵏ (unitᵏ ())))
impossibleᵏ (unitᵏ (unitᵏ ()))

-- Proof of the lack of a generalized join function for the composition of
-- two monads via the counter-example in category ⟶ᵏ
impossible : ¬ (∀ {a}  M  N  M  N  a  M  N  a)
impossible f = impossibleᵏ (to-k f)