Currying by using zippers and an allusion to the Cartesian Theater

Here is a recipe for understanding currying with the help of zippers.  (Done in graphic lambda calculus.)

We have a graph A \in GRAPH which has one output and several inputs. We want to curry it. For this we have to artificially give names to the inputs, i.e. to number them (notice that such a thing is not needed in graphic lambda).


The next step is to use a n-zipper in order to clip the inputs, by using n graphic beta moves, until we get this:


This graph is, in fact, the following one (we replace the n-zipper, which is just a notation, or a macro, with its expression).


The graph inside the green dotted rectangle is the currying of A, let’s call him Curry(A).  This graph has only one output and no inputs.  (The procedure of currying can be made itself into a graph which is applied to  the output of A, but we stop at this level for this post.) The graph inside the red dotted rectangle is almost a list. We shall transform it into a list by using again a zipper and one graphic beta move.


Now we’re done!

As you see, the currying creates the list, or the list creates the currying, or both form a pair, like the homunculus Curry(A) and the scenic space List(1,2, ... , n), an allusion to my post on the Cartesian Theater.


10 thoughts on “Currying by using zippers and an allusion to the Cartesian Theater”

    1. They are the two sides of a whole. The post is a mathematical proof of this. Think about A as being a function with several variables. Currying means to express this function as a function of a variable with values in ( functions of a variable with values in (functions of a variable with values in …))) until the list of variables ends. What is interesting here is that in graphic lambda there are no names for variables. The graph A from the first figure is equivalent with the graph from the last figure (i.e. A can be transformed by using graphic beta moves into the last graph). The graph from the last figure means that the curryed version of the “function” (though not a function without using extensionality) A is applied (at the right, funny but meaningful) to the list of variables. That’s equivalent with A with an arbitrary numbering of its inputs. This is obvious once you admit names for variables. But is less trivial to show that the pair (curry, cons) appears as a consequence of the procedure of naming variables. If you want, A is like a geometrical object (say, a sphere) and the graph at the end is like a parametrization of the geometrical object. The parametrization is not geometrical. Or A is like a physical property of a system expressed intrinsically and the graph at the end is like the same physical property expressed in a reference frame. But physical properties are those which are independent wrt the choice of reference frame. That’s exactly my critic in the post on the cartesian theater, namely that by using the theater in a box as a model of the cartesian theater, one is misled to think that homunculus existence leads to fallacies, but otherwise everything is OK with the scenic space. No, the scenic space is the other side of the homunculus. This is not meaning to deny the existence of the objective space exterior to the observer.

    1. Thanks! So, once the currying and lists are in place, then the choice concerning the order of taking beta moves (i.e. reductions) narrows, to the point that one may practically reduce it to two main strategies (for example lazy). This gives the illusion that there is no other choice to be made by an exterior manipulator of the expressions. This is also what makes computers feasible, because we are not asked before any reduction step to choose among multiple reduction possibilities, if any.

      Coming back to the “geometric property” analogy, then, per my weak understanding of those matters, indeed you are right that the evaluation strategy has to do with bisimulation, as you communicated in private. For me this is like the old way of differentiable geometry, which is to say that a quantity (like a tensor given as an array of numbers) computed wrt a chart is geometrical if there is a given rule of transformation (between tensorial quantities given in coordinates) which transforms the initial quantity into the one which is computed by the same recipe in a different chart.

      Finally, we may speculate that natural computing systems, as maybe is our visual system, don’t need to curry, because the order of taking reduction step is given by a physical process (like diffusion, or some probabilistic rule concerning the local state of the graph). In this way, the number of “computational steps” (i.e. reductions) is much lower than in curried form, observation which might be relevant for the puzzle that in the visual system all “computation” is done by at most 6 synaptic jumps. Such natural systems would be then massively parallel, instead of being massively sequential, due to currying. But in order to understand how they work, in order to simulate them on a computer, we would have to curry the process. Maybe brain work is like a massively parallel version of Brainfuck, who knows?

      EDIT: One more thing. There is a way to check this hypothesis, in principle. It goes like this: take an algorithm, express it in untyped lambda calculus, better in Unlambda, then express it in graphic lambda calculus, then uncurry it and spread it as much as possible (i.e. such that it is transformed into a graph in graphic lambda calculus with the properties that: (1) there is as small as possible distance between inputs and outputs of the graph (measured as the number of nodes one has to pass from an input to an output, for example), (2) the reduction steps (or other moves) are as evenly spread as possible over the graph, allowing for as much as possible parallelism). If this procedure works then the result is the “geometrical” picture of the algorithm, and maybe the most resembling one with what happens in a brain. You imagine that just by looking at such a graph one would be hardly capable to say what is the algorithm.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s