Handling Higher-Order Effectful Operations with Judgemental Monadic Laws
Zhixuan Yang, Nicolas Wu
TL;DR
The paper tackles the challenge of designing languages with higher-order effect handlers by introducing System Fha, a core calculus that treats handlers as carried by raw monads while computation judgments remain governed by monadic laws. It develops a rigorous semantic foundation using realizability and synthetic logical relations (STC) to establish canonicity and parametricity for the recursion-free fragment and extends to general recursion via synthetic domain theory. By leveraging a logical framework (LccLF) to encode System Fha and deploying Artin gluing among models, the authors obtain a consistent equational theory and a path to program extraction from well-typed terms. The work clarifies how to reconcile lawless monadic handling with judgmental monadic laws, enabling precise reasoning about higher-order effects and laying groundwork for future type-and-effect extensions and compiler optimizations.
Abstract
This paper studies the design of programming languages with handlers of higher-order effectful operations -- effectful operations that may take in computations as arguments or return computations as output. We present and analyse a core calculus with higher-kinded impredicative polymorphism, handlers of higher-order effectful operations, and optionally general recursion. The distinctive design choice of this calculus is that handlers are carried by lawless raw monads, while the computation judgements still satisfy the monadic laws judgementally. We present the calculus with a logical framework and give denotational models of the calculus using realizability semantics. We prove closed-term canonicity and parametricity for the recursion-free fragment of the language using synthetic Tait computability and a novel form of the $\top\top$-lifting technique.