{- 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  _∙_       -- type application
infix  _⟶_ _⟶ᵏ_   -- 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)