Re: [Haskell-cafe] Very freaky

On 7/12/07, Andrew Coppin
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

On Thu, 2007-07-12 at 14:07 -0700, Dan Piponi wrote:
On 7/12/07, Andrew Coppin
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?
Equations.
To a good approximation (and there is a certain amount of choice over which approximation you pick) Haskell also forms a category.
Haskell does form a category. To a good approximation Haskell forms a -nice- category.

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.)
participants (3)
-
Al Falloon
-
Dan Piponi
-
Derek Elkins