co

Computations with higher-order effects, and their handlers. The idea is from Yang and Wu’s “Handling Higher-Order Effectful Operations with Judgemental Monadic Laws” (POPL 2026).

A computation is a function: given any handler, and what to do next in that handler’s monad, it runs (the paper’s realizability model). So val and bind keep the monad laws by beta and eta alone, and a handler’s own monad need keep none of them.

When pure work runs: by value, an argument is computed where the computation is built (pure (f x) computes f x there), and a step after a bind is taken by the handler as it handles — only what comes after an operation is left to the handler’s monad, to run when that runs. So a handler into Co e (through) that puts a part elsewhere (another process, a later turn) finds its pure work done: later leaves it to the handler’s monad.

RawFunctor

theory RawFunctor where
  f : Type -> Type
  fmap : {a b : Type} -> (a -> b) -> f a -> f b

A functor, no laws asked: a type function and its action on functions.

HFunctor

theory HFunctor where
  f : (Type -> Type) -> Type -> Type
  hfmap : (m : RawFunctor) -> {a b : Type} -> (a -> b) -> f m.f a -> f m.f b
  hmap : (m : RawFunctor)
       -> (n : RawFunctor)
       -> ({x : Type} -> m.f x -> n.f x)
       -> {a : Type}
       -> f m.f a
       -> f n.f a

The signature of an effect: a higher-order functor. f takes a functor to one (f m.f is one when m is), hfmap is that functor’s action on functions, and hmap its action on the transformations between functors.

Handler

theory Handler (h : HFunctor) where
  M : Type -> Type
  ret : {a : Type} -> a -> M a
  bind : {a b : Type} -> M a -> (a -> M b) -> M b
  malg : {a : Type} -> h.f M a -> M a

A handler of the effect h: a raw monad (no laws asked) and what each operation does in it (its algebra, malg).

Co

type Co (h : HFunctor) a =
  (hd : Handler h) -> (r : Type) -> (a -> hd.M r) -> hd.M r

A computation with the effect h: for any [Handler], a continuation into its monad. Its [bind] satisfies the monad laws by beta and eta.

val

val : {h : HFunctor} -> {a : Type} -> a -> Co h a

bind

bind : {h : HFunctor} -> {a b : Type} -> Co h a -> (a -> Co h b) -> Co h b

pure

pure : {h : HFunctor} -> {a : Type} -> a -> Co h a

instanceMonadCo

instance instanceMonadCo : {h : HFunctor} -> Monad (Co h)

A computation as a [Monad]: [pure] and [bind], what do takes by name.

later

later : {h : HFunctor} -> {a : Type} -> (Unit -> a) -> Co h a

f (), and what comes after it, computed when the handler’s monad runs them, not where the computation is built or handled: through a handler into Co e ([through]), when that Co e runs. (pure (f x) computes f x where it is built; bind c (\x -> pure (f x)), where it is handled.)

coFunctor

coFunctor : (h : HFunctor) -> RawFunctor

A computation as a functor: its answer mapped.

handlerFunctor

handlerFunctor : {h : HFunctor} -> Handler h -> RawFunctor

A handler’s monad as a functor.

handle

handle : {h : HFunctor} -> {a : Type} -> (hd : Handler h) -> Co h a -> hd.M a

Run a computation with a [Handler].

op

op : {h : HFunctor} -> {a b : Type} -> h.f (Co h) a -> (a -> Co h b) -> Co h b

Perform an operation: its computations are handled first, by the same handler; then what comes after it.

SumF

data SumF (f : (Type -> Type) -> Type -> Type) (g : (Type -> Type) -> Type -> Type) (m : Type -> Type) a
  = InL (f m a)
  | InR (g m a)

Two effects as one: each operation is one or the other’s.

<+>

(<+>) : HFunctor -> HFunctor -> HFunctor

<:

(<:) : HFunctor -> HFunctor -> Type

h <: e is the evidence that the effect h is in e: its operations, put among e’s. The effects are given, not inferred — nothing of an operation says what the rest of its sum is, and which world an operation belongs to is nowhere in its type: the evidence is the program saying it. Evidence composes as functions do, \p -> outer (inner p), and may route a whole sum into another shape, a case on its tags.

here

here : (h : HFunctor) -> h <: h

An effect in itself: the evidence where nothing is summed.

inl

inl : (h : HFunctor) -> (k : HFunctor) -> h <: (h <+> k)

An operation of one effect, put left in a sum: the evidence at its smallest (lift, and parallel.hf’s parallelIn, take one).

inr

inr : (h : HFunctor) -> (k : HFunctor) -> k <: (h <+> k)

… and right.

lift

lift : {h : HFunctor}
     -> {k : HFunctor}
     -> {a : Type}
     -> {{inj : h <: k}}
     -> Co h a
     -> Co k a

A computation of a smaller effect, in a bigger one (by the evidence that it is in there): whoever handles the bigger effect handles the smaller through it — one monad for all of a sum, the operations told apart by the evidence.

through

through : (h : HFunctor)
        -> (e : HFunctor)
        -> ({a : Type} -> h.f (Co e) a -> Co e a)
        -> Handler (h <+> e)

A handler of h <+> e that says only what h does — in Co e, the computations of the rest: an operation of e is an op again. handle (through h e alg) c peels one world off c and keeps the others as they are, to be handled by whoever handles e. It takes c’s pure steps as it handles: only what comes after an operation of e, or after [later], waits for the Co e to run.

extend

extend : (k : HFunctor)
       -> (h : HFunctor)
       -> (hd : Handler h)
       -> ({a : Type} -> k.f hd.M a -> hd.M a)
       -> Handler (k <+> h)

One more world on the handler there is: never two monads composed — the sum’s one monad is hd’s, and k brings only its algebra.

within

within : (h : HFunctor)
       -> (e : HFunctor)
       -> ({a : Type} -> (hd : Handler e) -> h.f hd.M a -> hd.M a)
       -> {a : Type}
       -> Co (h <+> e) a
       -> Co e a

c with what h does said within the handler of the rest: alg is given that handler, hd, and answers an operation of h in hd’s own monad, at once — hd.ret an answer, or hd.malg the operation (or another) handed on, with its own continuation. So no Co e stands between h and e, as it does in through, where an operation of h is a computation of e to be run outside: a query passed on through many such layers builds nothing at each. The answer is hd’s to bind, not a Co e’s: the same as through’s where hd’s ret and bind keep the monad laws.

Binder

theory Binder c where
  Contents : HFunctor -> Type -> Type
  World : HFunctor -> HFunctor = \w -> w
  Result : Type -> Type

What a with’s names are, by what they are bound to, a c: one value, or a pair of the first and the rest’s (with a := M binds M; with a := M and b := N under it, (M, N); three, (M, (N, O))): their type in its body, given the world w of the block around and a region s of its own (a With s a, which cannot leave the body, as scoped’s), the world its body runs in, made from w (that world itself, unless said: \w -> stdio <+> w, a body whose output is the holder’s to handle), and what the with comes to, its body having come to an r.

Holder

theory Holder (e : HFunctor) c (contents : Type -> Type) (world : HFunctor -> HFunctor) (result : Type -> Type) where
  held : {r : Type}
       -> c
       -> List Bool
       -> ({s : Type} -> contents s -> Co (world e) (r, contents s))
       -> Co e (result r)

How a with of a c is held in the world e, its names of the type contents (a Binder c’s, given e), its body run in world e and what it comes to result (a Binder c’s): held c written body takes what the c holds, all at once, runs body with it, and is done with it — body gives back its value beside what the names are at its end, and written says, a Bool a name in the names’ order, which of them its statements set, for the holder to write back those alone (or none: a file, an event). Where, when and how often body runs is the holder’s, and so is what it does in world e that e does not: its handler.

holding

holding : {e : HFunctor}
        -> {c r : Type}
        -> c
        -> {{b : Binder c}}
        -> {{h : Holder e c (b.Contents e) b.World b.Result}}
        -> List Bool
        -> ({s : Type} -> b.Contents e s -> Co (b.World e) (r, b.Contents e s))
        -> Co e (b.Result r)

with x := M ... do ss: what the bindings are bound to, held by its holder in the world e — a do block’s with of bindings is this, its body ss, a block of its own in the world the binder says, the names its variables. (The evidence the body’s statements ask for is found in that world, through e’s in scope where it is there.)

Waiter

theory Waiter (e : HFunctor) c (contents : Type -> Type) (world : HFunctor -> HFunctor) (result : Type -> Type) where
  heldWhere : {r : Type}
            -> c
            -> List Bool
            -> List Bool
            -> ({s : Type} -> contents s -> Bool)
            -> ({s : Type} -> contents s -> Co (world e) (r, contents s))
            -> Co e (result r)

How a with of a c with a condition, with x := M where p do ss, is held in the world e, as a Holder’s is: heldWhere c written read p body takes what the c holds and checks p of it; where p holds, runs body with it, as held does, and where it does not, lets go of it all, untouched, and takes it again later, to check p again — until it holds. read says, as written does, which names p reads: only a change to one of those can make it hold, so it is those the holder waits on. How it waits, and what “later” is, is the holder’s: a behaviour queued again on its cowns once one of them is written, a condition variable waited on. A holder that cannot let go and take again (a file, an event) has no Waiter, and a with ... where of it is a type error.

holdingWhere

holdingWhere : {e : HFunctor}
             -> {c r : Type}
             -> c
             -> {{b : Binder c}}
             -> {{h : Waiter e c (b.Contents e) b.World b.Result}}
             -> List Bool
             -> List Bool
             -> ({s : Type} -> b.Contents e s -> Bool)
             -> ({s : Type}
                 -> b.Contents e s
                 -> Co (b.World e) (r, b.Contents e s))
             -> Co e (b.Result r)

with x := M ... where p do ss: holding’s, with the condition p over the names, and which of them it reads, held by its Waiter — the body run once p holds.