[Haskell-cafe] Re: a regressive view of support for imperative
programming in Haskell
apfelmus
apfelmus at quantentunnel.de
Tue Aug 14 03:53:33 EDT 2007
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
More information about the Haskell-Cafe
mailing list