[Haskell-cafe] Category theory as a design tool

[Alexander Solla]

On Wed, Jun 22, 2011 at 12:06 AM, Arnaud Bailly <arnaud.oqube at gmail.com>wrote:

> Thanks Sebastien,
> This paper has passed in my radar's field but I must confess that
> although I think I grasped the idea, I was quickly lost in the
> profusion of symbols and notations. I am no mathematician, only a
> simple developer, although I am fascinated by several topics in
> mathematics so my attention tend to drop sharply when confronted with
> more or less complex proofs and layers of defintions and mappings.
>

Please read http://en.wikipedia.org/wiki/Abstract_interpretation .  Keep in
mind that it applies to /all/ formal languages, including programming
languages and the languages of mathematics.

There are two hard phases of becoming a mathematician:  understanding the
symbolism, and understanding when/how to skip over new symbolism/notation.
 After all, every mathematician is taught a slightly different version of
mathematics.  If we are to communicate with each other, we have to elide the
differences.  "Abstract interpretation" is a formal method of doing that for
computer languages.  It also helps when you understand the relationships
between theorems, free functions, free structures, and so on.  (I.e., they
are the same things seen from different points of view, and always can be
skipped when trying to interpret/understand, because they are always "true")

If you're looking for books on the subject, take a look at Topoi:  The
Categorical Analysis of Logic.  It isn't a book /about/ category theory (it
has a decent introduction), but it builds up various logics using
categorical constructs.  It aims to show that Category  theory can become a
"foundation" for mathematics.  But since every constructive logic *is a*
programming language, it builds up the theory of computation in a very
general way.

Also, I would suggest drawing diagrams to represent your programs during the
design phase.  Use your own notation if you don't know the 'standard'
notation for an idea.  A fair bit of category theory is "refactoring" these
ad hoc diagrams into pieces that each express a single idea, at least to get
the intuition behind the single ideas taken together.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110622/e4a7e040/attachment.htm>