Handling Higher-Order Effectful Operations with Judgemental Monadic Laws

TL;DR

This paper introduces a core calculus for programming languages with higher-order effectful operations, using lawless monads and monadic laws, with formal semantics and proofs of key properties.

Contribution

It presents a novel calculus that combines lawless monads with monadic laws for higher-order effectful operations, along with logical framework and denotational models.

Findings

Proves closed-term canonicity for the recursion-free fragment.

Establishes parametricity using synthetic Tait computability.

Provides realizability semantics for the calculus.

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.