Type- and Effect Systems

Research Project: Contextual Effect Polymorphism

Combining tracking of effects with higher-order functions inevitably leads to effect polymorphism. However, effect polymorphism often complicates the types of programs and can lead to difficult error messages.

We introduce contextual polymorphism as an alternative to the traditional parametric polymorphism. Contextual effect polymorphism arises naturally in the context of lexical effect handlers by closing over capabilities.

Contextual effect polymorphism leads to concise types and supports lexical reasoning.

Current implementations of contextual effect polymorphism come with a set of limitations, such as limited reasoning about purity and restricted use of (first-class) function arguments. In this research project, we are investigating different effect systems, lifting these restrictions, with the goal to make contextual effect polymorphism widely applicable.

Collaborators

• Jonathan Brachthäuser (University of Tübingen)
• Philipp Schuster (University of Tübingen)
• Aleksander Boruch-Gruszecki (EPFL, Switzerland)
• Edward Lee (University of Waterloo)

Reference Publication

Research Project: Capability Safety

Retrofitting existing main-stream programming languages with support for effect systems is a difficult undertaking. Ideally, the extension is backwards compatible and existing programs do not need to be changed.

The Scala 3 programming language is well equipped with features for contextual abstraction, allowing programmers to model effects in terms of capabilities.

This way of expressing effects is not necessarily effect safe and thus runtime errors, such as unhandled exceptions, can occur. In this research project, we working on type-system based solutions that can establish effect safety in terms of capability safety. As an underlying mechanism, we enhance types with additional information, allowing programmers to answer questions, such as: "What capabilities do values of this type potentially close over?"

Collaborators

• Jonathan Brachthäuser (University of Tübingen)
• Martin Odersky (EPFL, Switzerland)
• Aleksander Boruch-Gruszecki (EPFL, Switzerland)
• Ondřej Lhoták (University of Waterloo)
• Edward Lee (University of Waterloo)

Reference Publication