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

[Stefan O'Rear]

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.

Stefan
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20070813/e336f356/attachment.bin