{- 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)