Practical coeffects

The context (or runtime environment) in which programs run is extremely important. Programs usually have requirements on this context, such as a requirement that some resource be available, and will fail if the requirements are not satisfied. The context may also affect the performance and monetary cost of a program. It is therefore necessary to track such requirements and other contextual information, either to avoid bugs or to improve performance. Since programming languages do not include support for this, it can only done on a case-by-case basis, using a range of different methods. These rarely work perfectly: the programmer may forget about a particular requirement for example. A general method of tracking contextual requirements would be better.

Type systems already found in programming languages serve a similar purpose, but are limited in the properties they can check. We can however consider type systems which are extended to track contextual information, allowing requirements to be enforced and information useful for optimization to be inferred. Coeffects, introduced by Petricek et al., are a promising method of doing this. Type-and-coeffect systems add to traditional typing judgements by associating an additional value -- a coeffect -- with the typing environment, and infer or check this value using rules that take into account, for example, which variables are used. Hence in situations where it is only valid to use a particular variable under some circumstances, a type-and-coeffect system would be able to ensure that this requirement is met. The availability of a resource is an example of this. Moreover, coeffects should allow these requirements to be checked without requiring the programmer to think about them everywhere they exist: this reduces the burden that is placed on them.

To use coeffects to check and optimize real programs, they need to be made practical. First, they require support from programming languages and their implementations -- this is the initial objective of my research. The support would need to include syntax for specifying coeffects and for operating on them, and support for inferring and checking coeffects. For this it will be necessary to determine how coeffects interact with features found in practical programming languages. Due to the relationship between coeffects and effects, Moggi's metalanguage for effects is a promising source of ideas for a dual framework.

The next objective is to show that coeffects are useful as a programming construct by studying practical applications. A rich source of these would likely be distributed systems. There may be a requirement, for example, for a particular part of a program to execute on a particular group of servers, and the choice of server may also affect the performance of the system. Coeffects could provide a way of specifying and enforcing these requirements, and of statically analyzing a program to determine which servers parts of it should be executed on.

Another source of applications is security. Tainting, in which a value becomes sensitive because sensitive data was used in its computation, could be modelled using coeffects, for example. Support in a programming language could allow programs to be checked by the type-and-coeffect system to ensure that sensitive data is only used where it should be, making code more trustworthy, with minimal additional work for the programmer.

Security and distributed systems are only two sources of applications; there are undoubtedly more. Additionally, further study of the theoretical properties of coeffects is a useful area of research.

This research will ensure that coeffects are of practical use to programmers.