Software Engineering

Type- and Effect Systems

Type-sys­tems are an im­por­tant tool for pro­gram­mers to rule out cer­tain classes of er­rors, be­fore run­ning a pro­gram. Types are also in­dis­pens­able to man­age the com­plex­ity of large soft­ware by struc­tur­ing it into smaller com­po­nents with well-de­fined in­ter­faces.

Ef­fect sys­tems ex­tend these guar­an­tees and equip the pro­gram­mer with tools to rea­son about the pres­ence or ab­sence of po­ten­tial (side-) ef­fects.

Using ef­fect sys­tems, pro­gram­mers can for in­stance

  • rea­son about ex­cep­tion-safety of a pro­gram (that is, “are all ex­cep­tions han­dled?”)
  • rule out data races (that is, “can I run these two pro­grams safely in par­al­lel?”)
  • es­tab­lish se­cu­rity (that is, “can this plu­gin ac­cess the file sys­tem?”)
  • and many more…

In this re­search area, we in­ves­ti­gate novel al­ter­na­tives to es­tab­lish ef­fect safety that are light­weigt yet ex­pres­sive. That is, they should be light­weight enough to not get into the way of pro­gram­mers when con­cerned with other tasks while being ex­pres­sive enough to en­able the above modes of rea­son­ing.

Re­search Pro­ject: Con­tex­tual Ef­fect Poly­mor­phism

Com­bin­ing track­ing of ef­fects with higher-or­der func­tions in­evitably leads to ef­fect poly­mor­phism. How­ever, ef­fect poly­mor­phism often com­pli­cates the types of pro­grams and can lead to dif­fi­cult error mes­sages.

We in­tro­duce con­tex­tual poly­mor­phism as an al­ter­na­tive to the tra­di­tional para­met­ric poly­mor­phism. Con­tex­tual ef­fect poly­mor­phism arises nat­u­rally in the con­text of lex­i­cal ef­fect han­dlers by clos­ing over ca­pa­bil­i­ties.

Con­tex­tual ef­fect poly­mor­phism leads to con­cise types and sup­ports lex­i­cal rea­son­ing.

Cur­rent im­ple­men­ta­tions of con­tex­tual ef­fect poly­mor­phism come with a set of lim­i­ta­tions, such as lim­ited rea­son­ing about pu­rity and re­stricted use of (first-class) func­tion ar­gu­ments. In this re­search pro­ject, we are in­ves­ti­gat­ing dif­fer­ent ef­fect sys­tems, lift­ing these re­stric­tions, with the goal to make con­tex­tual ef­fect poly­mor­phism widely ap­plic­a­ble.

Col­lab­o­ra­tors

Ref­er­ence Pub­li­ca­tion

Re­search Pro­ject: Ca­pa­bil­ity Safety

Retro­fitting ex­ist­ing main-stream pro­gram­ming lan­guages with sup­port for ef­fect sys­tems is a dif­fi­cult un­der­tak­ing. Ide­ally, the ex­ten­sion is back­wards com­pat­i­ble and ex­ist­ing pro­grams do not need to be changed.

The Scala 3 pro­gram­ming lan­guage is well equipped with fea­tures for con­tex­tual ab­strac­tion, al­low­ing pro­gram­mers to model ef­fects in terms of ca­pa­bil­i­ties.

This way of ex­press­ing ef­fects is not nec­es­sar­ily ef­fect safe and thus run­time er­rors, such as un­han­dled ex­cep­tions, can occur. In this re­search pro­ject, we work­ing on type-sys­tem based so­lu­tions that can es­tab­lish ef­fect safety in terms of ca­pa­bil­ity safety. As an un­der­ly­ing mech­a­nism, we en­hance types with ad­di­tional in­for­ma­tion, al­low­ing pro­gram­mers to an­swer ques­tions, such as: "What ca­pa­bil­i­ties do val­ues of this type po­ten­tially close over?"

Col­lab­o­ra­tors

Ref­er­ence Pub­li­ca­tion

Pub­li­ca­tions

Ef­fects, Ca­pa­bil­i­ties, and Boxes: From Scope-based Rea­son­ing to Type-based Rea­son­ing and Back

by Jonathan Im­manuel Brachthäuser, Philipp Schus­ter, Ed­ward Lee, and Alek­sander Boruch-Gruszecki

In Pro­ceed­ings of the In­ter­na­tional Con­fer­ence on Ob­ject-Ori­ented Pro­gram­ming, Sys­tems, Lan­guages and Ap­pli­ca­tions (OOP­SLA), 2022.

Learn More

Qual­i­fy­ing Sys­tem F-sub

by Ed­ward Lee, Yaoyu Zhao, Ondřej Lhoták, James You, Kavin Satheesku­mar, and Jonathan Im­manuel Brachthäuser

In Pro­ceed­ings of the In­ter­na­tional Con­fer­ence on Ob­ject-Ori­ented Pro­gram­ming, Sys­tems, Lan­guages and Ap­pli­ca­tions (OOP­SLA), 2024.

Learn More

From Ca­pa­bil­i­ties to Re­gions: En­abling Ef­fi­cient Com­pi­la­tion of Lex­i­cal Ef­fect Han­dlers

by Mar­ius Müller, Philipp Schus­ter, Jonathan Lin­de­gaard Starup, Klaus Os­ter­mann, and Jonathan Im­manuel Brachthäuser

In Pro­ceed­ings of the In­ter­na­tional Con­fer­ence on Ob­ject-Ori­ented Pro­gram­ming, Sys­tems, Lan­guages and Ap­pli­ca­tions (OOP­SLA), 2023.

Learn More

With or With­out You: Pro­gram­ming with Ef­fect Ex­clu­sion

by Matthew Lutze, Mag­nus Mad­sen, Jonathan Im­manuel Brachthäuser, and Philipp Schus­ter

In Pro­ceed­ings of the In­ter­na­tional Con­fer­ence on Func­tional Pro­gram­ming (ICFP). ACM Press, 2023.

Learn More

Get­ting into the Flow: To­wards Bet­ter Type Error Mes­sages for Con­straint-Based Type In­fer­ence

by Ishan Bhanuka, Li­onel Par­reaux, David Binder, and Jonathan Im­manuel Brachthäuser

In Pro­ceed­ings of the In­ter­na­tional Con­fer­ence on Ob­ject-Ori­ented Pro­gram­ming, Sys­tems, Lan­guages and Ap­pli­ca­tions (OOP­SLA), 2023.

Learn More

Track­ing Cap­tured Vari­ables in Types

by Alek­sander Boruch-Gruszecki, Jonathan Im­manuel Brachthäuser, Ed­ward Lee, On­drej Lhoták, and Mar­tin Oder­sky

In CoRR abs/2105.11896, 2021.

Learn More

Safer Ex­cep­tions for Scala

by Mar­tin Oder­sky, Alek­sander Boruch-Gruszecki, Jonathan Im­manuel Brachthäuser, Ed­ward Lee, and Ondřej Lhoták

In Pro­ceed­ings of the 12th ACM SIG­PLAN In­ter­na­tional Sym­po­sium on Scala, pages 1–11. As­so­ci­a­tion for Com­put­ing Ma­chin­ery, 2021.

Learn More

Rep­re­sent­ing Mon­ads with Ca­pa­bil­i­ties

by Jonathan Brachthäuser, Alek­sander Boruch-Gruszecki, and Mar­tin Oder­sky

Tech­ni­cal re­port. Higher-Or­der Pro­gram­ming with Ef­fects (HOPE), 2021.

Learn More

Ef­fekt: Light­weight Ef­fect Poly­mor­phism for Han­dlers (Tech­ni­cal Re­port)

by Jonathan Im­manuel Brachthäuser, Philipp Schus­ter, and Klaus Os­ter­mann

Tech­ni­cal re­port. Uni­ver­sity of Tübin­gen, Ger­many, 2020.

Learn More