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

[apfelmus]

Stefan O'Rear schrieb:
> On Mon, Aug 13, 2007 at 04:35:12PM +0200, 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"
> 
> (\a x -> a >>= ($ x)) ((\f -> return f) X) ==> (β)
> (\a x -> a >>= ($ x)) (return X)           ==> (β)
> (\x -> (return X) >>= ($ x))               ==> (monad law)
> (\x -> ($ x) X)                            ==> (β on the sugar-hidden 'flip')
> (\x -> X x)                                ==> (η)
> X
> 
> Up to subtle strictness bugs arising from my use of η :), you're safe.

Yes, but that's only one direction :) The other one is the problem:

  return . (\f x -> f >>= ($ x)) =?= id

Here's a counterexample

  f :: IO (a -> IO a)
  f = writeAHaskellProgram >> return return

  f' :: IO (a -> IO a)
  f' = return $ (\f x -> f >>= ($ x)) $ f
  ==> (β)
   return $ \x -> (writeAHaskellProgram >> return return) >>= ($ x)
  ==> (BIND)
   return $ \x -> writeAHaskellProgram >> (return return >>= ($ x))
  ==> (LUNIT)
   return $ \x -> writeAHaskellProgram >> (($ x) return)
  ==> (β)
   return $ \x -> writeAHaskellProgram >> return x

Those two are different, because

  clever  = f  >> return () = writeAHaskellProgram
  clever' = f' >> return () = return ()

are clearly different ;)

Regards,
apfelmus