[Haskell-cafe] Article review: Category Theory

[David House]

On 17/01/07, Yitzchak Gale <gale at sefer.org> wrote:
> 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 at gmail.com