http://www.haskell.org/haskellwiki/Category_theory#Categorical_programming
http://www.cl.cam.ac.uk/~mpf23/
2008 February 26 – 6:31 pm
With really cool bugs!
http://www.langorigami.com/index.php4
2008 February 22 – 11:55 pm
Here’s a design for a passive polarization clock.
The sky is polarized in concentric circles around the sun. The polarization of the southern sky moves through around 180 degrees during daylight hours. It is polarized vertically in the morning, horizontally at noon, and vertically again in the evening.
Align slices of polarized film such that [...]
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 [...]
