Qualified Types with Boolean Algebras
summary
Proposes qualifier-backed effects using Boolean algebras by formalizing System F⧼:B (negation, qualifier polymorphism, subqualification) and deriving an effect calculus System F⧼:BE. Implements a practical Flix prototype using boolean unification plus a small trick: three limited forms of subeffecting (abstraction, definition, instantiation) realized as slack in constraints. Empirical results remove 47 unchecked upcasts from Flix’s standard library with <5% compile overhead and reproducible artifacts.
AI-written summary · about
chapters (15)
- 0:00Qualified types with boolean algebras
- 0:23Research motivation
- 1:26Effect systems
- 2:30Flix effect system features
- 3:53Limitations of Flix effects
- 4:58Subeffecting in practice
- 6:03Type qualifiers with lattices
- 7:07Lattices to boolean algebras
- 8:09Formalizing the effect system
- 8:51Limited subeffecting in Flix
- 9:54Slack in unification
- 10:36Empirical results
- 10:56Contributions summary
- 11:38Availability and future work
- 11:59Question and answer session
related talks
16mPolymorphic Types and Effects with Boolean Unification
18mQualifying System F-sub
18mFast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect...
26mThe Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic(…)
19mAssociated Effects: Flexible Abstractions for Effectful Programming
15mSignature restriction for polymorphic algebraic effects
30mEffects,capabilities,and boxes: from scope-based reasoning to type-based reasoning and back
22mAlgebraic Effects Meet Hoare Logic in Cubical Agda