
On 17/01/07, Yitzchak Gale
A few semicolons were missing in the do blocks of the Points-free style/Do-block style table. I fixed that. I think it would be simpler without the do{} around f x and m - are you sure it's needed?
They're not needed, but I think it makes it more symmetric. It also clarifies that we're talking about moving things around within do-blocks; one could potentially have statements before and after the given statements. There isn't much of a case either way, I guess.
You wrote: "category theory doesn't have a notion of 'polymorphism'". Well, of course it does - after all, this is "abstract nonsense", it has a notion of *everything*. But obviously we don't want to get into that complexity here. Here is a first attempt at a re-write of that paragraph:
Note: The function id in Haskell is 'polymorphic' - it can have many different types as its domain and range. But morphisms in category theory are by definition 'monomorphic' - each morphism has one specific object as its domain and one specific object as its range. A polymorphic Haskell function can be made monomorphic by specifying its type, so it would be more precise if we said that the Haskell function corresponding to idA is (id :: A -> A). However, for simplicity, we will ignore this distinction when the meaning is clear.
I've changed the paragraph to almost what you said, modulo a few tweaks to make it sit nicer with the rest of the article.
It is nice that you gave proofs of the >>= monad laws in terms of the join monad laws. I think you should state more clearly that the two sets of laws are completely equivalent. (Aren't they?) Maybe give the proofs in the opposite direction as an exercise.
Yes, they are, here are my proofs: join . fmap join = join . join join . fmap join (\m -> m >>= id) . fmap (\m -> m >>= id) \m -> (m >>= (\n -> return (n >>= id))) >>= id \m -> m >>= (\n -> return (n >>= id) >>= id) \m -> m >>= (\n -> id (n >>= id)) \m -> m >>= (\n -> n >>= id) \m -> m >>= (\n -> id n >>= id) \m -> (m >>= id) >>= id \m -> join m >>= id \m -> join (join m) join . join join . fmap return = id join . fmap return (\m -> m >>= id) . (\m -> m >>= return . return) \m -> (m >>= return . return) >>= id \m -> m >>= (\n -> return (return n) >>= id) \m -> m >>= (\n -> id (return n)) \m -> m >>= (\n -> return n) \m -> m >>= return \m -> m id join . return = id join . return (\m -> m >>= id) . (\m -> return m) \m -> return m >>= id \m -> id m id return . f = fmap f . return return . f (\x -> fmap f x) . return \x -> fmap f (return x) \x -> return x >>= return . f \x -> (return . f) x return . f join . fmap (fmap f) = fmap f . join join . fmap (fmap f) (\m -> m >>= id) . (\m -> m >>= return . (\n -> n >>= return . f)) \m -> (m >>= return . fmap f) >>= id \m -> (m >>= \x -> return (fmap f x)) >>= id \m -> m >>= (\x -> return (fmap f x) >>= id) \m -> m >>= (\x -> id (fmap f x)) \m -> m >>= (\x -> fmap f x) \m -> m >>= (\x -> x >>= return . f) \m -> m >>= (\x -> id x >>= return . f) \m -> (m >>= id) >>= return . f (\m -> m >>= id) >>= return . f fmap f . (\m -> m >>= id) fmap f . join I've added the suggested exercise. -- -David House, dmhouse@gmail.com