cove

English | 简体中文 | Español | 日本語 | Français

cove

Context layer for carrying explicit ambient context across kont suspension boundaries in Go.

Overview

When an external runtime such as a proactor, event loop, or dispatcher steps through kont suspensions one at a time, each suspended operation may need state that lives outside the operation itself: dispatch budget, ring capabilities, protocol phase, buffer-group validity. Without explicit context carriers, that state ends up in ad-hoc side maps or implicit globals that break composition.

cove pairs ambient context with values and suspensions so the context travels across asynchronous stepping boundaries as typed, composable data.

_, sv := cove.StepExprWith(Runtime{Budget: 8}, computation)
for sv.Suspension != nil {
    result := dispatch(sv.Ask(), sv.Op())
    _, sv = sv.ResumeWith(result, func(r Runtime) Runtime {
        r.Budget--
        return r
    })
}

The package is policy-free: it carries and checks context, but never schedules, retries, or dispatches.

Installation

go get code.hybscloud.com/cove

Requires Go 1.26+.

Core Types

Ambient constrains context type parameters (C, D). World gives the same structural constraint the Kripke vocabulary, and Focus constrains value type parameters (A, B).

Contextual Stepping

StepWith and StepExprWith evaluate a kont computation and pair its first suspension with ambient context. Each suspension is affine: consume it exactly once, via Resume, ResumeWith, or Discard.

val, sv := cove.StepExprWith(ctx, expr)
for sv.Suspension != nil {
    op := sv.Op()
    result := handle(op)
    val, sv = sv.Resume(result)
}

ResumeWith evolves the carried context between steps. For example, it can decrement budget, update capabilities, or advance protocol phase:

val, sv = sv.ResumeWith(result, func(r Runtime) Runtime {
    r.Budget--
    return r
})

MapContextSuspension and WithContextSuspension transport or replace the context carried on an already observed suspension, without changing the current suspension frontier:

sv = cove.MapContextSuspension(sv, func(r Runtime) Runtime {
	r.Budget += 4
	return r
})
sv = cove.WithContextSuspension(sv, Runtime{Budget: 16})

Once the computation completes, sv.Suspension becomes nil, but sv.Ask() still returns the carried context.

cove forwards kont's stepping classifier, so Step, StepExpr, StepWith, StepExprWith, Resume, and ResumeWith inherit kont's nil-completion convention: completion is observed by a nil suspension result, and on completion the returned value is the zero value of A. Suspended steps may also return the zero value of A, so callers must use the suspension result—not A itself—to distinguish completion from suspension. Computations whose result type is a nilable type (pointer, interface, map, slice, channel, or function) therefore cannot use nil as a meaningful completed value; wrap nil in an explicit sum or witness type when that distinction matters. Carrier context is unaffected.

ObserveSuspension attaches ambient context to an existing kont.Suspension without performing any requirement check. CheckSuspension and CheckSuspensionExpr provide gated forms:

sv, ok := cove.CheckSuspension(runtime, susp, func(r Runtime) bool {
    return r.Budget > 0
})
if !ok {
    susp.Discard()
    return
}
result := dispatch(sv.Ask(), sv.Op())
val, sv = sv.Resume(result)

exprReq := cove.ExprAtom(func(r Runtime) bool { return r.Budget > 0 })
sv, ok := cove.CheckSuspensionExpr(runtime, susp, exprReq)
if !ok {
    susp.Discard()
    return
}
result := dispatch(sv.Ask(), sv.Op())
val, sv = sv.Resume(result)

Step and StepExpr re-export kont's evaluators without context binding.

Step-Indexed Kripke Evidence

cove can make the Kripke reading explicit without turning context into scheduler policy. A Preorder[C] defines world extension and exposes Extends, ReflexiveAt, and TransitiveAt checks; Transition[C], CheckTransition, CheckForcingTransition, and CheckInvariantTransition check concrete world edges; Forcing pairs a requirement with that preorder; and Relation indexes semantic validity by world, finite StepIndex, and value.

Use DiscreteWorlds for equality-only worlds and TotalWorlds for a preorder that relates every world pair. ForceExpr mirrors Force for ReqExpr; CheckRelation, WeakenIndexedView, and WeakenIndexedSuspension make relation checks and step-credit weakening explicit.

type RuntimeWorld struct {
	Epoch uint64
}

leq := func(w, next RuntimeWorld) bool {
	return w.Epoch <= next.Epoch
}
_ = cove.Preorder[RuntimeWorld](leq).ReflexiveAt(RuntimeWorld{Epoch: 1})
_ = cove.Preorder[RuntimeWorld](leq).TransitiveAt(RuntimeWorld{Epoch: 1}, RuntimeWorld{Epoch: 2}, RuntimeWorld{Epoch: 3})

canObserve := cove.Force(leq, func(w RuntimeWorld) bool {
	return w.Epoch > 0
})
_ = canObserve.MonotoneAt(RuntimeWorld{Epoch: 1}, RuntimeWorld{Epoch: 2})

rel := cove.Relate(leq, func(w RuntimeWorld, n cove.StepIndex, value int) bool {
	return uint64(n) <= w.Epoch && value >= 0
})
later := cove.Later(rel)
_ = later.Holds(RuntimeWorld{Epoch: 8}, 3, 4)

For operational prefixes, StepWithIndex and StepExprWithIndex pair a SuspensionView with explicit fuel. Each indexed Resume consumes one unit of step credit, making finite observations visibly decrease. Use ResumeTo when the successor context must be checked as a Kripke world extension; CheckCompletedRelation checks the final relation at a completed indexed frontier:

_, sv := cove.StepExprWithIndex(RuntimeWorld{Epoch: 2}, 2, expr)
var val int
for sv.Extract() != nil {
	result := dispatch(sv.Ask(), sv.Op())
	next := sv.Ask()
	next.Epoch++
	val, sv = sv.ResumeTo(leq, result, next)
}
_ = cove.CheckCompletedRelation(sv, val, rel)

Commands

Cmd[C, A, B] is the coKleisli arrow View[C, A] -> B. Run applies a command to a concrete View; ExtractCmd is the identity command; LiftCmd lifts a focus-only map into the contextual world; Compose composes commands through Extend, satisfying Compose(g, f)(v) == g(Extend(v, f)).

cmd := cove.Compose(
	func(v cove.View[Runtime, int]) string {
		return fmt.Sprintf("budget=%d value=%d", v.Ask().Budget, v.Extract())
	},
	cove.LiftCmd(func(n int) int { return n + 1 }),
)
out := cove.Run(cove.Observe(Runtime{Budget: 8}, 41), cmd)
_ = out // "budget=8 value=42"

Requirements

Requirements are predicates over the ambient context, available in both closure and data form. Both forms support All, Any, and Not, with True and False as the neutral elements of conjunction and disjunction.

Closure form (Req): direct and concise.

req := cove.All(
    cove.Req[Runtime](func(r Runtime) bool { return r.Budget > 0 }),
    cove.Req[Runtime](func(r Runtime) bool { return r.CanDispatch }),
)
ok := cove.Need(runtime, req)

Data form (ReqExpr): composable Boolean structure that avoids closure allocation during composition.

expr := cove.ExprAll(
    cove.ExprAtom(func(r Runtime) bool { return r.Budget > 0 }),
    cove.ExprAtom(func(r Runtime) bool { return r.CanDispatch }),
)
ok := cove.NeedExpr(runtime, expr)

Combinators: All/ExprAll (conjunction ∧), Any/ExprAny (disjunction ∨), Not/ExprNot (negation ¬), True/ExprTrue (⊤), False/ExprFalse (⊥).

Pullback and ExprPullback transport requirements contravariantly along a context projection. Given f: C → D, Pullback(req, f) maps Req[D] to Req[C]. ExprPullback preserves the Boolean structure and distributes over ExprNot, ExprAll, and ExprAny.

Choosing Req vs ReqExpr

Use Req for ad-hoc, one-off predicates. Use ReqExpr when composing many requirements, or when closure allocation at construction time matters.

Bridge helpers keep the two forms aligned: ReifyReq is a lossy quotation helper that wraps a closure-form requirement as an ExprAtom, so ReifyReq(nil) is invalid and panics when evaluated; ReflectReq evaluates an Expr-form requirement through a closure rather than recovering its original structure.

Gated Values

Guard pairs a value with a requirement; IntoView yields a View only when the ambient context satisfies that requirement:

checked := cove.Guard(canDispatch, payload)
if view, ok := checked.IntoView(runtime); ok {
    _ = view.Extract()
}

GuardRule adds diagnostics via named rules and Report:

rule := cove.Require("budget", func(r Runtime) bool { return r.Budget > 0 })
guarded := cove.GuardRule(rule, payload)
if view, report := guarded.IntoView(runtime); report.OK() {
    _ = view.Extract()
}

CheckRules and CheckRulesExpr evaluate several rules in order, stopping at the first failure:

report := cove.CheckRules(runtime, budgetRule, permRule)
if !report.OK() {
    // report.Failed names the first rule that did not hold
}

The Expr-form diagnostic path has the same shape through CheckRulesExpr and GuardRuleExpr:

type Runtime struct{ Budget int }

runtime := Runtime{Budget: 1}
payload := "packet"
exprRule := cove.RequireExpr("budget", cove.ExprAtom(func(r Runtime) bool {
    return r.Budget > 0
}))
report := cove.CheckRulesExpr(runtime, exprRule)
if !report.OK() {
    return
}
guardedExpr := cove.GuardRuleExpr(exprRule, payload)
if view, report := guardedExpr.IntoView(runtime); report.OK() {
    _ = view.Extract()
}

Expr-form equivalents: GuardExpr, GuardRuleExpr, CheckedExpr, GuardedExpr. Map and pullback helpers: MapChecked, MapGuarded, PullbackChecked, PullbackGuarded (and their Expr variants).

View Operations

View[C, A] is a comonad over the category of Go types. The carrier is the product C × A; Extract (ε) projects the value; Duplicate (δ) embeds the observation as the focused value:

v := cove.Observe(ctx, value)
v.Ask()       // ambient context  (π₁)
v.Extract()   // value in focus   (ε = π₂)

Transformations: Map (functorial lift on A), MapContext (functorial lift on C), Replace (substitute the value), WithContext (substitute the context).

Duplicate and Extend satisfy the comonad laws:

// Counit law:  ε ∘ δ = id
cove.Duplicate(v).Extract() == v

// Extension identity:  extend(ε) = id
cove.Extend(v, func(w cove.View[C, A]) A { return w.Extract() }) == v

// Associativity:  extend(f) ∘ extend(g) = extend(f ∘ extend(g))

Extend is the contextual extension operator: given f: W(C, A) → B, it lifts f to W(C, A) → W(C, B) while preserving the ambient context. The induced command composition with g: W(C, B) → D is g ∘ Extend(f).

Ecosystem Position

Formal Structure

View[C, A] is an environment comonad (Uustalu & Vene 2008) with carrier C × A, counit ε = π₂ (Extract), and comultiplication δ(c, a) = (c, (c, a)) (Duplicate). Extend implements contextual extension (coKleisli extension in the categorical literature).

Req[C] and ReqExpr[C] are objects in the Boolean algebra of predicates over C. Pullback implements the contravariant functor f* induced by a morphism f: C → D, mapping predicates on D to predicates on C. ExprPullback preserves the Boolean algebra structure: f*(p ∧ q) = f*(p) ∧ f*(q), f*(¬p) = ¬f*(p).

kont models algebraic effects (free monad, handlers, fold); cove models coeffects (comonad, requirements, unfold). The two are categorical duals at the suspension boundary: kont describes what the computation does to the world, whereas cove states what the computation needs from the world.

Read through the lens of modal effects, the carrier shape can be read as naming what happens to ambient context: kont ( C → D) replaces it, cove (W(C, A) → B) handles it relatively, and pure pass-through preserves it. Effect structure rides on the carrier, not on a function colour, which keeps cove policy-free.

ReqExpr defunctionalizes the Boolean algebra into a tagged union, namely the initial algebra of the Boolean signature functor, so that the structure of a requirement is inspectable data rather than an opaque closure (Reynolds 1972).

Practical Recipes

A complete contextual computation typically proceeds in three stages: declare requirements, gate values against them, then observe the result under a concrete context.

// 1. Declare a requirement on the ambient context.
type Caps struct{ CanSubmit, HasToken bool }
req := cove.All(
	func(c Caps) bool { return c.CanSubmit },
	func(c Caps) bool { return c.HasToken },
)

// 2. Gate a value on that requirement. This produces a Checked[Caps, T].
checked := cove.Guard(req, payload)

// 3. Reify into an Expr to step under different ambient contexts.
expr := cove.ReifyReq(req)
ok := cove.NeedExpr(Caps{CanSubmit: true, HasToken: true}, expr)
_ = checked
_ = ok

Pullback lets a caller adapt a requirement defined over one context so that it works over another (Pullback(req, f) for f: D → C); MapChecked and MapGuarded transport gated values through value-level transformations without re-checking the predicate. The combination All + Pullback + Guard is how downstream packages build typed capability checks without coupling to a single context type.

References

• John C. Reynolds. 1972. Definitional Interpreters for Higher-Order Programming Languages. In Proc. ACM Annual Conference (ACM '72). 717–740. https://doi.org/10.1145/800194.805852
• Tarmo Uustalu and Varmo Vene. 2008. Comonadic Notions of Computation. Electronic Notes in Theoretical Computer Science 203, 5 (June 2008), 263–284. https://doi.org/10.1016/j.entcs.2008.05.029
• Tomas Petricek, Dominic Orchard, and Alan Mycroft. 2014. Coeffects: A Calculus of Context-Dependent Computation. In Proc. 19th ACM SIGPLAN International Conference on Functional Programming (ICFP '14). 123–135. https://tomasp.net/academic/papers/structural/coeffects-icfp.pdf
• Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, and Tarmo Uustalu. 2016. Combining Effects and Coeffects via Grading. In Proc. 21st ACM SIGPLAN International Conference on Functional Programming (ICFP '16). 476–489. https://doi.org/10.1145/2951913.2951939
• Jonathan Immanuel Brachthäuser, Philipp Schuster, and Klaus Ostermann. 2020. Effects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism. Proc. ACM on Programming Languages 4, OOPSLA (Nov. 2020), Article 126, 30 pages. https://se.cs.uni-tuebingen.de/publications/brachthaeuser20effekt.pdf
• Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal. 2021. Multimodal Dependent Type Theory. Logical Methods in Computer Science 17, 3 (2021), Paper 11, 67 pages. https://doi.org/10.46298/lmcs-17(3:11)2021
• Wenhao Tang, Leo White, Stephen Dolan, Daniel Hillerström, Sam Lindley, and Anton Lorenzen. 2025. Modal Effect Types. Proc. ACM Program. Lang. 9, OOPSLA1 (Apr. 2025), Article 120, 1130–1157. https://arxiv.org/abs/2407.11816
• Wenhao Tang and Sam Lindley. 2026. Rows and Capabilities as Modal Effects. Proc. ACM Program. Lang. 10, POPL (Jan. 2026), 923–950. https://arxiv.org/abs/2507.10301

Platform Support

cove is a pure Go package in this module. It has no platform-specific files or build tags; the module requirement is Go 1.26+.

License

MIT License. See LICENSE for details.

©2026 Hayabusa Cloud Co., Ltd.