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
signature.asc
Description: Digital signature
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
