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 lambda calculus on a countable set of types. In the description below, means “ applied to ” Note the position of the term in each case:
A full binary tree of applications is either a leaf or an application of a left subtree to a right subtree. says that this leaf is the variable in question; says that the variable is in the right subtree; and says it’s in the left subtree. So, for example, in the linear lambda term
appears in the left subtree, so applying abstraction elimination once gives
Now is on the right; eliminating again in the bracketed term gives
Now is on the left; eliminating again in the bracketed term gives
And finally, we replace with
to get a term with no bound occurrences of The “I-terminated” list of combinators we added, in this case tells us exactly where in the tree the variable appeared.
In the (nonlinear) lambda calculus, the variable may appear in either branch or not at all. The and combinators are a universal basis for this calculus, and can be interpreted as
- the variable may appear in either subtree, since
- the variable does not appear in this subtree, since
- this leaf is a copy of the variable, since
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 falsehood? Well, we can pick any proposition to represent falsehood and form
The Yoneda embedding takes a category and produces a category :
This embedding is better known among computer scientists as the continuation passing style transformation.
In a symmetric monoidal closed category, like lambda calculus, we can move everything “inside:” every morphism has an internal version The internal Yoneda embedding of is
Here is the “unit” type; notice how the target type is isomorphic under the Curry-Howard isomorphism to the contrapositive. This is a term that maps a continuation and a value to
To get double negation, first do the Yoneda embedding on the identity to get
then uncurry, braid, and recurry to get
This takes a value to a function value
Call-with-current-continuation expects a term that has been converted to CPS style as above, and then hands it the remainder of the computation in
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,
- given a node add a new node and an edge (creation,
- given edges and add an edge (introduction,
- remove an edge. (deletion,
- remove a node and all its outgoing edges if it has no incoming edges. (garbage collection)
- add a new node. (creation,
It’s a monoidal category where the tensor product is disjoint union. Also, since two disjoint graphs can never become connected, they remain disjoint.
Programs in a capability-secure language get interpreted in GraphUp. A program’s state graph consists of nodes, representing the states of the system, and directed edges, representing the system’s transitions between states upon receiving input. A functor from a program state graph to GraphUp assigns an object reference graph as state to each node and an update generated by Granovetter rules to each edge.
where is either an input channel or an output channel and is taken from a countably infinite set.
- [with replacing ] if does not appear in (alpha conversion)
- (parallel processes)
- if is not free in
- [with replacing ]
- If then
- If then
- If and then
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 a functor. You have to define the map of morphisms separately.
To define the map of morphisms, we have to define (aka ) and . We define to be the category-theorist’s unit composed with the input. Applying to gives
To compose “half-functored” morphisms like we define like this: given an input and a morphism like bind produces
So a “monad” in Haskell is always the monad for categories, except the lists are of bindable half-functored morphisms like rather than lists of composable morphisms.
A side-effect monad has where is the data type for the environment on which the morphism is to act. The IO monad is a specific instance of a side-effect monad with the environment being the keyboard queue, disk drive, network, etc.