How do coeffects work, anyway?

Posted on April 26, 2026

I’ve done some more reading on coeffects. These were some of the main sources I read:

These are my main takeaways:

Coeffects are dual to effects in that you use a graded comonad instead of a graded monad. I’m still not totally sure how strict of a categorical dual this is? The particular difference that makes me skeptical of the duality is that coeffect grades aren’t just a monoid. Some earlier papers use a specialized “coeffect algebra” but it seems like the newer ones have settled on semirings.

Effects track the wrapper you’re putting around the result, coeffects track the wrapper you’re putting around the context. At first, I thought that “context” was a little metaphorical. But the comonadic extract is a function of type M A -> A, so the premise of its introduction rule is of the form G, M A |- A. The wrapper M appears on a variable in the context! Whereas to introduce a monadic return (of type A -> M A), we have a premise G, A |- M A with M wrapping the result. (Different coeffect systems take different approaches to the context, so this might not always be quite how it works, but they’re mostly equivalent; see this helpful paper by Vilem Liepelt.)

The comonad operations (extract, extend) operate on the multiplicative monoid of the semiring, which looks like what I guessed graded comonads would look like in the previous post. They behave like linear logic’s dereliction and promotion rules. The additive monoid of the semiring is used for the context-combining operation, again following the mold of linear logic.

A Core Quantitative Coeffect Calculus defines a categorical semantics for coeffects as a “bounded exponential situation”. I’m working off the rough assumption that the details I don’t have strong intuitions for (e.g. this functor is symmetric comonoidal aka oplax monoidal) are basically just coherence conditions. Setting those aside, what it amounts to is that the semiring (call this S) acts like exponentiation on bases drawn from the main category of types (call this A with terminal object I). The natural transformations mostly let you push operations downwards from S into A, and not the other way around:

  • Rule epsilon: if you have a^1 you can convert it to a. This is the basis for dereliction and looks exactly like comonadic extract.
  • Rule delta: if you have a^(x*y) you can convert this to (a^x)^y. This looks exactly like comonadic extend and is part of the basis for promotion.
  • Rule C: if you have a^(x+y) you can convert this to a^x (times_A) a^y. Semiring sum distributes into product type.
  • Rule W: if you have a^0 you can convert this to A’s terminal object I, dropping it.

There’s also a rule that just shifts operators in A:

  • Rule M: you can convert a^x (times_A) b^x to (a (times_A) b)^x. This lets you merge equally-coeffected things into their product types

and one rule that lets you introduce exponents without already having one:

  • rule N: you can convert I to I^x for any x. This lets you make any number of copies of constants (functions I -> a)

Also, not a natural transformation, but subtyping comes from the functoriality of this exponentiation, because the categorical semiring’s arrows correspond to its preordering. so you can go from a greater to a lesser exponent as desired. The idea is that a context is a product of objects of A (the types of its variables) possibly taken to powers from the semiring (the coeffects on the variables). An arrow from a context to a type T gives a term of T in that context. This inclines me to think that the exponentiation-like behavior of the coeffects is because they’re acting like functions.

All the rules have pretty obvious meanings when the semiring is the natural numbers. You can convert A^(n+1) to (A^n, A^1), and A^1 to linear A, which lets you decrement the coeffect to use the variable once linearly. So having a natural number grade tells you how many copies of something you have. This corresponds neatly to functions from n-element sets to the type in question, or equivalently n-way products.

What I’m less sure about is how it generalizes to other semirings. Unfortunately their other examples all depend on the fiddly details of where you insert “observations”, which feel rather unsatisfying to me. It’s not entirely clear to me how much of the behavior falls naturally out of the choice of semiring or is implementation-dependent. I also need to be careful when trying to think about semirings that aren’t the natural numbers.

In the case of the min-plus (“tropical”) semiring on the natural numbers, it looks like this:

  • Semiring addition is min, semiring multiplication is addition, semiring infty is 0, semiring 1 is 0, and ordering is reversed.
  • Since min(x, x) = x, you can convert a^x = a^(min(x, x)) into (a^x, a^x) by rule C, which can be converted into (a, a)^x by rule M. Notably a^0 (remember, 0 is semiring-1) can be converted to (a, a)^0 and extracted to (a, a). It’s fully nonlinear for non-coeffected terms.
  • In fact, given a^x and any y normally-larger (tropical-smaller) than x, a^x = a^(min(x, y)) = (a^x, a^y) by rule C, though you can’t pull out the exponent since they differ.
  • By subtyping, if you have a^n, you can convert n to any normally-larger (tropical-smaller) m. It can be dropped at infty.
  • Since nat-addition is semiring multiplication, a^(n + m) can be converted to (an)m.

So where we think of natural number coeffects as counting “how many of these are you allowed to use”, we might perhaps think of tropical coeffects as some baggage attached to your variable that you have to get rid of before you can use it normally:

  • Subtyping says you can always unnecessarily carry around extra baggage.
  • epsilon says if you’ve got no baggage left (semiring-1 being nat-0) you can use your variable normally.
  • delta says that if your variable has (n+m) baggage you can split the baggage into n-baggage and m-baggage.
  • C says that you can duplicate your variable into a product, as long as both halves of the product have as much baggage as the original (e.g. a^min(n,m) -> (a^n, a^m)).
  • W says that if you’ve got infinite baggage, you can give up on ever getting rid of it and just throw away your variable.
  • M says if you have the same baggage on both a and b, you can combine them into a product with the shared baggage.
  • N says you can put as much baggage on constants as you like, including none at all.

The max-plus (“arctic”) semiring mostly looks like this but backwards, so it could maybe be interpreted as a sort of “fuel” used by some terms. It seems to be used for functions that operate on streams, to count the number of future stream values. That makes some sense to me.

Information flow in these systems seems like a little bit of a nightmare. I attempted to implement the type system from the Core Quantitative Calculus paper and ran into some substantial obstacles, especially around the rule for function application. On the one hand, I want to infer types for at least some terms, because otherwise you have to guess the types of the subterms in a beta redex. On the other hand, I want to infer the coeffects required by terms, because otherwise you have to simply guess how to split up the incoming context between subterms of a beta redex. But then you have to try to simultaneously infer the type for a term and the context in which it has that type, which seems impossible. I think this is why Granule relies so heavily on SMT solvers, to do the guessing.