[Haskell-cafe] Feeding a monad into itself

MarLinn monkleyon at gmail.com
Sat Jul 22 15:14:52 UTC 2017

This sounds very interesting, thank you. So if I understand correctly, 
(––>) is supposed to mean “something like implication”? So far so good, 
but I fail to grasp that in a more precise way because the law makes no 
sense to me yet. Or rather, something seems to be missing? I suppose 
it's because I don't have the mathematical perspective to get that part. 
Even such common things like “Left Adjoints” fail to click in my head, 
so they're missing on my side…

So the operations have the types

     (∧) ∷ Monad m ⇒ m a → (a → m ()) → m a

     (≤) ∷ SetLike m ⇒ m a → m a → Bool -- implicitely

     (––>) ∷ (Eq a) ⇒ m a → m a → a → m ()

Because (≤) returns something non-monadic, the only way the law makes 
sense is if it's bracketed like this:

     (x ∧ f) ≤ y  iff  f ≤ (x ––> y)

Because of the left side, f must have type (a → m ()). That makes sense 
because (x ––> y) has that same type. But now (≤) has to be defined over 
this type of functor. In other words you seem to claim this type of 
functors is “set-like”? I assume the definition is something like

     f ≤ g  iff  ∀ x.f x ≤ g x

? I'm still not sure what that would mean for the law, but it seems like 
the first step towards understanding it a bit.


More information about the Haskell-Cafe mailing list