[Haskell-cafe] Very freaky
Dan Piponi
dpiponi at gmail.com
Thu Jul 12 17:07:47 EDT 2007
On 7/12/07, Andrew Coppin <andrewcoppin at btinternet.com> wrote:
> Stefan O'Rear wrote:
> > On Thu, Jul 12, 2007 at 07:19:07PM +0100, Andrew Coppin wrote:
> >
> >> I'm still puzzled as to what makes the other categories so magical that
> >> they cannot be considered sets.
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.)
--
Dan
More information about the Haskell-Cafe
mailing list