Continuing from Simply typed graphic lambda calculus , let’s look at decorations for the S,K,I combinators.
We want to decorate the arrows of such graphs, according to the rules given in the following figure:
Decorations are denoted by letters … or by letters …. (what’s in a name?). These decorations are called “types”. There is only one operation, called ““, which takes a pair of types and returns the type .
In algebraic terms, here’s what is happening. We start with a graph in and we decorate all it’s arrows with different letters from an alphabet (of types). Then we associate to it the magma with:
- generators being the (decorations of the) arrows
- relations being the ones from the rules of decorations given in the previous figure.
If the magma is free, then we say that the graph is well typed. That means we can find a finite collection of types, with no relation between them, such that all arrows can be decorated by some element of the free magma generated by that collection of types.
Remark 1: Please, don’t let me reinvent the wheel. Surely somewhere in the big work on type theory, there is something analogous done already. Just send me citations and I shall add them with due acknowledgements.
Remark 2: This is exactly the same idea which is used in knot theory, where we associate to a knot diagram it’s knot quandle. But with a twist: while in knot theory we look for quandles which are not free (we cannot eliminate all relations between the generators), in this simply typed lambda calculus we concentrate only on those graphs which have free magmas associated. Please look at the right, lower corner from the previous figure, where is given the rule of decoration for the gate. (We are not going to use it in relation to the lambda calculus sector.) As you see, this is compatible with the trivial quandle with the operation .
Remark 3: I am not going to enter or take the extremely interesting path of cartesian closed categories , basically because my strong bias against anything cartesian. The initial source of this bias comes from the experience with sub-riemannian geometry, where any application of cartesian ideas, like slicing a problem until it becomes 1 dimensional, then solving it by 1d calculus and analysis techniques, then reassembling the slices, leads always to “rigidity results”, which have the form: if you try then you arrive at a contradiction. Don’t get me wrong, there are amazing and extremely deep such results, but they are always in the form of a proof by contradiction.
Remark 4: The point of view from this simply typed graphic lambda calculus is surely related to the Hindley-Milner type system.
Let’s see how this works for the I, K, S combinators, then for the combinator.
The procedure is the following:
- we number the nodes of the graph (arbitrarily)
- we put arbitrary, different labels on each arrow of the graph
- we write the relations which appear from each node, according to the rules of decoration
- finally, we examine the generated magma, to see if, eliminating some generators by using the relations, we can arrive to prove that’s a free magma.
In the next figure this is done for the combinator (the identity) and for the combinator.
We obtain the right types for identity and combinators (there are no contexts, that’s for later). It was easy, they are “well typed” according to the definition from here.
Now, let’s look at the combinator:
We have to work a bit, but not too much:
(For the convenience of the readers, I added in the figures the usual notations for combinators and types. )
We obtain again the right types for as well as for the variables involved.
Let’s try to decorate the combinator .
We obtain the following magma presentation:
which cannot be free, because of relations (4) and (6). So is not well typed, exactly like in the simply typed lambda calculus.