Treeline on top of a snow covered hill

A theory of computation
e3lli's dual core calculus

An introduction to & a theory combining

the computational sequent calculus
lambda calculus with in/out duals
concurrent ML
first-class staged interaction
effects and handlers
a universal scope transcending request scheme
vau calculus
call-by-text with first class eval

Early alchemical ouroboros illustration with the words ἓν τὸ πᾶν ("The All is [[][One]]") from the work of Cleopatra the Alchemist.

computation : c
in          : i
out         : o
stage       : .
link        : o*.i* (* means zero or more)
attach      : :
name        : x
named i/o   : I/O ::= x:i. | x:.o | x:o.i
env         : E   ::= (I/O) - with unique x

Let me introduce you to the theory behind e3lli.

The core calculus in listing 1 is like the untyped lambda calculus with an opaque computation but it names inputs and outputs. It is the art of naming dual things ☯!

Computation & composition

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.

Abstraction brings a stage

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.

Attaching information brings matching

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.

Control flow

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 all1 inputs (I) to a computation result in one or more of its outputs (O):


This relates the i/o and the AND/OR duality and is called a sequent2. 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

Related research

The theory so far uses a variant of sequent calculus2 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)3. 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 handlers4. 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 calculus5:

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

Calling conventions


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 their 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's generalized eval/apply duality

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 fexprs6.

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-text 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 parent7.

Lisp frontend

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
& look at ./5--exp/



All inputs consumed is only valid for a special form of computation, that has no inputs after branch points. But general computations could always be suitably split to transform them into this special form.


Sequent calculus and its computational specification sequent core are the foundation of the presented theory. I highly encourage you to look into this alternate logical basis of computation. It is a richer theory than lambda calculus alone and has over two decades of research as a computational theory.

For a quick introduction and impressive summary of implications I recommend Introduction and Elimination, Left and Right. For a much more detailed, yet still very approachable introduction have a look at A tutorial on computational classical logic and the sequent calculus.


For an introduction you can watch this talk: Concurrent ML - The One That Got Away and have a look at a new concurrent ml for a nice scheme based introduction. CML is the fruit of John Reppys work and you can read about it directly from him here: Parallel Concurrent ML.


Effects and handlers where introduced by Cartwright & Felleisen in extensible denotational language specifications. This was picked up by Kiselyov in "having an effect" and improved by decentralizing the handlers. Its been further developed in effect systems for various languages and specialized languages build on top of effects.


The combination of links and environment acts like the effect indexed monad from having an effect. This ties into a bigger proposition: That links and environments are a nested monad while computations are arrows, having the conditional control flow that monads lack.


Only mostly forgotten thanks to the late great John Shutt who brought them back with his vau calculus.


An example of call-by-text most should be familiar is a system shell. The called programm is the child. It receives its arguments as unevaluated text and can interpret them however it likes. It can further communicate with the parent via system calls (effect requests) or by looking up names in its environment.