Source-linked AI summary
Cambria: Resource Abstraction for Parametrized Algebraic Effects and Handlers
Jack Liell-Cock, Sam Staton
TL;DR
Cambria addresses how algebraic effects can support dynamically allocated resources without exposing their representations to clients. It combines parametrized handlers with a step-indexed logical relation, type inference results, and an implementation, establishing abstraction guarantees alongside type safety and expressive concurrent examples. Its limitations include non-equivalence between handlers with different scheduling strategies and unavoidable retention of unused references in one handler.
Problem
Existing effect interfaces may expose resource types that clients should use but not inspect, motivating abstraction for dynamically allocated resources such as locations and thread IDs.
Method
Cambria extends algebraic effects with parametrized handlers, decomposes them into classic handlers and existential types, and proves properties using a step-indexed logical relation.
Results
Cambria provides parametricity, type safety, complete practical inference with annotations only on parameter-mentioned operation arities, and expressive examples including coordinated concurrent threads.
Takeaways & Limitations
Clients cannot depend on concrete resource representations, while parametrized effects express dynamic allocation and shared thread coordination beyond standard independent instances.
Takeaways & Limitations
Handlers with different scheduling strategies are not observationally equivalent, and the function-based handler can retain unused references for the handle's entire body.
Abstract
from arXiv · showhide
The algebraic effects and handlers paradigm separates the concerns of the interface and implementation of computational effects in programming languages. We present Cambria, a language that extends this framework to the parametrized setting. Effect signatures may use abstract parameter types that are instantiated by the handler along with the operation implementations. Parameters abstract over resources, such as memory locations or thread IDs, permitting algebraic effects to encode dynamic allocation. They are first-class in the type system but erased at runtime, requiring no coercions or type-directed reduction. We prove parametricity via a step-indexed logical relation, formalizing the abstraction guarantee provided by parametrized handlers. We also establish type safety and classify the annotations needed for completeness of the type inference algorithm. We demonstrate Cambria's practicality with a working implementation and provide examples including local state, Pólya's urn, and concurrent thread management. The last is a parametrized effect whose abstract thread IDs are shared between concurrent computations, going beyond standard instances. Cambria is the first calculus with user-defined resource-allocating effects that guarantees, via parametricity, that client code cannot depend on how a handler represents its resources.
1 Introduction
Cambria extends algebraic effects and handlers with abstract parameters for dynamically allocated resources, while preserving representation independence and practical typing. Its theory establishes parametricity, type safety, annotation completeness, and expressive implementations including dynamically coordinated concurrency.
- Resource abstraction: Abstract resource representations prevent clients from inspecting, forging, or performing arithmetic on resources outside the provided effect interface.Local state illustrates how locations can remain abstract while still supporting allocation, reading, and writing.
- Language design: Cambria extends algebraic effects and handlers with parameters that handlers instantiate as resource types while interpreting operations.This supports dynamically allocated resources such as memory locations and enables idiomatic parametrized effects.
- Expressiveness and implementation: Cambria expresses dynamically threaded concurrency in which abstract thread IDs are shared across processes, and provides runnable examples plus a Rocq mechanization.The implementation includes handlers for concurrent thread management and other examples, while all novel results are mechanized.
- Metatheory: Parametrized handlers decompose into classic handlers and existential types, keeping the surface language ergonomic while reducing the metatheory to modular components.The decomposition provides the basis for representation independence for effects with dynamic resources.
- Parametricity: A step-indexed logical relation establishes parametricity for Cambria's type variables and parameters.The result formalizes that well-typed client code cannot depend on how handlers represent abstract resources.
- Type inference: Cambria's annotation completeness result requires annotations only for operations whose arities mention abstract parameter types; other types are inferred.The remaining inference uses ordinary Algorithm W with parameters treated as constants.
2 Overview of the Cambria Language
Cambria uses parametrized handlers to abstract resource representations while supporting dynamic allocation, polymorphism, probabilistic effects, and shared concurrency parameters. Its examples show that one effect interface can support multiple implementations and that clients remain unable to inspect abstract representations.
- Core language: Parametrized handlers instantiate abstract parameter types alongside operation implementations, while effect declarations themselves allocate nothing.Generative behavior is supplied by handlers such as !ref.
- Core language: Cambria’s handle construct substitutes abstract parameter types before applying a classic handler, recovering ordinary handling when no substitution is present.Multiple substitutions are comma-separated, and the clause may be omitted for classic handlers.
- Local state and polymorphism: Parametrized handlers support statically unbounded effect-instance creation, including allocating a reference for each integer in a runtime list through polymorphic map.The same polymorphic function accesses each parameter-typed reference afterward.
- Local state and polymorphism: Parametricity prevents clients from distinguishing handler representations, including representations of locations used under let-polymorphism.The dynamic creation idiom is presented as enjoying a parametricity guarantee.
- Probabilistic urns: Two Pólya’s urn handlers induce the same returned-pair distribution, with both yielding P(both red) = 1/3 despite different implementations.The state-based calculation is 1/2·2/3, while the direct handler computes E_p∼Uniform[0,1] [p^2].
- Dynamically threaded concurrency: Cambria handles shared thread parameters in multiple ways, including parent- or child-biased execution and DAG generation of action dependencies.One implementation executes actions in order 2, 4, 1, 3, while remaining consistent with the dependency diagram.
3 The Calculus
Cambria’s calculus adds parameter variables and parameter substitutions to algebraic handlers, while preserving a standard core with recursion and let-polymorphism. Its typing and operational semantics establish type safety and erase parameter substitutions during reduction.
- Types and Syntax: Cambria extends a handler calculus with parameter variables, parameter substitutions, and parametrized handling, alongside recursion and let-polymorphism.The implementation adds standard data types and surface conveniences that map directly onto calculus terms.
- Types and Syntax: The language uses type, parameter, and term-variable contexts; parameter variables represent abstract types introduced by effect interfaces.Universal quantification in operation arities is disallowed, which permits the annotation-completeness result for type inference.
- Typing Rules: A parameter substitution in a handle term bridges abstract types in the computation body to concrete representations supplied by the handler.The ParHandle rule applies the substitution before matching the handler input type, while substituted parameters remain confined to the handled body.
- Typing Rules: Handled operations may be forwarded, and operation continuations are ordinary variables, permitting multi-shot resumption.Forwarding is allowed for operations outside the handled subset, while captured continuations may be resumed any number of times.
- Operational Semantics and Type Safety: Parameter substitutions are erased from reduction: no rule inspects them, so runtime reduction needs no dynamic dispatch, coercions, or type-directed reduction.Erasure preserves reducibility and corresponds to discarding substitutions in parametrized-handle reductions.
- Operational Semantics and Type Safety: Well-typed computations satisfy progress and preservation: they become values, remain control-stuck only on operations in their effect signature, or can reduce.The preservation statement is parameter-erased, requiring a weakened form that still yields type safety.
4 Parametricity
Cambria establishes parametricity for parametrized handlers by elaborating them into classic handlers and existential types, then proving the resulting abstraction properties with a step-indexed logical relation. The results connect this guarantee to contextual equivalence, representation independence, equational reasoning, and several explicit scope boundaries.
- Core decomposition: Parametrized handlers decompose into classic handlers and existential types, keeping the surface language ergonomic while reducing the metatheory to standard components.The elaboration translates parametrized handles into existential packing and classic handling, with existential elimination contributing no runtime content.
- Fundamental theorem: The step-indexed logical relation proves that every well-typed term is related to itself uniformly across admissible interpretations of type variables and parameters.The relation is defined over the core language and is transferred back to Cambria through a faithful elaboration.
- Abstraction guarantee: Parametricity prevents clients from inspecting or using abstract parameters outside the effect interfaces, providing representation independence for dynamically allocated resources.This is the formal abstraction guarantee for parameters such as locations or thread IDs.
- Metatheoretic connection: Type preservation and operational correspondence connect Cambria terms with their elaborations, while adequacy connects the logical relation to contextual equivalence.Contextual equivalence is characterized by the inability of any context to distinguish program behavior.
- Applications: Parametricity supports observational equivalence for handlers related on their abstract parameters, but handlers with different thread-scheduling strategies need not be representation independent.Handlers using different representations of the same scheduling strategy can remain observationally equivalent because clients cannot inspect thread IDs.
- Limitations and scope: The framework has explicit boundaries: probabilistic equivalence requires a probability-monad extension, recursive types and universal operation arities remain future work, and naive liveness detection conflicts with parametricity.Allocating an unused reference is observationally undetectable, but the function-based handler retains it for the entire handled body, producing a memory leak.
5 Type Inference
Cambria’s type inference extends Hindley–Milner inference with rigid parameters while retaining soundness, decidability, and principal solutions. Completeness requires annotations only for operations whose arities introduce parameters.
- Inference machinery: Cambria’s inference differs from effect-handler Hindley–Milner inference only in the parameterized handle rule, with parameters treated as rigid constants.Parameters unify only with themselves; the remaining inference uses ordinary Algorithm W, value-type unification, and row unification.
- Inference machinery: The inference algorithm is syntax-directed and terminating, with principal solutions for value types and effect rows.This makes inference decidable while preserving principality.
- Soundness and completeness: Theorem 5.1 establishes soundness: every type inferred by the algorithm is derivable in Cambria’s declarative system.Therefore, accepted programs receive the type-safety and parametricity guarantees of the declarative system.
- Annotation burden: The completeness result assumes monomorphic operation arities; universally quantified arities would require additional annotations and remain future work.The full annotated and relevantly annotated completeness lemmas build on this restriction.
- Soundness and completeness: Theorem 5.5 establishes completeness for relevantly annotated terms, where annotations list only operations mentioning introduced parameters.Return types and parameter-free operations need not be annotated.
- Annotation burden: The local-state example needs annotations for only three parameter-relevant arities, and term-level flow can make some such annotations unnecessary.Annotating only !set can suffice to infer the arity of !ref in the illustrated program.
6 Related Work
Cambria realizes parametrized algebraic theories within an effect-handler calculus, addressing dynamic resource allocation and representation abstraction. It also gives abstract thread IDs for concurrent effects while deriving abstraction guarantees through logical relations.
- Parametrized algebraic theories: Cambria implements parametrized algebraic theories in algebraic effects and handlers, where operations can bind and use abstract parameters for resource allocation.The approach complements prior theoretical work by providing a language realization.
- Effect instances and named handlers: Unlike approaches using concrete instances, Cambria separates dispatch from instances and exposes resources only as abstract parameters instantiated by the handler.This provides representation independence for user-defined resources without type-directed reduction.
- Parametricity and logical relations: Cambria’s parametricity comes from interpreting parameters as existential types and is established with a step-indexed logical relation adapted to handlers.The relation supplies the calculus’s abstraction guarantees.
- Reasoning about dynamic allocation: Cambria obtains analogous abstraction guarantees for local state and fresh-name effects without possible-world indices.The relational interpretation of parameter types plays the role that worlds play for a primitive mutable heap.
- Concurrent effects: For concurrent effects, abstract parameter variables represent thread IDs shared across processes, allowing one handler to interpret dynamically coordinated threads.This differs from prior dynamic-thread accounts using concrete thread IDs.
7 Conclusion
Cambria extends algebraic effects and handlers with type abstraction for resource-allocating effects, combining parametricity with an ergonomic implementation strategy. Its examples and implementation demonstrate practical expressiveness, while garbage collection and polymorphic extensions remain outside the supported scope.
- Conclusion: Cambria makes parameter variables first-class in the type system but erases them at runtime, while step-indexed parametricity prevents clients from inspecting concrete resource representations.Parametrized handlers decompose into ordinary handlers and existential types.
- Conclusion: The implementation demonstrates local state, Pólya’s urn, and concurrent thread management, with type safety, backwards compatibility, practical inference, and Rocq mechanization.Only effect arities mentioning parameters need annotations in the demonstrated inference approach.
- Future work: Future work includes substructural parameters, built-in references, region-based memory management, probabilistic semantics, and denotational semantics.These directions also include addressing the reachability limitation and refining the type system.
- Future work: Reachability-based garbage collection for parametric local state remains outside the paper’s scope, motivating alternatives such as substructural typing and regions.The paper argues that client-transparent liveness analysis would violate parametricity.