When Types Intersect and Effects Get Handled
2026-06-08 • Logic in Computer Science
Logic in Computer ScienceProgramming Languages
AI summaryⓘ
The authors present a new type system for a version of the lambda calculus that includes algebraic effects and handlers, which help manage side effects in computations. Their system has important properties like subject reduction and expansion, meaning it behaves well when terms change during evaluation. This type system can identify which programs will finish running and allows checking program behavior through type inference. It is the first of its kind to combine these features with handlers and also introduces a simpler type system that is sound and has decidable properties unlike some earlier approaches.
lambda calculusalgebraic effectshandlersintersection type systemsubject reductionsubject expansionterminationtype inferencetype soundnessdecidability
Authors
Ugo Dal Lago, Taro Sekiyama, Stefano Catozi
Abstract
We introduce a novel intersection type system for a $λ$-calculus with algebraic effects and handlers. The system, inherently behavioral in nature, enjoys the classical properties of intersection type systems, in particular subject reduction and expansion. It thus characterizes the set of terms whose evaluation process terminates and, at the same time, allows reducing the reachability problem to type inference. This new system, the first with these features for a calculus with handlers, induces a system of simple types which, although not guaranteeing termination, is type sound and admits a decidable HOMC problem, unlike similar type systems like Dal Lago and Ghyselen's HEPCF.