[Haskell-cafe] Re: a regressive view of support for imperative
programming in Haskell
Stefan O'Rear
stefanor at cox.net
Mon Aug 13 12:10:43 EDT 2007
On Mon, Aug 13, 2007 at 05:39:34PM +0200, apfelmus wrote:
> 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 ;)
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 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:
(@) ma1 = \x -> join (proj ma1 x)
Application respects equivalence:
ma1 ≡ ma2 -> (@) ma1 = (@) ma2 (intro ->)
ma1 ≡ ma2 => (@) ma1 = (@) ma2 (β)
ma1 ≡ ma2 => (\x -> join (proj ma1 x)) = (\x -> join (proj ma2 x)) (extensionality)
ma1 ≡ ma2 => join (proj ma1 x) = join (proj ma2 x) (application respects = left)
ma1 ≡ ma2 => proj ma1 x = proj ma2 x (application respects = right)
ma1 = ma2 => proj ma1 = proj ma2 (lemma)
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/2e088453/attachment.bin
More information about the Haskell-Cafe
mailing list