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.

\[ \definecolor{leff}{RGB}{255,107,102} \definecolor{lcoeff}{RGB}{78,206,88} \definecolor{ltyp}{RGB}{255,202,79} \definecolor{lkvd}{RGB}{127,165,255} \definecolor{eff}{RGB}{177,35,43} \definecolor{coeff}{RGB}{35,177,53} \definecolor{typ}{RGB}{177,93,43} \definecolor{expr}{RGB}{0,0,0} \definecolor{kvd}{RGB}{0,45,177} \definecolor{num}{RGB}{43,177,93} \]

What problem are coeffects solving?

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!

Cross-platform caching

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.

val readFromCache : key:string -> f:(unit -> string) -> string

Full name: Document.readFromCache
val key : string
val f : (unit -> string)
val cache : Cache

Full name: Document.cache
member Cache.Contains : key:string -> bool
member Cache.Get : key:string -> string
val result : string
member Cache.Set : key:string * value:string -> unit

Stencil computations

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.

val sum : int

Full name: Document.sum
val input : int []

Full name: Document.input
val cursor : int

Full name: Document.cursor
val output : int []

Full name: Document.output

Simple type systems

To understand effects and coeffects, let's look at how their type systems work. In languages like F#, the following holds:

\[x:{\color{ltyp} \text{int}},~ y:{\color{ltyp} \text{int}} \vdash x+y : {\color{ltyp} \text{int}}\]

This says that in a context with variablex \(x\) and \(y\) of type \(\color{ltyp}\text{int}\), the type of expression \(x+y\) is also \(\color{ltyp}\text{int}\). The context on the left of \(\vdash\) is important! If the variables \(x\) and \(y\) had incompatible types, this would not be well-typed!

Effect systems

The type of expressions with side-effect is \(\color{ltyp}\text{unit}\), which does not tell us very much! Effect systems add one more component:

\[hello : {\color{ltyp} \text{string}} \vdash {\color{lkvd} \text{print}}~hello : {\color{ltyp} \text{unit}} {\scriptsize \;\&\;} {\color{leff} \{ \text{io} \} }\]

Effect systems understand built-in functions like \({\color{lkvd} \text{print}}\) and they infer not just the type of an expression, but also an effect. Here \({\color{leff} \{ \text{io} \} }\) means that the expression requires I/O access but not, for example, direct access to mutable memory.

Coeffect systems

Coeffects add an annotation to the context of an expression. For example, checking whether we missed a deadline returns \(\color{ltyp} \text{bool}\) and requires a set of resources \(\color{lcoeff} \{ \text{clock} \}\):

\[deadline : {\color{ltyp} \text{time}} {\scriptsize \;@\;} {\color{lcoeff} \{ \text{clock} \} } \vdash {\color{lkvd} \text{now}} \geq deadline : {\color{ltyp} \text{bool}}\]

Coeffects can do more though. We can add requirements to the whole context (as here), but also to individual variables. We will do this later for checking dataflow computations.

Type systems side-by-side

\[\Gamma \vdash e : {\color{ltyp} \tau}\]

In standard type systems, we say that given variables in \(\Gamma\), an expression \(e\) has a type \({\color{ltyp} \tau}\):

\[\Gamma \vdash e : {\color{ltyp} \tau} {\scriptsize \;\&\;} {\color{leff} r}\]

Effect systems add annotation to the result. Given variables in \(\Gamma\), an expression \(e\) has a type \({\color{ltyp} \tau}\) and an effect \({\color{leff} r}\):

\[\Gamma {\scriptsize \;@\;} {\color{lcoeff} r} \vdash e : {\color{ltyp} \tau}\]

Coeffect systems say more about the context. Given a variables in \(\Gamma\) and additional context \({\color{lcoeff} r}\) an expression \(e\) has a type \({\color{ltyp} \tau}\):

Lambda abstraction

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.

Structural coeffects

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!

Comonadic semantics

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.

Two coeffect languages

Implicit parameters

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.

Dataflow language

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.

How does the coeffect playground work?

You choose a snippet. Coeffect system checks it.

The system infers the names of the required implicit parameters or the required number of past values in the input streams.

Behind the scenes, the snippet is desugared.

In the translated code, implicit parameters are passed around as dictionaries and streams become lists of values.

Enter inputs and run the code. It cannot fail!

The coeffect type system guarantees that program accesses only the values that it asks for and so the program runs correctly!

Implicit parameters

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:

  • Numbers 42, variables foo and implicit parameters ?foo
  • Numerical operators +, -, *, / and ^
  • Let binding let x = e1 in e2 where in is required
  • Application e1 e2 and functions fun x -> e
  • Define a named function using let foo x = x + 1 in ...
  • Curring is supported. For example: fun x y -> x + y

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

?fst + ?snd

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.

Static and dynamic scoping

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:

let dyn =
  (fun snd -> ?fst + snd) in
let ?fst = 10 in dyn ?other

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:

let lex =
  let ?fst = 10 in
  (fun snd -> ?fst + snd) in
lex ?other

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.

Resolving ambiguity

let both =
  let ?fst = 100 in
  (fun trd -> ?fst + ?snd + trd) in
let ?fst = 200 in both 1

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.

Dataflow computations

fun n -> (n + prev n) / 2

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!

Structural and flat coeffects

edit
let flat x y = x + prev y in
flat

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 following snippet is checked using the structural coeffect system. The type of struct says that we need one past value of y but only the current value of x:

edit
let struct x y = x + prev y in
struct

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:

Interactive dataflow programs

let oldx x y =
  let prev4 v = prev prev prev prev v in
  prev4 (prev4 (prev4 x)) in
oldx

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.

let smooth x y =
  let sum4 v = v + prev (v + prev (v + prev v)) in
  let prev4 v = prev prev prev prev v in
  let s1 = sum4 x + sum4 (prev4 x) in
  let s2 = sum4 (prev4 (prev4 x)) in
  (s1 + s2) / 12 in
smooth

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

let speed x y =
  let dx = x - prev x in
  let dy = y - prev y in
  dx * dx + dy * dy
in speed

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!

Move mouse or touch
here to get started!

Why languages need coeffects?

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.

Theory of coeffects

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 is 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 function define how the concrete contextual information are passed around and used.

Coeffect type system

Lambda abstraction

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.

Pure languages

Given a function body \(e\) of type \({\color{ltyp}\tau_2}\) and a variable \(x\) of type \({\color{ltyp}\tau_1}\), the expression \({\color{lkvd} \text{fun}}~x \rightarrow e\) creates a function of type \({\color{ltyp}\tau_1 \rightarrow \tau_2}\).

\[\dfrac {\Gamma, x:{\color{ltyp} \tau_1} \vdash e : {\color{ltyp} \tau_2}} {\Gamma \vdash {\color{lkvd} \text{fun}}~x \rightarrow e : {\color{ltyp} \tau_1} \rightarrow {\color{ltyp} \tau_2}}\]

This is the standard textbook lambda abstraction rule. Now, let's look what happens for effect and coeffect systems!

Effect systems

In effectful language, the body \(e\) has an additional effect \({\color{leff} r}\). This could be writing to console, modifying memory, network communication etc.

\[\dfrac {\Gamma, x:{\color{ltyp} \tau_1} \vdash e : {\color{ltyp} \tau_2 } {\scriptsize \;\&\;} {\color{leff} r} } {\Gamma \vdash {\color{lkvd} \text{fun}}~x \rightarrow e : {\color{ltyp} \tau_1} \xrightarrow{~\color{leff} r~} {\color{ltyp} \tau_2} {\scriptsize \;\&\;} {\color{leff} \emptyset}}\]

The effect of the function creation is \({\color{leff} \emptyset}\), meaning that nothing happens when the function is created. All the effects \({\color{leff} r}\) are delayed and attached to the type of the function. They occur when the function is called.

Coeffect systems

With coeffects, the body has additional contextual requirements, but those can be split between the immediate coeffects \({\color{lcoeff} r}\) (required when creating the function) and delayed coeffects \({\color{lcoeff} s}\) (required when the function is called).

\[\dfrac {\Gamma, x:{\color{ltyp} \tau_1} {\scriptsize \;@\;} {\color{lcoeff} r\wedge s} \vdash e : {\color{ltyp} \tau_2 } } {\Gamma {\scriptsize \;@\;} {\color{lcoeff} r} \vdash {\color{lkvd} \text{fun}}~x \rightarrow e : {\color{ltyp} \tau_1} \xrightarrow{~\color{lcoeff} s~} {\color{ltyp} \tau_2}}\]

How \({\color{lcoeff} \wedge}\) works depends on the concrete language. For implicit parameters, it captures as many available parameters as possible and delays the rest.

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!

Flat coeffect system

In the general version, coeffects are combined using the operations of the coeffect algebra. \({\color{lcoeff} \sf \text{use}}\) represents the coeffect of variable access and \({\color{lcoeff} \wedge}\) appears in lambda abstraction as earlier.

\[\dfrac {x:{\color{ltyp} \tau} \in \Gamma} {\Gamma {\scriptsize \;@\;} {\color{lcoeff} \sf \text{use}} \vdash x : {\color{ltyp} \tau}}\]

\[\dfrac {\Gamma, x:{\color{ltyp} \tau_1} {\scriptsize \;@\;} {\color{lcoeff} r\wedge s} \vdash e : {\color{ltyp} \tau_2 } } {\Gamma {\scriptsize \;@\;} {\color{lcoeff} r} \vdash {\color{lkvd} \text{fun}}~x \rightarrow e : {\color{ltyp} \tau_1} \xrightarrow{~\color{lcoeff} s~} {\color{ltyp} \tau_2}}\]

\[\dfrac {\Gamma {\scriptsize \;@\;} {\color{lcoeff} r} \vdash e_1 : {\color{ltyp} \tau_1} \xrightarrow{~\color{lcoeff} t~} {\color{ltyp} \tau_2} ~~~~~~ \Gamma {\scriptsize \;@\;} {\color{lcoeff} s} \vdash e_2 : {\color{ltyp} \tau_1} } {\Gamma {\scriptsize \;@\;} {\color{lcoeff} r \oplus (s \circledast t)} \vdash e_1~e_2 : {\color{ltyp} \tau_2}}\]

In application, we use point-wise composition \({\color{lcoeff} \oplus}\). On the left, we reduce \(e_1\) to a function. On the right, we evaluate its argument and then the function. The function call is modelled by sequential composition \({\color{lcoeff} \circledast}\) of the coeffect of the argument and of the function.

Implicit parameter coeffects

The coeffect algebra of implicit parameters is simple. A variable access requires no implicit parameters and is annotated with \({\color{lcoeff} \emptyset}\) (there is a separate rule for accessing implicit parameters).

\[\dfrac {x:{\color{ltyp} \tau} \in \Gamma} {\Gamma {\scriptsize \;@\;} {\color{lcoeff} \emptyset} \vdash x : {\color{ltyp} \tau}}\]

\[\dfrac {\Gamma, x:{\color{ltyp} \tau_1} {\scriptsize \;@\;} {\color{lcoeff} r\cup s} \vdash e : {\color{ltyp} \tau_2 } } {\Gamma {\scriptsize \;@\;} {\color{lcoeff} r} \vdash {\color{lkvd} \text{fun}}~x \rightarrow e : {\color{ltyp} \tau_1} \xrightarrow{~\color{lcoeff} s~} {\color{ltyp} \tau_2}}\]

\[\dfrac {\Gamma {\scriptsize \;@\;} {\color{lcoeff} r} \vdash e_1 : {\color{ltyp} \tau_1} \xrightarrow{~\color{lcoeff} t~} {\color{ltyp} \tau_2} ~~~~~~ \Gamma {\scriptsize \;@\;} {\color{lcoeff} s} \vdash e_2 : {\color{ltyp} \tau_1} } {\Gamma {\scriptsize \;@\;} {\color{lcoeff} r \cup (s \cup t)} \vdash e_1~e_2 : {\color{ltyp} \tau_2}}\]

In both lambda abstraction and application, we combine the coeffects using \({\color{lcoeff} \cup}\). A body of a lambda has access to a combination of available parameters and an application requires all parameters that are needed by the sub-expressions.

Dataflow coeffects

Accessing the value of a variable requires \({\color{lcoeff} 0}\) past values. A function body can access \({\color{lcoeff} \text{min}}\) of the past values that are available for the variables in scope and the bound variable \(x\).

\[\dfrac {x:{\color{ltyp} \tau} \in \Gamma} {\Gamma {\scriptsize \;@\;} {\color{lcoeff} 0} \vdash x : {\color{ltyp} \tau}}\]

\[\dfrac {\Gamma, x:{\color{ltyp} \tau_1} {\scriptsize \;@\;} {\color{lcoeff} \text{min}(r, s)} \vdash e : {\color{ltyp} \tau_2 } } {\Gamma {\scriptsize \;@\;} {\color{lcoeff} r} \vdash {\color{lkvd} \text{fun}}~x \rightarrow e : {\color{ltyp} \tau_1} \xrightarrow{~\color{lcoeff} s~} {\color{ltyp} \tau_2}}\]

\[\dfrac {\Gamma {\scriptsize \;@\;} {\color{lcoeff} r} \vdash e_1 : {\color{ltyp} \tau_1} \xrightarrow{~\color{lcoeff} t~} {\color{ltyp} \tau_2} ~~~~~~ \Gamma {\scriptsize \;@\;} {\color{lcoeff} s} \vdash e_2 : {\color{ltyp} \tau_1} } {\Gamma {\scriptsize \;@\;} {\color{lcoeff} \text{max}(r, s + t)} \vdash e_1~e_2 : {\color{ltyp} \tau_2}}\]

In application, we need \({\color{lcoeff} s+t}\) past values to produce \({\color{lcoeff} t}\) past values (to call the function) using an expression \(e_2\) that requires \({\color{lcoeff} s}\) past values to produce a single value. The overall context also needs to have enough past values to satisfy the requirements of \(e_1\).

Flat coeffect systems

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 coeffect systems

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.

Interactive coeffect type checker

Choose a coeffect language from the dropdown and load a sample snippet to get started.

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.



        

Now explore the typing derivation. Click on the judgements in the assumptions to navigate through the typing derivation. Compare flat and structural dataflow typing for the same program!

Comonadic translation

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.

Comonads for stencil computations

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.01.01.0
0.02.02.0
2.03.04.0
???
???
???

How is this captured by a comonad?

  • The type \(C {\color{ltyp} \tau}\) is a two dimensional grid of \(\tau\) values together with the coordinates of a current position in the grid.
  • The counit operation returns the value at the current position.
  • The cobind operation produces a new grid of the same size as the input and it calls the given function for all possible positions in the input grid.

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

Implicit parameters

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\).

Dataflow computations

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}\).

Multiple items
union case IP.IP: 'a * (string -> obj) -> IP<'a>

--------------------
type IP<'a> = | IP of 'a * (string -> obj)

Full name: Document.IP<_>
Multiple items
val string : value:'T -> string

Full name: Microsoft.FSharp.Core.Operators.string

--------------------
type string = System.String

Full name: Microsoft.FSharp.Core.string
type obj = System.Object

Full name: Microsoft.FSharp.Core.obj
val counit : IP<'a> -> 'a

Full name: Document.counit
val v : 'a
val cobind : f:(IP<'a> -> 'b) -> IP<'a> -> IP<'b>

Full name: Document.cobind
val f : (IP<'a> -> 'b)
val p : (string -> obj)
val p1 : (string -> obj)
val p2 : (string -> obj)
val lookup : name:string -> IP<'a> -> obj

Full name: Document.lookup
val name : string
val f : (string -> obj)
Multiple items
union case DF.DF: 'a list -> DF<'a>

--------------------
type DF<'a> = | DF of 'a list

Full name: Document.DF<_>
type 'T list = List<'T>

Full name: Microsoft.FSharp.Collections.list<_>
val counit : DF<'a> -> 'a

Full name: Document.counit
val cobind : f:(DF<'a> -> 'b) -> _arg1:DF<'a> -> DF<'b>

Full name: Document.cobind
val f : (DF<'a> -> 'b)
val x : 'a
val xs : 'a list
val tl : 'b list
val prev : DF<'a> -> DF<'a>

Full name: Document.prev
val vs : 'a list

Implicit parameters

Let's start by looking at a few examples that use implicit parameters. The first one is already loaded and translated!

?param

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.

?one + ?two

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.

fun x -> x + ?param

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.

let ?param = 10 in
fun x -> ?param + ?other

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.


            

          

Flat dataflow

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:

fun x -> x

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.

fun x -> x + prev x

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!

fun x y -> x + prev y

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.

Structural dataflow

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):

fun x y -> prev x

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:

fun x -> (fun v -> prev v) (prev 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)!

Inspiration and references

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:

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!