[Haskell-cafe] Re: Very freaky

[Al Falloon]

This is the best intro to category theory I have ever heard. I finally 
understand. Thank you.

Dan Piponi wrote:
> I thought I'd dive in with a comment to explain why category theory is
> an important subject and why it often crops up in Haskell programming.
> The key thing is this: in many branches of mathematics people draw
> what are known as commutative diagrams:
> http://mathworld.wolfram.com/CommutativeDiagram.html
> 
> So what do these diagrams represent? The letters at the 'vertices'
> (known as objects) often represent sets and the arrows represent
> functions. But in different branches of mathematics the same diagrams
> appear with the objects and arrows having a quite different
> interpretation. For example you could use a diagram like 1 -> 2 to
> mean 1<2. Or you could use X -> Y to mean X implies Y. Or in {1,2} ->
> {4,5,6} the arrow might mean containment and so on. But here's a
> remarkable fact: you can often take a definition in one branch of
> mathematics and write it diagrammatically. You can then reinterpret
> that diagram in a different branch of mathematics as different
> definition. Sometimes the new definition isn't interesting, but often
> it is. So now you can define things in multiple branches of
> mathematics at the same time. It gets better. Statements of theorem
> can also sometimes be written in purely diagrammatic language so a
> theorem that holds in one branch of mathematics turns out to be an
> interesting theorem in another. Sometimes the entire proof can be
> written diagrammatically meaning you can solve problems in different
> branches of mathematics at the same time. This whole
> 'multidisciplinary' subject is known as Category Theory.
> 
> To a good approximation (and there is a certain amount of choice over
> which approximation you pick) Haskell also forms a category. The
> objects are types and the arrows are functions. But as I've also
> hinted above, objects can represent propositions and arrows can
> represent implication. So that suggests theorems about logic might
> carry over to theorems about Haskell. They do, as has been mentioned
> in another thread. But that's a special case of a much wider
> phenomenon where constructions in different parts of mathematics can
> feed into Haskell.
> 
> So knowing category theory can help you to bring to bear mathematical
> knowledge from other fields when writing Haskell code. A big example
> of that payoff has been the notion of a monad. But there are many
> more.
> 
> It also works the other way too. As you acquire a grasp of Haskell you
> get insight into other parts of mathematics and computer science, even
> if you don't yet know it! Haskell has certainly helped me this way.
> (And I should confess that this is one of my primary motivations for
> learning it.)