Type- and Effect Systems

Type-systems are an important tool for programmers to rule out certain classes of errors, before running a program. Types are also indispensable to manage the complexity of large software by structuring it into smaller components with well-defined interfaces.

Effect systems extend these guarantees and equip the programmer with tools to reason about the presence or absence of potential (side-) effects.

Using effect systems, programmers can for instance

  • reason about exception-safety of a program (that is, “are all exceptions handled?”)
  • rule out data races (that is, “can I run these two programs safely in parallel?”)
  • establish security (that is, “can this plugin access the file system?”)
  • and many more…

In this research area, we investigate novel alternatives to establish effect safety that are lightweigt yet expressive. That is, they should be lightweight enough to not get into the way of programmers when concerned with other tasks while being expressive enough to enable the above modes of reasoning.

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

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

Reference Publication

Publications

Effects, Capabilities, and Boxes: From Scope-based Reasoning to Type-based Reasoning and Back

by Jonathan Immanuel Brachthäuser, Philipp Schuster, Edward Lee, and Aleksander Boruch-Gruszecki

In Accepted for publication in Proceedings of the International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2022.

Learn More

Tracking Captured Variables in Types

by Aleksander Boruch-Gruszecki, Jonathan Immanuel Brachthäuser, Edward Lee, Ondrej Lhoták, and Martin Odersky

In CoRR abs/2105.11896, 2021.

Learn More

Safer Exceptions for Scala

by Martin Odersky, Aleksander Boruch-Gruszecki, Jonathan Immanuel Brachthäuser, Edward Lee, and Ondřej Lhoták

In Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, pages 1–11. Association for Computing Machinery, 2021.

Learn More

Representing Monads with Capabilities

by Jonathan Brachthäuser, Aleksander Boruch-Gruszecki, and Martin Odersky

Technical report. Higher-Order Programming with Effects (HOPE), 2021.

Learn More

Effekt: Lightweight Effect Polymorphism for Handlers (Technical Report)

by Jonathan Immanuel Brachthäuser, Philipp Schuster, and Klaus Ostermann

Technical report. University of Tübingen, Germany, 2020.

Learn More