apfelmus wrote:
My assumption is that we have an equivalence
forall a,b . m (a -> m b) ~ (a -> m b)
because any side effect executed by the extra m on the outside can well be delayed until we are supplied a value a. Well, at least when all arguments are fully applied, for some notion of "fully applied"
I figured that wouldn't be a problem since our values don't escape, and the functions we define all respect the embedding... More formally:
Projections and injections:
Stefan O'Rear wrote: proj :: Monad m => m (a -> m b) -> (a -> m b)
proj ma = \x -> ma >>= \fn' -> fn' x inj fn = return fn
Define an equivalence relation:
ma ≡ mb <-> proj ma = proj mb
Projection respects equivalence:
ma ≡ mb -> proj ma = proj mb (intro ->) ma ≡ mb => proj ma = proj mb (equiv def) proj ma = proj mb => proj ma = proj mb (assumption)
Application respects equivalence:
Yeah, that's the right approach, but it has a few typos. The correct version is (@) :: Monad m => m (a -> m b) -> m a -> m b (@) ma = \x -> x >>= proj ma Formulating (@) in terms of proj ma is a very clever idea since it follows immediately that ma @ x = ma' @ x iff proj ma = proj ma' iff ma ≡ ma' In other words, when viewed through @ and proj only, equivalent actions give equivalent results. The main point is that this does not hold for the other curry-friendly type m a -> m b proj :: Monad m => (m a -> m b) -> (a -> m b) proj f = f . return (@) :: Monad m => (m a -> m b) -> m a -> m b (@) = id ma ≡ ma' iff proj ma = proj ma' since those functions may execute their argument multiple times. So, here's the counterexample once :: Monad m => m A -> m A once = id twice :: Monad m => m A -> m A twice x = x >> once x Now, we have proj once = return = proj twice but effect :: IO () -- a given effect effect = putStrLn "Kilroy was here!" once @ effect = effect ≠ twice @ effect = effect >> effect The same can be done for several arguments, along the lines of proj2 :: m (a -> m (b -> m c)) -> (a -> b -> m c) proj2 f = proj . (proj f) app2 :: m (a -> m (b -> m c)) -> (m a -> m b -> m c) app2 f mx my = (f @ mx) @ my = my >>= proj (mx >>= proj f) = my >>= \y -> mx >>= \x -> proj2 f x y and similar results. Regards, apfelmus