http://www.haskell.org/haskellwiki/Category_theory#Categorical_programming
http://www.cl.cam.ac.uk/~mpf23/
Consider some javascripty pseudocode:
aPoint = {x:3, y:4};
This is an object that responds to four messages: “x”, “x =”, “y”, “y =”
>> aPoint.x
[ {x:3, y:4}, 3 ]
>> aPoint.y
[ {x:3, y:4}, 4 ]
>> aPoint.x = 15
[ {x:15, y:4}, null ]
>> [...]
2008 January 30 – 3:29 pm
In linear lambda calculus, you must use each bound variable exactly once in a term. A term with a single bound variable is a full binary tree of applications in which one of the leaves is the bound variable, so it makes sense to ask, “which leaf?”
Three combinators are universal for the free linear [...]
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, [...]
where is either an input channel or an output channel and is taken from a countably infinite set.
Structural congruence:
[with replacing ] if does not appear in (alpha conversion)
(parallel processes)
(association)
(restriction)
(replication)
if is not free in
Reduction rules:
[with replacing ]
If [...]
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 [...]
