A theory of computation
e3lli's dual core calculus

It begings with computation (c) alone. Computation without context is eternal and closed: ◯ an ouroboros. Think of an infinite loop, the universal thing to do if there is nothing else to do. This might be the purest form of computation but it has no effect outside simply being there and gazing its naval.

For computation to be interesting and usefull there needs to be a context for it to interact with. Since there are two things now there is scope: The computation in context has an inside (in scope) and an outside (out of scope). Interaction with the context creates an interface between the scopes.

Since a closed computation does not interact, it needs to be opened. Splitting the closed computation yields a computation with a beginning and an end - an input (i) and an output (o). This interface allows the computation to consume things from and produce things for the context. This form of computation with an interface is called a continuation and makes the composition of computation possible. If you chain two compatible continuations you get a bigger continuation. Composition results from this fundamental duality of programming - the duality between input & output, beginning and end. An input is just an output from the other side.

Because i&o are duals they are fundamentally linked together, you cannot have one without the other. But this means composition does not work and scope is an illusion. While the later is true and perfectly fine, the former is possible with a little abstraction. We stage (.) i&o creating a link. It represents an potential interaction that has yet to happen.

Listing 2 shows the possible links and their creation. You create a link by staging nothing, i or o. If you combine two compatible open links you have a closed link.

    stage nil -> .    -  empty link
    stage i   -> .i   -   open link (staged input)
    stage o   -> o.   -   open link (staged output)
combine o. .i -> o.i  - closed link

To make a closed link happen you have to run it, realizing its potential interaction. There is now an additional run step and that means computation now happens in two stages:

• First stage computations interact with links - abstract interaction. They are independent of their context and instead present an interface of links at their boundary.
• The second stage runs closed links and makes the connection happen. At this stage the actual computation takes place.

The first stage can be understood as a frozen computation waiting for i/o while the second actually does the i/o. Both stages are distinct but not separate. They can be mixed fluently by making links first-class values. Thus the addition of staged interaction in the form of links makes the composition of computation possible.

Doing composition this way also properly propagates through the computation. Thus a computation that receives a staged input is now staged itself and while it waits for this input it propagates the link through later outputs, staging them too.

With the help of links the context can be abstracted as interfaces build from sets of open i&o links. Composing these interfaces is combining the links they contain. The resulting closed links can only run if they pass the same type of thing. This needs to be assured before running them.

To narrow the choice of compatible links and introduce a flexible notion of match we can attach additional information to links (:). We can now annotate a link with the type of thing it intents to pass. If the type is known during the first stage it can propagate and narrow the choice of matching links. This lifts the typecheck from run to combine. More information during composition reduces the potential for error later on.

Another usefull information about a link is its name. Names help during composition. With their help a interface can demand a dual link with a particular name. Thereafter it will only match a dual interface if the names match too.

Links with attached information (named or typed links) can be combined forming interfaces. They provide a match mechanism that looks up matching links for composition. These kind of interfaces with attached information are then called environments (E). They abstract the requirements and known information about the contex. An important feature of environments in programming is providing named things. This is archived by providing the name as additional information in the environment.

So far only two types of information where introduced but more are possible if needed.

Our ouroboros derived computation is strictly linear so far. The continuations are chained by an AND relation. Do this and then that and so on. Let's make the control flow more interesting and add OR - the dual of AND. Now all¹ inputs (I) to a computation result in one or more of its outputs (O):

I.c.O

This relates the i/o and the AND/OR duality and is called a sequent². Computation composed of sequents has a tree shaped conditional control flow. The computation in listing 3 is the model most expect while programming and the form we use from now on. It is an abstracted and composable computation with a well defined interface in the form of an attached dual environment.

(args:.i out:o. err:o.)
(name:(args:.i out:o. err:o.))

Listing 4 shows the signature environment of a typical function. It is waiting on its arguments and either produces something via its normal output or in case something goes wrong via an error output. This signature could itself be named and nested in another environment. This then is a named function.

Links are one to one so far. Let's change that too for an even richer theory. An obvious extension is to make them one to many. This does not need any decision logic. Several i/o can now wait on their dual. This is a copy operation. It could be used for example to implement a hook, that contains several functions waiting for a trigger.

Links already do a form of matching and depending on that either combine and run or not. Extending this allows to make links many to many. There is still no conditional logic inside links - this is exclusiv to computations. Links either combine or not. But this new form of links does not only copy (to many) but also enforces equality (many to). In this light copy is dual to equal.

This final form of links forms a narrow waist for things to go through. In addition they introduce a flexible match to the composition of computations and allow to gradually specify or collect information about ones context.

combine .i & .i -> .ii
combine o. & o. -> oo.
combine oo. & .ii -> oo.ii

The theory so far uses a variant of sequent calculus² to lay a rich foundation for a programming language. Other important ideas in computer science can be directly expressed on this foundation.

The first idea is a unfortunately half forgotten but nonetheless important paradigm for concurrent programming: Concurrent ML (CML)³. It solves the problem of how to organize and do things in parallel. It does so by introducing first-class synchronous events and their combinators. These events are the links we defined earlier.

The second idea seems to be on its way into the well deserved spotlight: Computational effects and handlers⁴. They allow for flexible and extensible semantics by defining them in terms of effects to the context. The context supplies their meaning using handlers. Handlers in first approximation are like a named function in an environment. But in contrast to functions they can act on two levels: One is the level the effect is invoked and the other the level where the handler is defined. This gives handlers and effects the ability to act between scopes.

This framework allows to define powerfull new effects (eg. error handling, fibers) without having to alter existing effects (= stable denotations). It does so by a general effect composition that works with a two stage evaluation model. Or in other words composition can skip unknown effects and delay running the computation until all effects are handled. Since we already defined a mechanism for two staged fluent computation we can implement effect on top of our core calculus⁵:

effect-request:(args:o. effect-level-out:.i)
handler:(args:.i effect-level-out:o. handler-level-out:o.)
- handler-level-out is provided where the handler is instantiated

o.i

The link in listing 6 is called a critical pair. When it is run a decision has to be made: Who gets to run first? Does run first wake the o & pass it the i? Or the other way around? One part of the pair will receive control first and can call the other at its discretion if it needs the thing passed.

If you think of the two links as two scopes then the decision is if the parent or the child scope controls the interaction. Putting the parent scope in control is call-by-value, because the parent evals the thing thats passed before the child receives anything. On the other hand putting the child in control is call-by-name since now the child can decide when to eval the things it received.

Lisp evaluation works by mutual recursion of eval and apply. Eval looks at an expression and if it is a function application it calls apply. Apply in turn calls eval on the arguments and invokes its function on them. This is call-by-value. If the function returns eval receives the return value and continues. This mutual recursion sits at the core of Lisp and its link to duality was made popular by the wizard book.

Lisp is among other things famous for its two stage evaluation model that brings two function colors with it: Macros and functions. Another today mostly forgotten evaluation scheme brings fluidity to the two stages and removes the two color distinction. It is called call-by-text and its functions are called fexprs⁶.

Call-by-text generalizes the eval/apply duality while combining it with another of lisp's strengths: code is data (the program code is just another nested list). Call-by-text evaluation passes arguments unevaluated as data to the child. The child now has total freedom to do what it wants with its arguments. One thing it can do is ask the parent to evaluate the arguments for it. This way call-by-value, call-by-name and even call-by-need can be implemented by the child. Or the child could decide this is not lisp anymore, evaluate its arguments as a regexp for example and just like this you have a built-in regular expression language. This gives even more power to the child scope while mainting a well defined communication channel to the parent⁷.

The core language developed so far should make a great compiler intermediate language (like CPS, ANF et al). Let's build a more structured language on top - an effect-based, call-by-text lisp frontend:

name          -> name:.i                  - a receive effect request
(name . args) -> name:(args:o. ()-out:.i) - a send & receive effect request

Listing 7 shows lisp's two main structured expressions (ignoring self evaluating atoms) and how they are translated into core effect requests. A symbol alone becomes a named, waiting input. A list becomes an i/o dual. It wants to provide its cdr as args, transfering control to the effect until the whole thing becomes the effect output.

This is a future I want to see in lisp. My goal and hope is to further the extensible language of languages quality of lisp and this should provide an adequate core.

Want more?

You can have a look at the notes that lead to this:
% git clone http://perma-curious.eu/eee.git
& look at ./5--exp/sequent-story.org