Skip to content

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.

FieldValue
LanguageHaskell
LicenseBSD-3-Clause
Repositorytheseus GitHub repository
DocumentationGitHub
Key AuthorsSebastian Berndt
StatusEarly release (2025); active development
EncodingHigher-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:

  1. Sound semantics: Correct handling of higher-order + algebraic effect combinations
  2. Order-independent interpretations: Handler order should not produce surprising results
  3. 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:

haskell
-- Freer monad with higher-order support
newtype Freer f a

-- f is a higher-order functor describing effect operations

ControlFlow for Resource Safety ​

A key innovation is the ControlFlow class that manages finalizers:

haskell
class ControlFlow f where
  -- Ensure cleanup runs even with continuations
  finalize :: f m a -> (a -> m ()) -> f m a

This 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 ​

FeatureTheseusheftia
SoundnessYes (Consistent semantics)Yes (via Elaboration)
MechanismHigher-order FreerHefty Algebras
ComplexityModerateHigher (Two-phase)
FinalizersBuilt-in (ControlFlow)Via base monad

Sources ​