http://www.haskell.org/haskellwiki/Category_theory#Categorical_programming
http://www.cl.cam.ac.uk/~mpf23/
2008 January 26 – 2:46 pm
Consider the problem of how to represent negation of a proposition when we only have implication and falsehood:
Since is true and is false, this does what we want.
The contrapositive says has the same truth value as Using only implication, the contrapositive of is
What if we don’t even have [...]
2008 January 17 – 1:16 pm
The category GraphUp of graphs and Granovetter update rules has
directed finite graphs as objects
morphisms generated by Granovetter rules, i.e. the following five operations:
add a new node. (creation, refcount=0)
given a node add a new node and an edge (creation, refcount=1)
given edges and add an edge (introduction, ++refcount)
remove an edge. (deletion, [...]
A monad in Haskell is about composing almost-compatible morphisms. Typically you’ve got some morphism and then you think of a reason that you’d rather have where is a functor. In Haskell, though, you don’t define functors right out: you define type constructors, which are like the map of objects in [...]
2007 December 28 – 1:39 pm
A few days ago, I thought that I had understood pi calculus in terms of category theory, and I did, in a way.
calculus
model in Set
type
set of values
term
function
(deterministic outcome)
rewrite rule
identity functional
calculus
model in Set
process
set of states
reduction rule
state update rule
(deterministic outcome)
To make lambda calculus into a category, we mod out by the rewrite rules and consider equivalence classes [...]
2007 December 21 – 12:18 pm
We can write any expression like as a full binary tree where the nodes denote evaluation of the left child at the right, and the leaves are values:
Figure 1:
[In the caption of figure 1, the expression is slightly different; when using trees, it's more convenient to curry all the functions---that is, replace every [...]
2007 December 20 – 11:14 pm
category
lambda calculus
pi calculus
Turing machine
objects
types
structural congruence classes of processes
where is the natural numbers and is all binary sequences with finitely many ones.
a morphism
an equivalence class of terms
a specific reduction from one process state to the next
a specific transition from one state and position of the machine to the next
dinatural transformation from the constant [...]
2007 December 19 – 4:59 pm
They’re the same thing! Why doesn’t anyone ever say so?
Assume A and B are types; the continuation passing transform takes a function (here I’m using C++ notation)
B f(A a);
and produces a function
<X> CPT_f(<X> (*k)(B), A a) {
return k(f(a));
}
where X is any type. In CPT_f, instead of returning the value f(a) directly, [...]
2007 November 3 – 5:58 pm
There are several good introductions to category theory, each written for a different audience. However, I have never seen one aimed at someone trained as a programmer rather than as a computer scientist or as a mathematician. There are programming languages that have been designed with category theory in mind, such as Haskell, [...]
