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