Stefan O'Rear wrote:
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:
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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
