Coeffects The next big programming challenge

Many advances in programming language design are driven by some practical motivations. Sometimes, the practical motivations are easy to see - for example, when they come from some external change such as the rise of multi-core processors. Sometimes, discovering the practical motivations is a tricky task - perhaps because everyone is used to a certain way of doing things that we do not even see how poor our current solution is.

The following two examples are related to the work done in F# (because this is what I'm the most familiar with), but you can surely find similar examples in other languages:

I believe that the next important practical challenge for programming language designers is of the kind that is not easy to see - because we are so used to doing things in certain ways that we cannot see how poor they are. The problem is designing languages that are better at working with (and understanding) the context in which programs are executed.

This article is a brief summary of the work that I did (am doing) during my PhD. It focuses on clearly explaining the motivation for the work, but if you're interested in the solution (and the theory), then you can find more on my academic home page.

Context-aware programming matters

The phrase context in which programs are executed sounds quite abstract and generic. What are some concrete examples of such context? For example:

These are all fairly standard problems that developers deal with today. As the number of devices where programs need to run increases, dealing with diverse contexts will be becoming more and more important (and I'm not even talking about ubiquitous computing where you need to compile your code to a coffee machine).

We do not perceive the above things as problems (at best, annoyances that we just have to deal with), because we do not realize that there should be a better way. Let me dig into four examples in a bit more detail.

Context awareness #1: Platform versioning

The number of different platform versions that you need to target is increasing, no matter what platform you are using. For Android, there is a number called API Level with mostly additive changes (mostly sounds very reassuring). In the .NET world, there are multiple versions, mobile editions, multiple versions of Silverlight etc. So, code that targets multiple frameworks easily ends up looking as the following sample from the Http module in F# Data:

for header, value in headers do
  match header with
  | StringEquals "accept" -> req.Accept <- value
  | StringEquals "user-agent" -> 
      req.Headers.[HttpRequestHeader.UserAgent] <- value
  | StringEquals "user-agent" -> req.UserAgent <- value
  | StringEquals "referer" -> 
      req.Headers.[HttpRequestHeader.Referer] <- value
  | StringEquals "referer" -> req.Referer <- value
  | _ -> req.Headers.[header] <- value

This is difficult to write (you won't know if the code even compiles until you try building all combinations) and maintaining such code is not particularly nice (try adding another platform version). Maybe we could refactor the code in F# Data to improve it, but that's not really my point - supporting multiple platforms should be a lot easier.

On Android, you can access API from higher level platform dynamically using techniques like reflection and writing wrappers. Again, this sounds very error prone - to quote the linked article "Remember the mantra: if you haven't tried it, it doesn't work". Testing is no doubt important. But at least in statically typed languages, we should not need to worry about calling a method that does not exist when writing multi-platform applications!

Context awareness #2: System capabilities

Another example related to the previous one is when you're using something like LINQ or FunScript to translate code written in a sub-set of C# or F# to some other language - such as SQL or JavaScript. This is another important area, because you can use this technique to target JavaScript, GPUs, SQL, Erlang runtime or other components that use a particular programming language.

For example, take a look at the following LINQ query that selects product names where the first upper case letter is "C":

var db = new NorthwindDataContext();

from p in db.Products
where p.ProductName.First(c => Char.IsUpper(c)) == "C"
select p.ProductName;

This looks like a perfectly fine piece of code and it compiles fine. But when you try running it, you get the following error:

Unhandled Exception: System.NotSupportedException: Sequence operators not supported for type System.String.

The problem is that LINQ can only translate a subset of normal C# code. Here, we are using the First method to iterate over characters of a string and that's not supported. This is not a technical limitation of LINQ, but a fundamental problem of the approach. If we target a limited language, we simply cannot support the full source language. Is this an important problem? If you search on Google for "has no supported translation to SQL" (which is a part of a similar error message that you get in another case), you get some 26900 links. So yes - this is an issue that people are hitting all the time.

Context awareness #3: Confidentiality and provenance

The previous two examples were mainly related to the (non-)existence of some API functions or to their behaviour. However, this is not the only case of context-awareness that is important in every day programming.

Most readers of this blog will immediately see what is wrong with the following code, but that does not change the fact that it can be compiled and deployed (and that there is a large number of systems that contain something similar):

let query = sprintf "SELECT * FROM Products WHERE ProductName = '%s'" name
use cmd = new SqlCommand(query)
use reader = cmd.ExecuteReader()

The problem is obviously SQL Injection. Concatenating strings to build an SQL command is a bad practice, but it is an example of a more general problem.

Sometimes, we have special kinds of variables that should have some contextual meta-data associated with them. Such meta-data can dictate how the variable can be used. Here, name comes from the user input and this provenance information should propagate to query and we should get an error when we try passing this - potentially unsafe - input to SqlCommand. Similarly, if you have password or creditCard, it should be annotated with meta-data saying that this is a sensitive piece of data and should not, for example, be sent over an unsecured network connection. As a side note - this idea is related to a technique called taint checking.

In another context, if you are working with data (e.g. in some data journalism application), it would be great if your sources were annotated with meta-data about the quality and source of the data (e.g. can it be trusted? how up-to-date is it?) The meta-data could propagate to the result and tell you how accurate and trustworthy your result is.

Context-awareness #4: Resource & data availability

A vast majority of applications accesses some data sources (like database) or resources (like GPS sensor on a phone). This is more tricky for client/server applications where a part of program runs on the server-side and another part runs on the client-side. I believe that these two parts should be written as a single program that is cross-compiled to two parts (and I tried to make that possible with F# Web Tools a long time ago; more recently WebSharper implemented a similar idea).

So, say we have a function validateInput, readData and displayMessage in my program. I want to look at their types and see what resources (or context) they require. For example, readData requires database (or perhaps a database with a specific name), displayMessage requires access to user interface and validateInput has no special requirements.

This means that I can call validateInput from both server-side and client-side code - it is safe to share this piece of code, because it has no special requirements. However, when I write a code that calls all three functions without any remote calls, it will only run on a thick client that has access to a database as well as user interface.

I'll demonstrate this idea with a sample (pseudo-)code in a later section, so do not worry if it sounds a bit abstract at first.

Coeffects: Towards context-aware languages

The above examples cover a couple of different scenarios, but they share a common theme - they all talk about some context in which an expression is evaluated. The context has essentially two aspects:

As a proponent of statically typed functional languages I believe that a context-aware programming language should capture such context information in the type system and make sure that basic errors (like the ones demonstrated in the four examples above) are ruled out at compile time.

This is essentially the idea behind coeffects. Let's look at an example showing the idea in (a very simplified) practice and then I'll say a few words about the theory (which is the main topic of my upcoming PhD thesis).

Case study: Coeffects in action

So, how should a context-aware language look? Surely, there is a wide range of options, but I hope I convinced you that it needs to be context-aware in some way! I'll write my pseudo-example in a language that looks like F#, is fully statically typed and uses type inference.

I think that type inference is particularly important here - we want to check quite a few properties that should not that difficult to infer (If I call a function that needs GPS, I need to have GPS access!) Writing all such information by hand would be very cumbersome.

So, let's say that we want to write a client/server news reader where the news are stored in a database on a server. When a client (iPhone or Windows phone) runs, we get GPS location from the phone and query the server that needs to connect to the "News" database using a password defined somewhere earlier (perhaps loaded from a server-side config file):

let lookupNews(location) =
  let db = query("News", password)
  selectNews(db, location)  

let readNews() =
  let loc = gpsLocation()       
  remote { 

let iPhoneMain() =

let windowsMain() =    

The idea is that lookupNews is a server-side function that queries the "News" database based on the specified location. This is called from the client-side by readNews which get the current GPS position and uses a remote { .. } block to invoke the lookupNews function remotely (how exactly would this be written is a separate question - but imagine a simple REST request here).

Then, we have two main functions, iPhoneMain and windowsMain that will serve as two entry points for iPhone and Windows build of the client-side application. They are both using a corresponding platform-specific function to build the user interface, which takes a function for reading news as an argument.

If you wanted to write and compile something like this today, you could use F# in Xamarin Studio to target iPhone and Window phone, but you'd either need two separate end-application projects or a large number of unmaintainable #if constructs. Why not just use a single project, if the application is fairly simple?

I imagine that a context-aware statically typed language would let you write the above code and if you inspected the types of the functions, you would see something like this:

password      :   string { sensitive }
lookupNews    :   Location { database } → list<News>

gpsLocation   :   unit { gps } → Location
readNews      :   unit { rpc, gps } → Async<list<News>>

iPhoneMain    :   unit { cocoa, gps, rpc } → unit
windowsMain   :   unit { metro, gps, rpc } → unit

The syntax is something that I just made up for the purpose of this article - it could look different. Some information could even be mapped to other visual representations (e.g. blueish background for the function body in your editor). The key thing is that we can learn quite a lot about the context usage:

When writing the application, I want to be always able to see this information (perhaps similarly to how you can see type information in the various F# editors). I want to be able to reference multiple versions of base libraries - one for iPhone and another for Windows and see all the API functions at the same time, with appropriate annotations. When a function is available on both platforms, I want to be able to reuse the code that calls it. When some function is available on only one platform, I want to solve this by designing my own abstraction, rather than resorting to ugly #if pragmas.

Then, I want to take this single program (again, structured using whatever abstractions I find appropriate) and compile it. As a result, I want to get a component (containing lookupNews) that I can deploy to the server-side and two packages for iPhone and Windows respectively, that reference only one or the other platform.

Coeffects: Theory of context dependence

If you're expecting a "Download!" button or (even better) a "Buy now!" button at the end of this article, then I'll disappoint you. I have no implementation that would let you do all of this. My work in this area has been (so far) on the theoretical side. This is a great way to understand what is actually going on and what does the context mean. And if you made it this far, then it probably worked, because I understood the problem well enough to be write a readable article about it!

If you are interested in the theory, then go ahead and have a look at our papers about coeffects, otherwise continue reading and I'll try to introduce the key ideas in a more accessible form!

Brief introduction to type systems

I won't try to reproduce the entire content of the papers in this blog post - but I will try to give you some background in case you are interested (that should make it easier to look at the papers above). We'll start from the basics, so readers familiar with theory of programming languages can skip to the next section.

Type systems are usually described in the form of typing judgement that have the following form:

The judgement means that, given some variables described by Γ, the expression or program e has a type τ. What does this mean? For example, what is a type of the expression x + y? Well, this depends - in F# it could be some numeric type or even a string, depending on the types of x and y. That's why we need the variable context Γ which specifies the types of variables. So, for example, we can have:

Here, we assume that the types of x and y (on the left hand side) are both int and as a result, we derive that the type of x + y is also an int. This is a valid typing, for the expression, but not the only one possible - if x and y were of type string, then the result would also be string.

Checking what program does with effect systems

Type systems can be extended in various interesting ways. Essentially, they give us an approximation of the possible values that we can get as a result. For example refinement types can estimate numerical values more precisely (e.g. less than 100). However, it is also possible to track what a program does - how it affects the world. For example, let's look at the following expression that prints a number:

This is a reasonable typing in F# (and ML languages), but it ignores the important fact that the expression has a side-effect and prints the number to the console. In Haskell, this would not be a valid typing, because print would return an IO computation rather than just plain unit (for more information see IO in Haskell).

However, monads are not the only way to be more precise about side-effects. Another option is to use an effect system which essentially annotates the result of the typing judgement with more information about the effects that occur as part of evaluation of the expression (here, in orange):

The effect annotation is now part of the type - so, the expression has a type unit & { io } meaning that it does not return anything useful, but it performs some I/O operation. Note that we do not track what exactly it does - just some useful over-approximation. How do we infer the information? The compiler needs to know about certain language primitives (or basic library functions). Here, print is a function that performs I/O operation.

The main role of the type system is dealing with composition - so, if we have a function read that reads from the console (I/O operation) and a function send that sends data over network, the type system will tell us that the type and effects of send (read ()) are unit & {io, network}.

Effect systems are a fairly established idea - and they are a nice way to add better purity checking to ML-like languages like F#. However, they are not that widely adopted (interestingly, checked exceptions in Java are probably the most major use of effect system). However, effect systems are also a good example of general approach that we can use for tracking contextual information...

Checking what program requires with coeffect systems

How could we use the same idea of annotating the types to capture information about the context? Let's look at a part of the program from the case study that I described earlier:

The expression queries a database and gets back a value of the NewsDb type (for now, let's say that "News" is a constant string and query behaves like the SQL type provider in F# and generates the NewsDb type automatically).

What information do we want to capture? First of all, we want to add an annotation saying that the expression requires database access. Secondly, we want to mark the pass variable as secure to guarantee that it will not be sent over an unsecured network connection etc. The coeffect typing judgement representing this information looks like this:

Rather than attaching the annotations to the resulting type, they are attached to the variable context. In other words, the equation is saying - given a variable pass that is marked as secure and additional environment providing database access, the expression query("News", pass) is well typed and returns a NewsDb value.

As a side-note, it is well known that effects correspond to monads (and Haskell uses monads as a way of implementing limited effect checking). Quite interestingly, coeffects correspond to the dual concept called comonads and, with a syntactic extension akin to the do notation or computation expressions, you could capture contextual properties by adding comonads to a language.


This article is essentially a tabloid style report on my (upcoming) PhD thesis :-).

I started by explaining the motivation for my work - different problems that arise when we are writing programs that are aware of the context in which they run. The context includes things such as execution environment (databases, resources, available devices), platform and framework (different versions, different platforms) and meta-data about data we access (sensitivity, security, provenance).

This may not be perceived as a major problem - we are all used to write code that deals with such things. However, I believe that the area of context-aware programming is a source of many problems and pains - and programming languages can help!

In the second half of the article, I gave a brief introduction to coeffects - a programming language theory that can simplify dealing with context. The key idea is that we can use types to track and check additional information about the context. By propagating such information throughout the program (using type system that is aware of the annotations), we can make sure that none of the errors that I used as a motivation for this article happen.

Where to go next?

If you want to learn more about the theory of coeffects (and how they relate to comonads) then check out the two papers I mentioned earlier:

Dominic Orchard (who is co-author of the above two) also did some nice work on integrating comonads into Haskell:

val header : string
val value : string
val headers : (string * string) list

Full name: whycoeffectsmatter.headers
active recognizer StringEquals: 'a -> 'b -> unit option

Full name: whycoeffectsmatter.( |StringEquals|_| )
val req : System.Net.HttpWebRequest

Full name: whycoeffectsmatter.req
property System.Net.HttpWebRequest.Accept: string
property System.Net.HttpWebRequest.UserAgent: string
property System.Net.HttpWebRequest.Referer: string
property System.Net.HttpWebRequest.Headers: System.Net.WebHeaderCollection
val query : string

Full name: whycoeffectsmatter.query
val sprintf : format:Printf.StringFormat<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.sprintf
val name : string

Full name:
val cmd : SqlCommand

Full name: whycoeffectsmatter.cmd
Multiple items
type SqlCommand =
  inherit DbCommand
  new : unit -> SqlCommand + 3 overloads
  member BeginExecuteNonQuery : unit -> IAsyncResult + 1 overload
  member BeginExecuteReader : unit -> IAsyncResult + 3 overloads
  member BeginExecuteXmlReader : unit -> IAsyncResult + 1 overload
  member Cancel : unit -> unit
  member Clone : unit -> SqlCommand
  member CommandText : string with get, set
  member CommandTimeout : int with get, set
  member CommandType : CommandType with get, set
  member Connection : SqlConnection with get, set

Full name: System.Data.SqlClient.SqlCommand

SqlCommand() : unit
SqlCommand(cmdText: string) : unit
SqlCommand(cmdText: string, connection: SqlConnection) : unit
SqlCommand(cmdText: string, connection: SqlConnection, transaction: SqlTransaction) : unit
val reader : SqlDataReader

Full name: whycoeffectsmatter.reader
SqlCommand.ExecuteReader() : SqlDataReader
SqlCommand.ExecuteReader(behavior: System.Data.CommandBehavior) : SqlDataReader
val lookupNews : location:Location -> string list

Full name: whycoeffectsmatter.lookupNews
val location : Location
val db : Database
val query : database:'a * password:string -> Database

Full name: whycoeffectsmatter.query
val password : string

Full name: whycoeffectsmatter.password
val selectNews : db:Database * loc:Location -> string list

Full name: whycoeffectsmatter.selectNews
val readNews : unit -> unit

Full name: whycoeffectsmatter.readNews
val loc : Location
val gpsLocation : unit -> Location

Full name: whycoeffectsmatter.gpsLocation
val remote : RemoteBuilder

Full name: whycoeffectsmatter.remote
val iPhoneMain : unit -> unit

Full name: whycoeffectsmatter.iPhoneMain
val createCocoaWidget : f:(unit -> 'a) -> unit

Full name: whycoeffectsmatter.createCocoaWidget
val windowsMain : unit -> unit

Full name: whycoeffectsmatter.windowsMain
val createMetroWidget : f:(unit -> 'a) -> unit

Full name: whycoeffectsmatter.createMetroWidget

Published: Wednesday, 8 January 2014, 4:31 PM
Author: Tomas Petricek
Typos: Send me a pull request!
Tags: research, coeffects, functional programming, comonads