I'm a computer programmer who's caught on to denotational semantics. I mostly work with Ruby, JavaScript and C, but I know a little Haskell and ML. I've taken my first steps towards reasoning about what my software means, but my knowledge of domain theory is weak. DCPOs, chains, new notation – can you recommend a coherent introduction to this stuff?
[Math] Resources for learning domain theory
ct.category-theorymathematics-education
Related Solutions
Online resources:
- The Catsters channel
- MATH198 course notes - examples in Haskell
- Rydehard, Burstall: Computional Category Theory - examples in ML (free reprint of a book)
- MAGIC course
- Barr, Wells: Category theory for computing science (TAC TR22 is a free reprint of the book)
- Jaap van Oosten: basic category theory
- Tom Leinster
- Eugenia Cheng
- Steve Awodey - very similar to the book mentioned by Quadrescence
- Daniele Turi
- Thomas Streicher
- Abstract and concrete categories: the joy of cats - might be considered too verbose, but it's full of examples; slightly newer (?) version as TAC TR17
- Spivak: Category Theory for Scientists - free textbook of a 2013 MIT OpenCourseWare; an updated (and non-free) version was published by MIT Press in 2014.
- Emily Riehl: Category Theory in Context
Books (not free):
- Benjamin Pierce: Basic category theory for computer scientists, MIT Press 1991; a slight expansion/update of the earlier (and free) CMU-CS-88-203 report
- MacLane - solid mathematical foundations, but hardly any references to computing
- Martin Brandenburg - Einführung in die Kategorientheorie (in german)
Category theory in Haskell:
- Wikibooks introductory text
- sigfpe's blog has a lot of category theory articles - (di)natural transformations, monads, Yoneda lemma...
- Comonad.Reader
- The Monad.Reader - check "Calculating monads with category theory"
- Bartosz Milewski - Category Theory for Programmers
The most immediately obvious relation to category theory is that we have a category consisting of types as objects and functions as arrows. We have identity functions and can compose functions with the usual axioms holding (with various caveats). That's just the starting point.
One place where it starts getting deeper is when you consider polymorphic functions. A polymorphic function is essentially a family of functions, parameterised by types. Or categorically, a family of arrows, parameterised by objects. This is similar to what a natural transformation is. By introducing some reasonable restrictions we find that a large class of polymorphic functions are in fact natural transformations and lots of category theory now applies. The standard examples to give here are the free theorems.
Category theory also meshes nicely with the notion of an 'interface' in programming. Category theory encourages us not to look at what an object is made of, but how it interacts with other objects, and itself. By separating an interface from an implementation a programmer doesn't need to know anything about the implementation. Similarly category theory encourages us to think about objects up to isomorphism - it doesn't precisely proclaim which sets our groups comprise, it just matters what the operations on our groups are. Category theory precisely captures this notion of interface.
There is also a beautiful relationship between pure typed lambda calculus and cartesian closed categories (CCC). Any expression in the lambda calculus can be interpreted as the composition of the standard functions that come with a CCC: like the projection onto the factors of a product, or the evaluation of a function. So lambda expressions can be interpreted as applying to any CCC. In other words, lambda calculus is an internal language for CCCs. This is explicated in Lambek and Scott. This means for instance that the theory of CCCs is deeply embedded in Haskell, because Haskell is essentially pure typed lambda calculus with a bunch of extensions.
Another example is the way structural recursion over recursive datatypes can be nicely described in terms of initial objects in categories of F-algebras. You can find some details here.
And one last example: dualising (in the categorical sense) definitions turns out to be very useful in the programming languages world. For example, in the previous paragraph I mentioned structural recursion. Dualising this gives the notions of F-coalgebras and guarded recursion and leads to a nice way to work with 'infinite' data types such as streams. Working with streams is tricky because how do you guard against inadvertently trying to walk the entire length of a stream causing an infinite loop? The appropriate dual of structural recursion leads to a powerful way to deal with streams that is guaranteed to be well behaved. Bart Jacobs, for example, has many nice papers in this area.
Best Answer
The book recommended by jef is the domain-theory bible. It may be a bit overwhelming for a beginner. For an easier and more compressed introduction I recommend that you have a look at Abramsky and Jung's chapter on domain theory from the Handbook of Logic in Computer Science. It is available in PDF from Achim's publications lits.