Monadically Speaking: Adventures in PLT Wonderland

January 16, 2009

Learning Haskell through Category Theory, and Adventuring in Category Land: Like Flatterland, Only About Categories

Filed under: Category Theory, Haskell — Benjamin L. Russell @ 8:55 pm

Two days ago, there was an interesting post by Andrzej Jaworski, entitled “[Haskell] Teach theory then Haskell as example,” dated “Wed, 14 Jan 2009 04:37:33 +0100,” on the Haskell mailing list on the Haskell programming language, recommending that Haskell be taught “on most abstract terms in a framework of higher order logic, types and CT right from the start.”  While I agreed with the gist of his post, I hadn’t found an appropriate publication on category theory that addressed the subject at the proper pace, level, and perspective.  Most publications did not explain enough detail, assumed too many topics not covered, or did not explain the concepts in a manner which would allow me to form a visual framework of reference in my mind.  In my response, I listed the following publications on category theory, a branch of mathematics which forms a theoretical framework for Haskell. (Author names and dates have been added, explicit URL’s replaced by hyperlinks in titles, and descriptions expanded, for referential convenience. In addition, I have added one additional book entry for cross-referential purposes.):

Category Theory Books:

Conceptual Mathematics: A First Introduction to Categories (Paperback)
by F. William Lawvere (author) and Stephen Hoel Schanuel (author)
Cambridge: Cambridge University Press, 1997
An elementary introduction to category theory

An introduction to category theory in four easy movements
by A. Schalk (author) and H. Simmons (author)
Manchester: A. Schalk and H. Simmons, October – December, 2005
A somewhat informal, reportedly in-depth introduction to category theory, which some students have described as being intricately layered. Personally, I like Harold Simmons style, because it seems to have more personality than that of many other authors on category theory. Sometimes he is actually funny; e.g., he writes (see p. 6),

“In the original examples of categories the arrows were morphisms which were then called homomorphism, and it wasn’t realized that this family could be very large. (Some out and out category theorists still don’t realize the significance of this. On the other hand, some off the wall set theorists don’t realize the significance of category theory.)”

I’ve heard of the UNIX wars and the editor wars, but now we have the category theory vs. set theory wars! The more some things change, the more they stay the same….

Category Theory by Magic: A short introduction to the basics of category theory
by Harold Simmons
Manchester: Harold Simmons, November 29, 2008
A somewhat more advanced text than An introduction to category theory in four easy movements, intended specifically for “postgraduate students,” but written in an exceptionally clear style.

Toposes, Triples and Theories
by Michael Barr and Charles Wells
Michael Barr and Charles Wells, 2000
An often-referenced introduction to category theory, intended for graduate students, reportedly
discussing monads as “triples.”  This book is a sequel to Category Theory for Computing Science, by the same author. This is one of the publications listed in the bibliography by Simmons in Category Theory by Magic: A short introduction to the basics of category theory.

Category Theory for Computing Science (Third Edition)
by Michael Barr and Charles Wells
Hertfordshire, U.K.: Prentice Hall International (UK) Ltd., 1999
Prequel to Toposes, Triples and Theories, “written specifically to be read by researchers and students in  computing science.”    Apparently, only available in dead-tree format.  Can be ordered from Centre de recherches mathématiques, or by e-mail to crmbooks@crm.umontreal.ca.  Often cited in the literature.

Categories and Computer Science
by R. F. C. Walters
Cambridge: Cambridge University Press, August 1992
Reportedly a straightforward introduction to category theory, with many examples from computer science

Arrow, Structures and Functors – The Categorical Imperative (no hyperlink available)
According to the HaskellWiki page on category theory, an out-of-print book covering monads and the Yoneda lemma, with very little prerequisite knowledge

Category Theory
by Steve Awodey
Oxford: Oxford University Press, 2006
This text aims to minimize mathematical prerequisites in providing an introduction to category theory for students in such topics as computer science, logic, linguistics, cognitive science, or philosophy, who may not necessarily be working (or aspiring) mathematicians. Students are not assumed to have much background in mathematics beyond a course in discrete mathematics and some calculus or linear algebra or logic.

The book starts out with a few basic examples of posets and monoids, and then develops them in further detail. While the book assumes little in mathematical prerequisites, it does not sacrifice rigor, and covers categories, functors, natural transformations, equivalence, limits and colimits, functor categories, representables, Yoneda’s lemma, adjoints, and monads. Optional topics covered include cartesian closed categories and the lambda calculus. However, 2-categories and monoidal categories are purposely excluded, and toposes are not covered in any depth.

Two aspects that I like about this book are the author’s style of starting out with examples from and references to set theory (although it is true that arrows, not objects, are the focus in category theory, many students come from a set-theoretical background, and references to set theory can ease the transition), and offering occasional examples from computer science. For instance, Example 10 on page 11 provides a case in which a functional programming language L is given and an associated category is shown where the objects are the data types of L, the arrows are the computable functions of L (“processes,” “procedures,” and “programs”), the composition of two programs, f mapping X to Y, and g mapping Y to Z, “is given by applying g to the output of f,” and the identity is the “do nothing” program. Such examples help tie the subject to computer science (in particular, to functional programming), and help render the subject more appealing to students of functional programming.

Category Theory Lecture Notes:

Category Theory Lecture Notes for ESSLLI
by Michael Barr and Charles Wells
Michael Barr and Charles Wells, 1999
Condensed version of Category Theory for Computing Science, discussing category theory from a computer science perspective

A Gentle Introduction to Category Theory – the calculational approach
by Maarten M. Fokkinga
Amsterdam: M. M. Fokkinga, 1992 (version of June 6, 1994)
Another set of lecture notes referenced on the HaskellWiki page on category theory

Categorical Programming with Examples in Haskell:

Categorical Programming with Inductive and Coinductive Types
by Varmo Vene
Tartu, Estonia: Varmo Vene, 2000 (Ph.D. dissertation)
A thesis on categorical programming, exploring inductive and coinductive types, and several programming constructs related to them in Haskell

In conclusion, I stated as follows:

I would believe that having specific Haskell code to help interact
with the categorical examples would help to motivate study of the
abstract theory for many programmers.  One problem that many people
have with studying abstract theory in isolation is that they often
tend to lose motivation unless they can see how the theory directly
relates to and influences the semantics and data structures in the
code.  Having specific examples of Haskell code to tie together
immediately with the abstract theory would most likely help to
motivate and maintain interest.

Then I discovered a similar thread in the USENET newsgroup comp.lang.haskell which had originated two days earlier, entitled “Book recommendations on underlying theory,” dated “Sun, 11 Jan 2009 15:11:40 -0800 (PST),” in which a reader nicknamed “grimey” was asking for recommended readings on the theory behind Haskell.  Grimey described himself as a programmer who had “studied physics at the undergrad level,” and whose mathematical background included “Diff & Integ. Calc, Linear Algebra, Diff Eq, Advanced (Vector) Calc, [and] Complex Analysis.”  In particular, he added,

Although the Vector Calc class was particularly difficult
for me and sort of “took the wind out of my sails” and leaving me
adrift on the sea of mathematics for a long time.  I always wanted to
continue on with more abstract math, like algebra and group theory, to
gain understanding of the beauty behind quantum physics; but for
various reasons, that didn’t happen.  Anyway years later I still use
Linear Algebra and Diff Eq quite frequently for work, and have a good
practical engineer’s grasp of those topics.  I use advanced calculus
less frequently and I use quaternions for very practical, non-
theoretical way for rotation sequences in 3D.  I am an expert C/C++
programmer.

He then mentioned the following books as two that had “piqued [his] interest,” before asking for further suggestions:

Topics In Algebra
by I.N. Herstein
Xerox Corporation: 1975

Lambda-Calculus and Combinators
by J. Roger Hindley and Jonathan P. Seldin
Cambridge: Cambridge University Press, 2008

In my response linking the two threads, I mentioned Andrzej Jaworski’s response to my earlier posting in the first thread, in which he had replied in part that:

[T]here are many very good
articles addressing specific issues of Haskell's theoretical foundations (e.g.
http://www.cs.ut.ee/~varmo/papers/thesis.pdf).  They however always assume more than they target to
explain making student turn around them like a dog not knowing which ball to catch first.

I.e., the problem was that many such papers depended on parts of other papers, which either depended on other parts of the first paper, or on parts of still other papers.  Then I mentioned a response to this issue that I had received in a private e-mail message from a reader of the first thread, in which that reader had written that:

… the problem “comes from trying to use academic papers as textbooks, a
purpose for which they’re not usually designed.”

I then added that this was the gist of the problem, and, as a possible solution, added a dead-tree-based book that I had read about earlier (already mentioned above):

Conceptual Mathematics: A First Introduction to Categories (Paperback)
by F. William Lawvere and Stephen Hoel Schanuel
Cambridge: Cambridge University Press, 1997
An elementary introduction

I added:

This book is reputed to be interesting even to non-mathematicians at a
philosophical level.  I myself have purchased a copy.

Then, on an afterthought, in an additional post immediately afterwards, I added that what would be even better would be a mathematical storybook (separate links to the storybooks hyperlinked in the following quoted portion):

What would be especially interesting would be an introductory storybook on category theory:  a book similar to, say, Flatland, by Edwin Abbott Abbott, or even Flatterland, by Ian Stewart.  These books would elevate category theory out of the realm of dry equations into a story which would keep me awake with suspense reading through the night.

Yes!  What we need is Category Land:  Like Flatterland, Only About Categories.  If only a book were so.  Any suggestions?

16 Comments »

  1. [...] Benjamin Russell posts on learning Haskell through Category Theory here. [...]

    Pingback by Learning Haskell through Category Theory | Wisdom and Wonder — January 20, 2009 @ 12:39 pm | Reply

  2. [...] or deepen them.  The latter has already been discussed in another blog post of mine here, “Learning Haskell through Category Theory, and Adventuring in Category Land: Like Flatterland, Only A…“; here I discuss the [...]

    Pingback by Motivating Category Theory for Haskell for Non-mathematicians « Benjamin L. Russell’s Adventures in Programming Language Theory Wonderland — January 20, 2009 @ 5:05 pm | Reply

  3. A possible starting-point for a categorical Flatland-alike might be my bridges and islands metaphor. I was thinking of extending it so that the bridge geeks had a long-standing feud with a tribe of mountaineers with thousand-yard stares and scars from their oxygen masks, but who were almost indistinguishable from the bridge geeks to outsiders – these would be set theorists, of course. The archipelago would have been settled in waves: starting with the island of finite sets, they explored surrounding islands slowly over centuries, then finally found their way to the category of sets about a hundred years ago, where their civilization thrived, allowing the exploration of islands that were further and further away (but not, for some reason, giving much thought to the bridges they were using to get there…).

    Comment by pozorvlak — January 20, 2009 @ 10:59 pm | Reply

  4. Wow. “Haskell” is listed five (5) times in the first sentence! ;-)

    Comment by Amused — January 21, 2009 @ 1:46 am | Reply

  5. [...] January 20, 2009 at 5:03 pm · Filed under Uncategorized [From Learning Haskell through Category Theory, and Adventuring in Category Land: Like Flatterland, Only A...] [...]

    Pingback by Learning Haskell through Category Theory, and Adventuring in Category Land: Like Flatterland, Only About Categories « Benjamin L. Russell’s Adventures in Programming Language Theory Wonderland « The other side of the firewall — January 21, 2009 @ 7:03 am | Reply

  6. On Tue, 20 Jan 2009 @ 10:59 pm, pozorvlak wrote:

    >A possible starting-point for a categorical Flatland-alike might be my bridges and islands metaphor.
    >I was thinking of extending it so that the bridge geeks had a long-standing feud with a tribe of
    >mountaineers with thousand-yard stares and scars from their oxygen masks, but who were
    >almost indistinguishable from the bridge geeks to outsiders – these would be set theorists, of
    >course. The archipelago would have been settled in waves: starting with the island of finite sets,
    >they explored surrounding islands slowly over centuries, then finally found their way to the category
    >of sets about a hundred years ago, where their civilization thrived, allowing the exploration of islands
    >that were further and further away (but not, for some reason, giving much thought to the bridges
    >they were using to get there…).

    Fascinating. In particular, I like the concept of a set theorist vs. category theorist feud, since set theorists and category theorists apparently tend to disagree in their approaches.

    What would the feud concern?

    Incidentally, on your Web site, you describe the islands as “categories,” and the bridges as “functors,” but since functors, strictly speaking, are morphisms in the category of small categories, it would seem that you should probably qualify the islands as “small categories.” In fact, if you are setting up a feud between mountaineers as set theorists on the islands and bridge geeks as category theorists, you may wish to call the islands “sets.”

    You would probably enjoy reading Flatterland. That book is also a highly mathematical story involving specific structural aspects of abstract entities.

    Comment by Benjamin L. Russell — January 21, 2009 @ 3:05 pm | Reply

  7. I would also recommend Awodey’s “Category Theory”, as a text which was written to minimise prerequisites, while developing some of the more important examples of categories internally to the book. It also has the advantage of containing quite a bit which is relevant to computer scientists, such as a development of the lambda calculus in the setting of Cartesian closed categories, and a good bit of discussion of categorical logic (which is closely tied to type theory).

    Comment by Cale Gibbard — January 23, 2009 @ 9:47 am | Reply

  8. >I would also recommend Awodey’s “Category Theory”, as a text which was written to minimise
    >prerequisites, while developing some of the more important examples of categories internally to the
    >book. It also has the advantage of containing quite a bit which is relevant to computer scientists,
    >such as a development of the lambda calculus in the setting of Cartesian closed categories, and a
    >good bit of discussion of categorical logic (which is closely tied to type theory).

    Thank you for the recommendation.

    I just checked out the Amazon.com entry for this book, but was disappointed to find that I had apparently missed an on-line .pdf format of Awodey’s manuscript, according to a comment by Jason Schorn “j schorn” posted there. This book has a listed price there of USD $124, but as a book collector, I would still prefer a new copy, which I can’t afford right now.

    I just performed a search on Google to find the on-line .pdf format copy of Awodey’s manuscript, but without luck…. You wouldn’t, perchance, happen to know where it resides now, would you?

    Comment by Benjamin L. Russell — January 23, 2009 @ 4:03 pm | Reply

  9. Hi,

    I’ve posted some links on my blog (blog.mestan.fr) giving the two following papers :
    * An introduction to category theory, category theory monads, and their relationship to functional programming, Jonathan M.D. Hill and Keith Clarke : http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.53.6497&rep=rep1&type=pdf
    * Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire, Erik Meijer, Maarten Fokkinga and Ross Paterson (I know this one is already well-known, but how would have it been possible to deal without this one ?!) : http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.41.125&rep=rep1&type=pdf

    Comment by alpmestan — March 2, 2009 @ 2:49 am | Reply

    • Hi alpmestan,

      Thank you for the two references. I was actually aware of the paper by Meijer, Fokkinga, and Paterson (the banana paper), but had not posted it because it was heavy on algebraic notation (the reason for its title, in fact), and did not use any commutative diagrams; most papers on category theory use the diagrams. Personally, I find the diagrams somewhat easier to grasp than just the algebraic notation. This is not to say that I am partial to diagrams; however, I would prefer some visual supplement to the algebraic notation.

      I was not aware of the paper by Hill and Clarke. Briefly glancing at the paper, it seems that the many diagrams offer a means to visualize such concepts as natural transformations (I like the phrase “sliding between categories,” and the three-dimensional diagram listed, as well as the diagrammatic representations of commutativity and associativity).

      One slight problem with the paper is that the authors use the term “computation” without fully defining it; when they say “a function that performs a computation,” what kind of “computation” do they really mean?

      Actually, Gregg Reynolds echoes similar thoughts in his blog “The Syntactic Century: “Computation” considered harmful. “Value” not so hot either.,” as follows:

      The term “computation” has at least six different senses, all of which are commonly used in technical literature:

      * a dynamic computing process
      * the result of a computational process
      * an algorithm that describes a computational process
      * a formal description of an algorithm in a specific language
      * a formal description of the semantics of a computational process; e.g. a lambda expression
      * a dynamic process that converts a lambda expression to normal form
      * a formal description of lambda conversion

      One could probably come up with additional technical uses for the term. Even worse, “computation” is an ordinary word with well-understood if inexact semantics. Readers come to a technical text with a well-formed idea of what the word means, and thus no reason to think their notion is incorrect.

      For example, Hill and Clarke (see p. 8 of their paper, third line from the bottom to second line from the bottom) write as follows:

      … if an object A has the type alpha, then the object T(A) have [sic] the type M alpha; where M is a type constructor that represents a “computation”.

      Which definition of “computation” is used here?

      Comment by Benjamin L. Russell — March 3, 2009 @ 4:34 pm | Reply

  10. Hi alpmestan,

    While searching for a version of your link to the downloadable PDF file for “Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire,” by Erik Meijer, Maarten Fokkinga, Ross Paterson which would display immediately in my browser, I discovered the following thread on the Haskell mailing list on category theory publications:

    [Haskell] Re: category theory (Frank Christoph christo at nextsolution.co.jp: Thu, 15 Oct 1998 18:27:51 +0900)
    http://www.mail-archive.com/haskell@haskell.org/msg02878.html

    There, I came across the following new references (some of the links were broken, so I did some research and was able to update the links below) (I have rephrased the link references below to place the titles before the author names of the related publications):

    “An Introduction to Categories in Computing,” by C. Barry Jay:
    https://wiki.ittc.ku.edu/lambda/images/f/fd/CategoriesInComputing-BarryJay.pdf

    “A Categorical Manifesto”, by Joseph Goguen, Mathematical Structures in Computer Science, Volume 1, Number 1, March 1991, pages 49-67:
    http://cs.ucsd.edu/~goguen/pps/manif.ps

    (Incidentally, the “new book by F. Lawvere and Stephen someone … which takes a very, very elementary and IMO unorthodox approach” is in fact the _Conceptual Mathematics: A First Introduction to Categories (Paperback)_ book, by F. William Lawvere (Author), Stephen Hoel Schanuel (Author), already mentioned in my post.)

    Comment by Benjamin L. Russell — March 3, 2009 @ 7:55 pm | Reply

    • Thank you for the link.

      Unfortunately, since this is a limited book preview, not all pages are available. Do you have any references for a full PDF or HTML file (a new paper copy would cost $124 from Amazon.com, and I would rather not purchase a pre-owned copy)?

      Incidentally, Awodey’s approach in introducing category theory at the beginning of his text is rather unusual; he starts out by giving various set-theoretic examples specifying the objects instead of the arrows, such as “all finite sets and functions between them,” or “the subset of f^(-1)(b) subset-of A that has at most two elements (rather than one)” (both on page 5). This approach contrasts sharply with, for example, the one taken by Harold Simmons in An introduction to category theory in four easy movements, in which Simmons starts out by listing, in a table, such examples as “Category: Set; Objects: sets; Arrows: functions” and “Category: RelA; Objects: sets; Arrows: binary relations” (coincidentally, both in the chart on page 5 in this text as well), where the objects don’t matter, and only the arrows matter.

      Although Awodey does later clarify (on page 8) that “One important slogan of category theory is, It’s the arrows that really matter!,” he doesn’t start in this vein until this point. Since category theory really focuses on the arrows, and not the objects, one might argue that Awodey’s approach is unorthodox.

      Nevertheless, I still find that Awodey’s approach does have its advantages. One difficulty that I have experienced with many treatments of category theory is that since they usually start out by emphasizing the arrows and discounting the objects, I have found it difficult to get used to this style of exposition, since I usually think in set-theoretic terms.

      Personally, after reading the first few pages, I find Awodey’s approach easier to get used to, since it is more similar to the approach taken by most set-theoretic books. While some may argue that this approach starts me off in the wrong frame of mind, I find it similar to getting my feet wet before jumping into a pool, rather than jumping straight into the pool.

      Comment by Benjamin L. Russell — July 16, 2009 @ 2:41 pm | Reply

  11. [...] describing how he overcame his math phobia and found his love for abstract mathematics. In Learning Haskell through Category Theory, and Adventuring in Category Land: Like Flatterland, Only A… Russell also includes literature on category [...]

    Pingback by Nice Introduction to Category Theory « Learntofish's Blog — July 22, 2009 @ 2:25 am | Reply


RSS feed for comments on this post. TrackBack URI

Leave a comment

Blog at WordPress.com.