This paper introduces a novel type-and-effect calculus, first-class effects, where the computational effect of an expression can be programmatically reflected, passed around as values, and analyzed at run time. A broad range of designs "hard-coded" in existing effect-guided analyses — from thread scheduling, version-consistent software updating, to data zeroing — can be naturally supported through the programming abstractions. The core technical development is a type system with a number of features, including a hybrid type system that integrates static and dynamic effect analyses, a refinement type system to verify application-specific effect management properties, a double-bounded type system that computes both over-approximation of effects and their under-approximation. We introduce and establish a notion of soundness called trace consistency, defined in terms of how the effect and trace correspond. The property sheds foundational insight on "good" first-class effect programming.
Fri 4 Nov Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:10: Typing, in PracticeOOPSLA at Matterhorn 1 Chair(s): Sebastian ErdwegDelft University of Technology, Netherlands | |||
10:30 - 10:55 Talk | A Practical Framework for Type Inference Error Explanation OOPSLA Calvin LoncaricUniversity of Washington, Satish ChandraSamsung Research America, Manu SridharanSamsung Research America, Cole SchlesingerSamsung Research America DOI Pre-print Media Attached | ||
10:55 - 11:20 Talk | Dynamically Diagnosing Type Errors in Unsafe Code OOPSLA Stephen KellUniversity of Cambridge DOI Media Attached | ||
11:20 - 11:45 Talk | First-Class Effect Reflection for Effect-Guided Programming OOPSLA DOI | ||
11:45 - 12:10 Talk | Java and Scala's Type Systems are Unsound: The Existential Crisis of Null Pointers OOPSLA Link to publication DOI Pre-print |