With or Without You: Programming with Effect Exclusion

Matthew Lutze; Magnus Madsen; Philipp Schuster; Jonathan Immanuel Brachthäuser

doi:10.1145/3607846

With or Without You: Programming with Effect Exclusion

Matthew Lutze, Magnus Madsen, Philipp Schuster, Jonathan Immanuel Brachthäuser

Institut for Datalogi

Publikation: Bidrag til tidsskrift/Konferencebidrag i tidsskrift /Bidrag til avis › Tidsskriftartikel › Forskning › peer review

Abstract

Type and effect systems have been successfully used to statically reason about effects in many different domains, including region-based memory management, exceptions, and algebraic effects and handlers. Such systems' soundness is often stated in terms of the absence of effects. Yet, existing systems only admit indirect reasoning about the absence of effects. This is further complicated by effect polymorphism which allows function signatures to abstract over arbitrary, unknown sets of effects. We present a new type and effect system with effect polymorphism as well as union, intersection, and complement effects. The effect system allows us to express effect exclusion as a new class of effect polymorphic functions: those that permit any effects except those in a specific set. This way, we equip programmers with the means to directly reason about the absence of effects. Our type and effect system builds on the Hindley-Milner type system, supports effect polymorphism, and preserves principal types modulo Boolean equivalence. In addition, a suitable extension of Algorithm W with Boolean unification on the algebra of sets enables complete type and effect inference. We formalize these notions in the λg calculus. We prove the standard progress and preservation theorems as well as a non-standard effect safety theorem: no excluded effect is ever performed. We implement the type and effect system as an extension of the Flix programming language. We conduct a case study of open source projects identifying 59 program fragments that require effect exclusion for correctness. To demonstrate the usefulness of the proposed type and effect system, we recast these program fragments into our extension of Flix.

Originalsprog	Engelsk
Tidsskrift	Proceedings of the ACM on Programming Languages
Vol/bind	7
Nummer	ICFP
Sider (fra-til)	448-475
Antal sider	28
ISSN	2475-1421
DOI	https://doi.org/10.1145/3607846
Status	Udgivet - aug. 2023

Adgang til dokumentet

10.1145/3607846Licens: CC BY

Andre filer og links

Link to publication in Scopus

Citationsformater

@article{afb5a3f0abdc4400a2efa69d5061098f,

title = "With or Without You: Programming with Effect Exclusion",

abstract = "Type and effect systems have been successfully used to statically reason about effects in many different domains, including region-based memory management, exceptions, and algebraic effects and handlers. Such systems' soundness is often stated in terms of the absence of effects. Yet, existing systems only admit indirect reasoning about the absence of effects. This is further complicated by effect polymorphism which allows function signatures to abstract over arbitrary, unknown sets of effects. We present a new type and effect system with effect polymorphism as well as union, intersection, and complement effects. The effect system allows us to express effect exclusion as a new class of effect polymorphic functions: those that permit any effects except those in a specific set. This way, we equip programmers with the means to directly reason about the absence of effects. Our type and effect system builds on the Hindley-Milner type system, supports effect polymorphism, and preserves principal types modulo Boolean equivalence. In addition, a suitable extension of Algorithm W with Boolean unification on the algebra of sets enables complete type and effect inference. We formalize these notions in the λg calculus. We prove the standard progress and preservation theorems as well as a non-standard effect safety theorem: no excluded effect is ever performed. We implement the type and effect system as an extension of the Flix programming language. We conduct a case study of open source projects identifying 59 program fragments that require effect exclusion for correctness. To demonstrate the usefulness of the proposed type and effect system, we recast these program fragments into our extension of Flix.",

keywords = "effect exclusion, polymorphic types and effects, without construct",

author = "Matthew Lutze and Magnus Madsen and Philipp Schuster and Brachth{\"a}user, {Jonathan Immanuel}",

note = "Publisher Copyright: {\textcopyright} 2023 Owner/Author.",

year = "2023",

month = aug,

doi = "10.1145/3607846",

language = "English",

volume = "7",

pages = "448--475",

journal = "Proceedings of the ACM on Programming Languages ",

issn = "2475-1421",

publisher = "Association for Computing Machinery",

number = "ICFP",

}

TY - JOUR

T1 - With or Without You

T2 - Programming with Effect Exclusion

AU - Lutze, Matthew

AU - Madsen, Magnus

AU - Schuster, Philipp

AU - Brachthäuser, Jonathan Immanuel

PY - 2023/8

Y1 - 2023/8

N2 - Type and effect systems have been successfully used to statically reason about effects in many different domains, including region-based memory management, exceptions, and algebraic effects and handlers. Such systems' soundness is often stated in terms of the absence of effects. Yet, existing systems only admit indirect reasoning about the absence of effects. This is further complicated by effect polymorphism which allows function signatures to abstract over arbitrary, unknown sets of effects. We present a new type and effect system with effect polymorphism as well as union, intersection, and complement effects. The effect system allows us to express effect exclusion as a new class of effect polymorphic functions: those that permit any effects except those in a specific set. This way, we equip programmers with the means to directly reason about the absence of effects. Our type and effect system builds on the Hindley-Milner type system, supports effect polymorphism, and preserves principal types modulo Boolean equivalence. In addition, a suitable extension of Algorithm W with Boolean unification on the algebra of sets enables complete type and effect inference. We formalize these notions in the λg calculus. We prove the standard progress and preservation theorems as well as a non-standard effect safety theorem: no excluded effect is ever performed. We implement the type and effect system as an extension of the Flix programming language. We conduct a case study of open source projects identifying 59 program fragments that require effect exclusion for correctness. To demonstrate the usefulness of the proposed type and effect system, we recast these program fragments into our extension of Flix.

AB - Type and effect systems have been successfully used to statically reason about effects in many different domains, including region-based memory management, exceptions, and algebraic effects and handlers. Such systems' soundness is often stated in terms of the absence of effects. Yet, existing systems only admit indirect reasoning about the absence of effects. This is further complicated by effect polymorphism which allows function signatures to abstract over arbitrary, unknown sets of effects. We present a new type and effect system with effect polymorphism as well as union, intersection, and complement effects. The effect system allows us to express effect exclusion as a new class of effect polymorphic functions: those that permit any effects except those in a specific set. This way, we equip programmers with the means to directly reason about the absence of effects. Our type and effect system builds on the Hindley-Milner type system, supports effect polymorphism, and preserves principal types modulo Boolean equivalence. In addition, a suitable extension of Algorithm W with Boolean unification on the algebra of sets enables complete type and effect inference. We formalize these notions in the λg calculus. We prove the standard progress and preservation theorems as well as a non-standard effect safety theorem: no excluded effect is ever performed. We implement the type and effect system as an extension of the Flix programming language. We conduct a case study of open source projects identifying 59 program fragments that require effect exclusion for correctness. To demonstrate the usefulness of the proposed type and effect system, we recast these program fragments into our extension of Flix.

KW - effect exclusion

KW - polymorphic types and effects

KW - without construct

UR - http://www.scopus.com/inward/record.url?scp=85170639932&partnerID=8YFLogxK

U2 - 10.1145/3607846

DO - 10.1145/3607846

M3 - Journal article

AN - SCOPUS:85170639932

SN - 2475-1421

VL - 7

SP - 448

EP - 475

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - ICFP

ER -

With or Without You: Programming with Effect Exclusion

Abstract

Adgang til dokumentet

Andre filer og links

Fingeraftryk

Citationsformater