The leading idea is:
types are decorations, in the same way as elements of an emergent algebra are decorations.
Motivation: Remember that emergent algebras appeared as an effort to understand the formalism of decorated binary trees which appeared first in Dilatation structures I. Fundamentals, section 4. Various efforts have been spent for this, as witnessed in Computing with space, sections 3-6, until finally arriving to the formalism of graphic lambda calculus, as exposed in arXiv:1305.5786 [cs.LO] . The main “trick” of graphic lambda calculus is that it eliminates variables, therefore it eliminates decorations of graphs!
So, the program is that now we go back from the other side, logic, where types are decorations, as you will see, in order to connect with emergent algebras, which deal with the problem of describing spaces in a purely relational way, without any appeal to points (well, in the graphic lambda calculus formalism).
Interesting thing will appear, surely.
In this version of simply typed lambda calculus we introduce types (just a bag of names , … ), with one operation, denoted by . We use types as decorations of arrows of graphs in , according to the following decoration rules:
Remark how the decoration of the gate corresponds to the trivial quandle.
I don’t claim that I can decorate any graph in by using these rules. But when I can do it, then under any move from graphic lambda calculus the decoration remains compatible with the decoration rules. Indeed, this is proved in the next figure:
The pruning and the FAN-OUT moves are trivially preserving decorations.
In another post we shall see why is this compatible with the simply typed combinatory logic.