Coeffects are Tomas Petricek's PhD research project. They are a programming language abstraction for understanding how programs access the context or environment in which they execute.
The context may be resources on your mobile phone (battery, GPS location or a network printer), IoT devices in a physical neighborhood or historical stock prices. By understanding the neighborhood or history, a context-aware programming language can catch bugs earlier and run more efficiently.
This page is an interactive tutorial that shows a prototype implementation of coeffects in a browser. You can play with two simple context-aware languages, see how the type checking works and how context-aware programs run.
This page is also an experiment in presenting programming language research. It is a live environment where you can play with the theory using the power of new media, rather than staring at a dead pieces of wood (although we have those too).
We hide some details by default to keep the tutorial shorter, but you can get them back if you want!
Short is good! You can always come back.
I'm practical! Show me more examples.
Love theory! Give me all the equations.
Show me all! Time is not an issue.
Programming languages evolve to reflect the changes in the computing ecosystem. The next big challenge for programming language designers is building languages that understand the context in which programs run.
This challenge is not easy to see. We are so used to working with context using the current cumbersome methods that we do not even see that there is an issue. We also do not realize that many programming features related to context can be captured by a simple unified abstraction. This is what coeffects do!
Say you need a function that caches values in an in-memory dictionary, or using
a local file system when it is available. Using #if, you can write:
let readFromCache key f =
// Read value from memory or disk
if cache.Contains(key) then
cache.Get(key)
#if LOCAL_FILE_SYSTEM
elif File.Exists(key) then
File.ReadAllText(key)
#endif
// Calculate and cache the value
else
let result = f()
cache.Set(key, result)
#if LOCAL_FILE_SYSTEM
File.WriteAllText(key, result)
#endif
result
You could refactor the code to make it less ugly, but the issue will not go away.
As you need to target more and more platforms, the combinations of #if flags grow
exponentially and it is hard to know that all configurations even compile.
Ideally, the programming language would understand which functions need what capabilities and it would automatically check on which platforms can your code run.
In stencil computations, we calculate value for each element of a grid or mesh based on its neighborhood. This is useful in simulations in fluid dynamics or weather modelling.
A simple example is Conway's Game of Life or other cellular automata. The following example
implements the rule 110 (arr.[x] accesses xth
element of the array and cursor is the current position):
let sum = input.[cursor-1] +
input.[cursor] + input.[cursor+1]
if sum = 2 || (sum = 1 &&
input.[cursor-1] = 0)
then output.[cursor] <- 1
else output.[cursor] <- 0
This automata looks at one item on the left and one item on the right. Knowing this is important for correctly handling border conditions. If the compiler knew the access pattern, it could check this and it could also pre-allocate the necessary space and produce more efficient code, especially when compiling for a GPU.
In effect systems, the effects of function body are always delayed. A printing inside function body will happen when the function is executed. Coeffects are different.
Say we have a function that requires a clock. We construct it on the server and then send it to the client. The clock can come from the declaration side (server) or from the call side (client). Scroll to coeffect type systems for the details.
Coeffects can be associated with the whole context, but they can also talk about individual variables. For example, we can track whether a variable is used (live) or not (dead):
\[x : {\color{typ} \text{int}}, y : {\color{typ} \text{int}} {\scriptsize \;@\;} {\color{coeff} \langle \sf L, \sf D \rangle } \vdash x : {\color{typ} \text{int}}\]
Here, the coeffect is a vector of annotations and we see the \(x\) is live but \(y\) is dead. The compiler can then eliminate dead variables!
Effectful computations can be modelled using monads. A function \(\tau_1 \rightarrow \tau_2\) with side effects becomes \(\tau_1 \rightarrow {\color{eff} M}\tau_2\) where the monad \({\color{eff} M}\) tracks the additional effects as part of the result.
Context-aware computations can be similarly modelled using comonads. A function that requires additional context becomes \({\color{coeff} C} \tau_1 \rightarrow \tau_2\) where the comonad \({\color{coeff} C}\) captures the additional context.
Here, you can play with two simple coeffect languages. A language with
implicit
parameters shows how coeffects track additional contextual information such as
available resources (GPS, network printer) or available device features (file system, network).
In our small demo, resources are written as ?size.
The second demo is a simple
dataflow language where all variables represent streams of values
and you can access previous value using the prev keyword. For example (x + prev x) / 2
calculates the average over the current and previous value. Here, coeffects track how many
past values you need.
Choose a sample from the tutorial or write your own snippet using
?param to access an implicit parameter value!
The program is well-typed. The type system reports the following type and coeffect information:
The context of the expression requires no implicit parameters. You can see the result below.
The expression requires some implicit parameter values. You can set their values here:
42, variables foo and implicit parameters ?foo+, -, *, / and ^let x = e1 in e2 where in is requirede1 e2 and functions fun x -> elet foo x = x + 1 in ...fun x y -> x + yThe syntax is ML and F#-inspired. Unlike in F#, it is not
indentation-sensitive and so you need the in keyword in each
let binding.
|
When you load the snippet in the editor, you will need to enter values for ?fst and ?snd
before you can run the code. This is because the two values are the required coeffects of
the expression. We use numbers, but the same mechanism would work for resources like GPS
sensors or printers.
Dynamic scoping is useful when you want to add a parameter to a function in a deeply nested chain of calls. With implicit parameters, you do not have to explicitly pass it around in each function. For example:
|
The function dyn uses a parameter ?fst. We set the parameter value when we call the
function. The coeffect system tracks the required implicit parameters and it won't allow calling the
function if we do not provide a value. You can see (in a tooltip for dyn) that the type of
the function is num -{ ?fst:num }-> num.
However, coeffects also support lexical scoping and capture parameters that are already in scope:
|
The implicit parameter ?fst is in scope when lex is defined and so the function
does not require any implicit parameters. Its type is num -> num.
This is where coeffects differ from effects and monads! If we were using the Reader monad,
we would get a function that requires ?fst. In other words, monads support only
dynamic scoping, but not lexical scoping.
|
The type of both is num -{ ?snd:num }-> num, which suggests that parameters available in
the lexical scope are always captured (this is the case of ?fst here). In other words,
the lambda abstraction rule in our type system splits the coeffects of the body so that only
requirements that cannot be satisfied from the current lexical scope (when defining the
function) are delayed and are required when calling the function.
For more information about how this works, scroll down to the type system section, which shows the typing derivations for these examples.
|
This function calculates the average between the current and the previous value. The
type of the function is num -{ 1 }-> num denoting that it needs one last value. Try
removing prev altogether or looking further into the history using prev (prev n) to see
how the number of required past values changes!
When checking the body x + prev y, the flat system infers that the required number of past
values is 1. There is just one number for the whole expression, so the system does not capture
the fact that we're only accessing past value of the variable y. Try changing the body to
x + y or to prev (x + y) and see how the inferred type changes. Click "edit" and then
"check" to type-check the code snippet.
The structural system keeps one annotation for each variable. When checking the body x + prev y,
it infers that we access the current value of x and one past value of y. This is
reflected in the type of the function. Try changing the body in the same way as previously
and see how the type of the function changes!
The flat system for tracking number of past values in dataflow languages is actually an instance of the same coeffect calculus as the one for tracking implicit parameters. The structural system is more sophisticated, because it needs to keep track of individual variables. Aside from dataflow, it can also capture variable liveness.
Experiment with dataflow programming here! You can use the same core language
as earlier; prev e accesses the previous value of e and you can
nest them and write prev (prev e).
The program is well-typed. The type system reports the following type and coeffect information:
The expression was not a function and you can see the result below.
For more fun, write a function like fun x -> prev x!
The function requires some input streams. You can set their current and historical values here:
|
To avoid nesting the prev construct 12 times, we define a function prev4 that
returns the 4th past value. When we then call prev4 (prev4 x) we are then accessing
the 8th past value. The chart updates 20 times per second, so you should see about
500ms delay.
|
Just like above, we use helper functions to make the code shorter. The sum4 function
adds the current value and 3 previous and prev4 returns 4th past value of an argument.
We then sum 12 values in chunks by adding sum4 x, sum4 (prev4 x) and sum4 (prev4 (prev4 x)).
|
We use x - prev x to calculate the difference between the current and previous value,
then we square it and add the speeds of X and Y moves. You should see higher spikes when
you move your mose faster and smaller spikes when you move it slowly.
Write simple dataflow computations that produce a value based on the current and previous X and Y coordinates.
The expression is well-typed, but it is not a function
taking X and Y arguments, so we cannot use it for this demo. Try writing for example
fun x y -> x + y.
All set! Start by moving mouse pointer or your finger in a circle in the box below and see what happens!
In the interactive playground above, you can write fun programs using a dataflow language
with the prev keyword. But what do you get from using coeffect system to track how
many past values are needed? Most importantly,
coeffects give you a unified way of thinking about context-requirements.
Readability. You get code that is easier to understand. When you look at a function, you know whether it uses just the current value or if it needs to look at the history. For implicit parameters, the requirements are also immediately visible.
Efficiency. By knowing how many past values we'll need, we can pre-allocate a fixed-size buffer to keep the past X and Y coordinates. This means that code can run faster and we can also better avoid potential memory leaks.
Safety. In case of implicit parameters, coeffects inferred which parameters are needed and you had to set their values before running the code. This means that we cannot get a runtime error when a required parameter is not set!
Modern programs need to run correctly in a larger number of increasingly diverse environments. Does your program need Android API level 23? GPS sensor and access to internet? Access to the friends of your friends on Facebook? Or historical stock prices for 2 years? A language with coeffect support can check the requirements statically and give you guarantees that things will run as expected. Most importantly, coeffects give you a unified way of thinking about context-requirements.
If you got as far as here, I guess you want to know everything there is about coeffects! The rest of the page shows more details about the theory about coeffects. Some parts may require more detailed programming language theory background, but there are still fun interactive demos to help you understand it!
The theory of coeffects consists of two type systems for checking coeffects and a semantics that defines the meaning of context-aware programs in terms of translation. We translate context-aware source language into a simple target language with a few comonadically-inspired primitives.
Type systems. The type system checks how many past values does a function use or which implicit parameters it accesses. Coeffects define two unified systems that can be specialized for individual contextual information.
Comonads. The meaning of effectful computations can be captured using monads. A concrete monad describes a concrete kind of effect. Similarly, context-aware computations can be captured using comonads. One concrete comonad describes dataflow and one implicit parameters.
Translation. We translate the source program to a target language and insert calls to a few special comonadically-inspired functions. Just like bind and return in Haskell's do notation, those functions define how the concrete contextual information is passed around and used.
When you have an expression that prints to a console and you wrap it inside a function, the printing will happen when the function is called. This is how effects behave. This is nicely captured by Wadler and Thiemann in the Marriage of effects and monads:
In the rule for abstraction, the effect is empty because evaluation immediately returns the function, with no side effects. The effect on the function arrow is the same as the effect for the function body, because applying the function will have the same side effects as evaluating the body.
Coeffects are different. When you require an implicit parameter from the environment, it can come from anywhere. You may get it (immediately) when the function is created or when it is called (later). In general, coeffects place requirements both on the declaration-site and on the call-site.
There is much more that can be said about the coeffect type system. You can find a detailed and precise description in the papers on coeffects. To get a quick idea of how things work, continue reading and expand the section below with more details. You can also scroll down and play with the interactive type checker!
The second interesting aspect of coeffect systems is that the information is attached to the variable context rather than to the resulting type of an expression. In flat coeffect systems, the coeffect is just a single annotation:
\[x_1\!:\!{\color{ltyp}\tau_1}, \ldots, x_n\!:\!{\color{ltyp}\tau_n} {\scriptsize \;@\;} {\color{lcoeff} r} \vdash e : {\color{ltyp} \tau}\]
For implicit parameters, the annotation is a set of implicit parameters. Flat coeffects can be used for dataflow too. In that case, the annotation is the maximal number of past values of any of the variables in the body.
For example the expression \(x + {\color{lkvd}\text{prev}}~y\) gets an annotation \({\color{lcoeff} 1}\). This is correct, but not precise. We need one past value of \(y\), but only the current value of \(x\).
Structural coeffects solve the limited precision of the flat system when tracking contextual information that are attached to individual variables.
Rather than adding a single annotation, structural coeffects add a vector of annotations with one annotation for each variable. We do not add annotations to individual variables separately to keep the same shape as in the flat system:
\[x_1\!:\!{\color{ltyp}\tau_1}, \ldots, x_n\!:\!{\color{ltyp}\tau_n} {\scriptsize \;@\;} {\color{lcoeff} \langle r_1,\ldots,r_n \rangle} \vdash e : {\color{ltyp} \tau}\]
In case of dataflow, each annotation in the vector captures the number of required past values of the corresponding single variable. Given an expression \(x + {\color{lkvd}\text{prev}}~y\), the vector attached to \(x, y\) is \({\color{lcoeff} \langle 0, 1 \rangle}\), requiring the current value of \(x\) and one past value of \(y\).
The structural system needs to ensure that the vector of annotations stays in sync with the variables, so they treat variable context as a vector too. Variables can still be freely rearranged and duplicated, but each of those structural rules performs a corresponding transformation on the vector of coeffect annotations.
By keeping a vector of annotations, we also know the exact coeffect that should be associated with a function, so we no longer need the \(\wedge\) operation in the lambda abstraction rule. Instead, function becomes annotated with the annotation that belongs to the bound variable:
\[\dfrac {\Gamma, x:{\color{typ} \tau_1} {\scriptsize \;@\;} {\color{coeff} r \times \langle s \rangle} \vdash e : {\color{typ} \tau_2 } } {\Gamma {\scriptsize \;@\;} {\color{coeff} r} \vdash {\color{kvd} \text{fun}}~x \rightarrow e : {\color{typ} \tau_1} \xrightarrow{~\color{coeff} s~} {\color{typ} \tau_2}}\]
Here \({\color{coeff} r \times \langle s \rangle}\) splits the vector into two parts. \({\color{coeff} r}\) is a vector of annotations that correspond to the variables in \(\Gamma\) and \({\color{coeff} \langle s \rangle}\) is a vector with just a single annotation that corresponds to \(x\) and becomes the annotation of the function type.
The meaning of coeffectful computations can be captured by a structure called comonad. In programming terms, comonad is a data structure (like a monad) with two operations called counit and cobind. Coeffects use an indexed version of comonads, which means that the data type also has an annotation and so we write it as \(C^{\color{coeff}r} {\color{typ} \tau}\) rather than just \(C {\color{typ} \tau}\). We'll get back to the annotations later, let's first look at the operations.
\[\begin{array}{rcl} \text{counit} &:& C^{\color{coeff}\sf\text{use}} {\color{typ} \tau} \rightarrow {\color{typ} \tau} \\ \text{cobind} &:& (C^{\color{coeff}r} {\color{typ} \tau_1} \rightarrow {\color{typ} \tau_2}) \rightarrow C^{\color{coeff}{r \circledast s}} {\color{typ} \tau_1} \rightarrow C^{\color{coeff}{s}}{\color{typ} \tau_2} \end{array}\]
The operations are dual to the unit and bind operations of the monad and have the following types. The annotations are from a coeffect algebra mentioned earlier, but feel free to ignore them for now.
A sample comonad is one for stencil or grid computations. It lets you write computations that calculate over a grid and can look at values in the neighborhood. For example, we can average the current value with those on the left, right, top and bottom:
| 0.0 | 1.0 | 1.0 |
| 0.0 | 2.0 | 2.0 |
| 2.0 | 3.0 | 4.0 |
| ? | ? | ? |
| ? | ? | ? |
| ? | ? | ? |
How is this captured by a comonad?
We use merge in lambda abstraction (to combine context from the declaration-site and from the call-site) and we need split whenever we need to evaluate multiple sub-expressions (for example, to split context between \(e_1\) and \(e_2\) in \(e_1 + e_2\)).
\[\begin{array}{rcl} \text{merge} &:& C^{\color{coeff}r} {\color{typ} \tau_1} \times C^{\color{coeff}s} {\color{typ} \tau_2} \rightarrow C^{\color{coeff}{r \wedge s}} ({\color{typ}\tau_1} \times {\color{typ}\tau_2}) \\ \text{split} &:& C^{\color{coeff}{r \oplus s}} ({\color{typ} \tau_1} \times {\color{typ}\tau_2}) \rightarrow C^{\color{coeff}r} {\color{typ} \tau_1} \times C^{\color{coeff}s} {\color{typ} \tau_2} \\ \text{duplicate} &:& C^{\color{coeff}{r}} {\color{typ} \tau_1} \rightarrow C^{\color{coeff}{r}} ({\color{typ} \tau_1} \times {\color{typ} \tau_1})\\ \end{array}\]
Merge takes two values with some additional context and combines them into a tuple while also merging the additional context. Split takes a single tuple with additional context and splits it into two components, while also splitting the additional context. Finally, duplicate is just a helper (not strictly needed) that duplicates a value inside a comonad.
The nice thing about coeffect systems is that a single type system and a single translation mechanism works for multiple different systems. For a concrete system like dataflow computations or implicit parameters, we just need to define a concrete data type \(C^{\color{coeff}{r}} {\color{typ} \tau}\) with its associated coeffect algebra (to be able to type check the program) and operations (to be able to run it).
Data type for implicit parameters is a tuple of the value 'a together
with a lookup function that returns the value of an implicit parameter
with the given name:
type IP<'a> = IP of 'a * (string -> obj)
The counit function returns the value (and ignores the implicit parameters).
In cobind, we duplicate the implicit parameters into p1 and p2, we call
the function f with the first set and we return a comonad with the resulting
value and the second set of implicit parameters:
let counit (IP(v, _)) = v
let cobind f (IP(v, p)) =
let p1, p2 = p, p
IP(f (IP(v, p1)), p2)
The merge operation combines the two lookup functions it gets and split
creates two copies. We also need a special lookup function to get the value
of an implicit parameter:
let lookup name (IP(_, f)) = f name
The coeffect annotations tell us what implicit parameters are available and all the operations of the coeffect algebra are \(\cup\).
Data type for dataflow computations is a non-empty list, but to keep the example simpler, we'll write it just as a list:
type DF<'a> = DF of list<'a>
The counit operation returns the head, which is why we need a non-empty list!
The cobind operation takes a list and produces a list of the same length. It
is done by applying f to all the suffixes:
let counit (DF(v::_)) = v
let rec cobind f = function
| DF [] -> DF []
| DF (x::xs) ->
let (DF tl) = cobind f (DF xs)
DF(f (DF xs) :: tl)
cobind f [1;2;3] produces [f [1;2;3]; f [2;3]; f [3]]. The merge
operation is zip and split simply duplicates the list.
A special operation prev shifts the list by 1 element to the past:
let prev (DF(_::vs)) = DF(vs)
The coeffect annotations represent the number of past values needed. When you write
counit x, you don't need any past values (just the current one), but when you say
counit (prev x), you're accessing one past value.
In the coeffect algebra, \({\color{coeff}{\circledast}}, {\color{coeff}{\wedge}}, {\color{coeff}{\oplus}}\)
are \(+, \text{min}, \text{max}\).
Let's start by looking at a few examples that use implicit parameters. The first one is already loaded and translated!
|
Code to access an implicit parameter is translated into a call to the lookup function.
The values that you enter in the user interface are passed in as a special finput value.
|
When you use multiple implicit parameters, the split primitive is used to divide the
context between ctx1 and ctx2. Each will contain only the required parameters.
|
When we define a function, the input context finput is first merged with the one that
is attached to the input of the function. The x variable is num in the source, but
C {?param:num} num in the translation. All parameters are required from the caller and
they are kept with the input of the function.
|
This is the most interesting case, because ?param is bound locally, but ?other needs
to be defined when the function is called later.
The first line is not interesting, but the second one defines ctx which combines all
finput parameters (there are none) with a new assignment for ?param. The function
then merges ctx with x - the first one contains the value for ?param and the other one
stores the value for ?other. After that, the context is split again and we access both
of the parameters separately.
Load one of the samples on the left (or above) for simple demos, or choose a language and write your own snippet!
In the formatted code below,
you can see types of variables in a tooltip. Curried functions with multiple parameters
and function defined using let are expanded.
The translation for the flat dataflow is the same as for implicit parameters. One thing we did not discuss before is the handling of variables:
|
Variables are passed around in a tuple in the ctx value and they are extracted
using counit together with fst and snd to find the right one.
|
The prev keyword is mapped to prev the operation, which turns a comonad value with \(n\)
past values into one with \(n-1\) past values (dropping the current value).
In flat dataflow, we keep one annotation for the whole context, because we need the same number of past values for all the variables in the context. They are all just elements of one big tuple!
|
Now you can see why we need 1 past value of both x and y. We first merge all the variables
into a single context value ctx2. Because we then need 1 past value of the variable y,
we also end up requiring 1 past value of x. This is because merge behaves like zip and
it needs two lists of the same length.
In structural dataflow, things work a bit differently. We have annotations for individual
variables in the context. For example, a context containing y and x where we need the current
value of y and one value of x will be represented as C [0, 1] (num * num):
|
The variables x and y are merged into ctx2. The initial context is now sinput and it
contains empty tuple of variables with empty vector of annotations written as C [] ().
To select a subset of variables from a context, we're now using a family of operations choose_v
where the subscript v denotes which of the variables from the context we want to extract
(1 means keep, 0 means drop).
The place where things become really interesting is when we have function application. The
following calls a helper function that accesses the previous value of its argument on
a previous value of x:
|
We need two past values of x and one past value of v. In the translation, the value ctx1
carries two past values of x. The function (fun v -> ...) is then called with an argument
produced by cobind (fun ctx2 -> ...) (...). Here, both v and ctx2 need to have one past
value and cobind adds the requirements (this is the \(+\) in the coeffect algebra)!
Thanks for making it to the very end of this interactive essay. I hope you enjoyed it! If you want to read more about coeffects, we have more in the format of dead wood:
Coeffects: A calculus of context-dependent computation (ICFP 2014) is the most recent and the most complete paper about coeffects. It covers both flat and structural systems. It comes with a nice recording of my ICFP talk!
Coeffects: Unified static analysis of context-dependence (ICALP 2013) is our first paper about coeffects. It only discusses the flat system, but the side-effect of that is that all the theory is simpler.
Context-aware programming languages (submitted PhD thesis). This is the document to read if you're interested in all the details, but it also starts with a readable introduction and good explanation of the background.
Rather than including a list of references to previous programming language research related to coeffects (it is in the papers), I would like to list some inspirations for turning coeffects into an interactive essay.
The obvious inspiration is Bret Victor's work on Explorable Explanations and his Scientific Communication demo. But I actually learned about these only later when I started working on this!
What made me think about different ways of presenting academic research earlier was Robert Pirsig's Zen and the Art of Motorcycle Maintenance and The Medium is the Massage by Marshall McLuhan and Quentin Fiore. Finally, it was also the Future Programming Workshop organized by Jonathan Edwards. Thanks!