Theseus (Haskell)
A Haskell library for sound higher-order and algebraic effects using higher-order Freer monads. Announced in early 2025 as an alternative approach to the soundness problem addressed by heftia.
| Field | Value |
|---|---|
| Language | Haskell |
| License | BSD-3-Clause |
| Repository | theseus GitHub repository |
| Documentation | GitHub |
| Key Authors | Sebastian Berndt |
| Status | Early release (2025); active development |
| Encoding | Higher-order Freer monad |
Overview
What It Solves
Theseus addresses the same problem as heftia: the unsound interaction between higher-order effects (like catch, local) and algebraic effects (like NonDet, State) that plagued earlier libraries like polysemy and fused-effects. While heftia uses the elaboration approach from the Hefty Algebras paper, Theseus takes a different approach using higher-order Freer monads.
Design Philosophy
Theseus aims for:
- Sound semantics: Correct handling of higher-order + algebraic effect combinations
- Order-independent interpretations: Handler order should not produce surprising results
- Built-in resource safety: Finalizers and cleanup handled correctly through
ControlFlow
Core Abstractions and Types
Higher-Order Freer Monad
Theseus builds on the Freer monad structure but extends it to handle higher-order computations natively:
-- Freer monad with higher-order support
newtype Freer f a
-- f is a higher-order functor describing effect operationsControlFlow for Resource Safety
A key innovation is the ControlFlow class that manages finalizers:
class ControlFlow f where
-- Ensure cleanup runs even with continuations
finalize :: f m a -> (a -> m ()) -> f m aThis ensures that resources are properly cleaned up even when continuations are resumed multiple times or not at all.
Linear Continuations
To ensure soundness and resource safety, Theseus enforces linear usage of certain suspended functions (continuations), preventing "multi-shot" violations that could leak resources or cause inconsistent state.
Comparison with heftia
| Feature | Theseus | heftia |
|---|---|---|
| Soundness | Yes (Consistent semantics) | Yes (via Elaboration) |
| Mechanism | Higher-order Freer | Hefty Algebras |
| Complexity | Moderate | Higher (Two-phase) |
| Finalizers | Built-in (ControlFlow) | Via base monad |