Higher-order Programming with Effects and Handlers — with First-Class Functions
Reasoning about the use of external resources is an important aspect of many practical applications. Examples range from memory management, controlling access to privileged resources like file handles or sockets, to analysing the potential presence or absence of side effects. Effect systems enable tracking such information in types, but at the cost of complicating signatures of common functions. Capabilities coupled with escape analysis offer safety and natural signatures, but are often overly restrictive. We present a calculus that builds on and generalises ideas from type-based escape analysis and comonadic type systems, and demonstrates that capabilities and effects can be reconciled harmoniously. By assuming that all functions are second class, we can admit natural signatures for many common programs. By introducing a notion of boxed values, we can lift the restrictions of second-class values at the cost of needing to track degree-of-impurity information in types.
Sun 22 AugDisplayed time zone: Seoul change
16:00 - 17:30 | |||
16:00 30mTalk | Representing Monads with Capabilities HOPE | ||
16:30 30mTalk | Higher-order Programming with Effects and Handlers — with First-Class Functions HOPE Jonathan Immanuel Brachthäuser EPFL, Philipp Schuster University of Tübingen, Edward Lee University of Waterloo, Aleksander Boruch-Gruszecki EPFL | ||
17:00 30mTalk | Computational and Contextual Program Differences: Reasoning About Non-equivalent Effectful Programs in an Higher-Order Scenario HOPE Ugo Dal Lago University of Bologna, Italy / Inria, France, Francesco Gavazzo University of Bologna & INRIA Sophia Antipolis |