[Haskell-cafe] Re: a regressive view of support for imperative programming in Haskell

[apfelmus]

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