Learning Haskell through Category Theory, and Adventuring in Category Land: Like Flatterland, Only About Categories
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 theoryAn 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 scienceArrow, 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 knowledgeCategory 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 perspectiveA 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 theoryCategorical 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: 1975Lambda-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?
Trackbacks & Pingbacks
- Learning Haskell through Category Theory | Wisdom and Wonder
- Motivating Category Theory for Haskell for Non-mathematicians « Benjamin L. Russell’s Adventures in Programming Language Theory Wonderland
- 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
- Nice Introduction to Category Theory « Learntofish's Blog
- Category Theory for the Mathematically Impaired: An Outline of A Short Reading List for “Mathematically-impaired Computer Scientists Trying to Learn Category Theory” « Monadically Speaking: Adventures in PLT Wonderland
- Functional Programming, Logic Progamming and Category Theory | Soto van Cavalera
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…).
Wow. “Haskell” is listed five (5) times in the first sentence! ;-)
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.
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).
>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?
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
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:
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:
Which definition of “computation” is used here?
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.)
awodey’s category theory boook is in google books at
http://books.google.com/books?id=SJVsb1jCZu8C&dq=category+theory+awodey&printsec=frontcover&source=bl&ots=FEL_PqM2Qy&sig=7fW0Az7wK0Xr4i-rIVpRFdutcX8&hl=en&ei=_RheSrfpN57MswPr5fmSBw&sa=X&oi=book_result&ct=result&resnum=3
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.
Hi,
I like Schanuel’s book, which 2nd edition is now out, and here’s a link to Awodey’s one :
http://www.math.uchicago.edu/~may/VIGRE/VIGRE2009/Awodey.pdf
Yann
Hi Yann Le Du,
Thank you very much for the link to Awodey’s Category Theory! I had been unable to find a link to a full online copy until now. I’ll now add the link to the list of links to category theory books.
If you have any other titles on category theory to recommend, please let me know!
what the heck?
this might be useful http://haskell.org/haskellwiki/User:Michiexile/MATH198
According to http://haskell.org/haskellwiki/User:Michiexile/MATH198/Lecture_1 linked from your referenced URL, under section “2.4 Good references,”
> Awodey: Category Theory
>
> This book is also available as an ebook, accessible from the Stanford campus network. The
> coursework webpage has links to the ebook under Materials.
I would be interested in reading Awodey as an ebook. Would you happen to know whether this ebook is accessible to interested readers who are not Stanford University students?
Excellent post. I used to be checking constantly this weblog and I’m impressed! Very useful info particularly the last phase :) I handle such information much. I used to be seeking this particular information for a very long time. Thanks and good luck.
bodybuilding chart wrote:
> Excellent post. I used to be checking constantly this weblog and I’m
> impressed! Very useful info particularly the last phase :) I handle
> such information much. I used to be seeking this particular
> information for a very long time. Thanks and good luck.
Thank you for your comment.
Could you please advise be more specific regarding which topics that you enjoyed most? I haven’t been posting much recently because I do not really consider myself either a programmer or a mathematician, and have recently come to the realization that the more I learn, the more I realize how little I know, and the more depressed I become, since I am really more of a writer/poet-aspirant than either of the former. Besides, most readers do not comment on my posts.
Ever since graduation (and even before, actually), I have been trying to find my niche, and it seems that, as a non-programmer/non-mathematician, that niche must exist somewhere in either prose or poetry. Unfortunately, it seems that the intersection of computer “science” (I am putting the term “science” in double-quotes because the discipline is not a true science, but a procedural epistemology) and prose/poetry is the empty set.
If you happen to know of an element of this intersection, please let me know; I suspect that no such element exists.
I liked up to you will obtain performed proper here. The comic strip is attractive, your authored material stylish. nonetheless, you command get bought an nervousness over that you want be handing over the following. ill no doubt come more earlier again as exactly the similar just about very often within case you protect this increase.
Its such as you learn my thoughts! You appear to grasp a lot approximately
this, like you wrote the e-book in it or something. I feel
that you just could do with a few percent to drive the message home a little bit, however other than that, this is excellent blog.
A fantastic read. I will certainly be back.
Have you ever thought about including a little bit more than just your articles?
I mean, what you say is valuable and all. Nevertheless imagine if you added some great photos
or video clips to give your posts more, “pop”! Your
content is excellent but with pics and clips, this blog could definitely
be one of the greatest in its niche. Great blog!
> Nevertheless imagine if you added some great photos
or video clips to give your posts more, “pop”!
Thank you for your suggestion; however, I do not have a camera or videocam, and therefore, am unable to take photographs or video clips. Also, I live in a rural area of Tokyo, and rarely step out of home.
Nevertheless, I shall keep your suggestion in mind, should I have the opportunity to acquire a camera or videocam in the future.