[Haskell-cafe] Feeding a monad into itself

[MarLinn]

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.

Cheers,
MarLinn