13 Aug
2007
13 Aug
'07
10:50 a.m.
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