## Depth Comonads

I haven’t written much on this blog recently: since starting a PhD all of my writing output has gone towards paper drafts and similar things. Recently, though, I’ve been thinking about streams, monoids, and comonads and I haven’t manage to wrangle those thoughts into something coherent enough for a paper. This blog post is a collection of those (pretty disorganised) thoughts. The hope is that writing them down will force me to clarify things, but consider this a warning that the rest of this post may well be muddled and confusing.

# Streams

The first thing I want to talk about is streams.

record Stream (A : Type) : Type where coinductive field head : A tail : Stream A

This representation is *coinductive*: the type above contains
infinite values. Agda, unlike Haskell, treats inductive and coinductive
types differently (this is why we need the `coinductive`

keyword in the definition). One of the differences is that it doesn’t
check termination for construction of these values:

alternating : Stream Bool alternating .head = true alternating .tail .head = false alternating .tail .tail = alternating

```
alternating :: [Bool]
= True : False : alternating alternating
```

We have the equivalent in Haskell on the right. We’re also using some fancy syntax for the Agda code: copatterns (Abel and Pientka 2013).

Note that this type is only definable in a language with some notion
of laziness. If we tried to define a value like `alternating`

above in OCaml we would loop. Haskell has no problem, and Agda—through
its coinduction mechanism—can handle it as well.

Update 4-5-22: thanks to Arnaud Spiwack (@aspiwack)
for correcting me on this, it turns out the definition of
`alternating`

above *can* be written in Ocaml, even
without laziness. Apparently Ocaml has a facility for strict cyclic data
structures. Also, I should be a little more precise with what I’m saying
above: even without the extra facility for strict cycles, you can of
course write a lazy list with some kind of lazy wrapper type.

There is, however, an isomorphic type that can be defined without coinduction:

(notice that, in this form, the function `ℕ-alternating`

is the same function as `even : ℕ → Bool`

)

In fact, we can convert from the coinductive representation to the inductive one. This conversion function is more familiarly recognisable as the indexing function:

_[_] : Stream A → ℕ-Stream A xs [ zero ] = xs .head xs [ suc n ] = xs .tail [ n ]

I’m not just handwaving when I say the two representations are isomorphic: we can prove this isomorphism, and, in Cubical Agda, we can use this to transport programs on one representation to the other.

## Proof of isomorphism

tabulate : ℕ-Stream A → Stream A tabulate xs .head = xs zero tabulate xs .tail = tabulate (xs ∘ suc) stream-rinv : (xs : Stream A) → tabulate (xs [_]) ≡ xs stream-rinv xs i .head = xs .head stream-rinv xs i .tail = stream-rinv (xs .tail) i stream-linv : (xs : ℕ-Stream A) (n : ℕ) → tabulate xs [ n ] ≡ xs n stream-linv xs zero = refl stream-linv xs (suc n) = stream-linv (xs ∘ suc) n stream-reps : ℕ-Stream A ⇔ Stream A stream-reps .fun = tabulate stream-reps .inv = _[_] stream-reps .rightInv = stream-rinv stream-reps .leftInv xs = funExt (stream-linv xs)

One final observation about streams: another way to define a stream is as the cofree comonad of the identity functor.

record Cofree (F : Type → Type) (A : Type) : Type where coinductive field root : A step : F (Cofree F A) 𝒞-Stream : Type → Type 𝒞-Stream = Cofree id

Concretely, the `Cofree F A`

type is a possibly infinite
tree, with branches shaped like `F`

, and internal nodes
labelled with `A`

. It has the following characteristic
function:

{-# NON_TERMINATING #-} trace : ⦃ _ : Functor 𝐹 ⦄ → (A → B) → (A → 𝐹 A) → A → Cofree 𝐹 B trace ϕ ρ x .root = ϕ x trace ϕ ρ x .step = map (trace ϕ ρ) (ρ x)

Like how the free monad turns any functor into a monad, the cofree
comonad turns any functor into a comonad. Comonads are less popular and
widely-used than monads, as there are less well-known examples of them.
I have found it helpful to think about comonads through spatial
analogies. A lot of comonads can represent a kind of walk through some
space: the `extract`

operation tells you “what is immediately
here”, and the `duplicate`

operation tells you “what can I
see from each point”. For the stream, these two operations are inhabited
by `head`

and the following:

duplicate : Stream A → Stream (Stream A) duplicate xs .head = xs duplicate xs .tail = duplicate (xs .tail)

# Generalising Streams

There were three key observations in the last section:

- Streams are coinductive. This requires a different termination checker in Agda, and a different evaluation model in strict languages.
- They have an isomorphic representation based on
*indexing*. This isomorphic representation doesn’t need coinduction or laziness. - They are a special case of the cofree comonad.

Going forward, we’re going to look at generalisations of streams, and we’re going to see what these observations mean in the contexts of the new generalisations.

The thing we’ll be generalising is the index of the stream.
Currently, streams are basically structures that assign a value to every
`ℕ`

: what does a stream of—for instance—rational numbers look
like? To drive the intuition for this generalisation let’s first look at
the comonad instance on the `ℕ-Stream`

type:

ℕ-extract : ℕ-Stream A → A ℕ-extract xs = xs zero ℕ-duplicate : ℕ-Stream A → ℕ-Stream (ℕ-Stream A) ℕ-duplicate xs zero = xs ℕ-duplicate xs (suc n) = ℕ-duplicate (xs ∘ suc) n

This is the same instance as is on the `Stream`

type,
transported along the isomorphism between the two types (we could have
transported the instance automatically, using `subst`

or
`transport`

; I have written it out here manually in full for
illustration purposes).

The `ℕ-duplicate`

method here can changed a little to
reveal something interesting:

ℕ-duplicate₂ : ℕ-Stream A → ℕ-Stream (ℕ-Stream A) ℕ-duplicate₂ xs zero m = xs m ℕ-duplicate₂ xs (suc n) m = ℕ-duplicate₂ (xs ∘ suc) n m ℕ-duplicate₃ : ℕ-Stream A → ℕ-Stream (ℕ-Stream A) ℕ-duplicate₃ xs n m = xs (go n m) where go : ℕ → ℕ → ℕ go zero m = m go (suc n) m = suc (go n m) ℕ-duplicate₄ : ℕ-Stream A → ℕ-Stream (ℕ-Stream A) ℕ-duplicate₄ xs n m = xs (n + m)

In other words, `duplicate`

basically adds indices.

There is something distinctly *monoidal* about what’s going on
here: taking the `(ℕ, +, 0)`

monoid as focus, the
`extract`

method above corresponds to the monoidal empty
element, and the `duplicate`

method corresponds to the binary
operator on monoids. In actual fact, there is a comonad for any function
from a monoid, often called the `Traced`

comonad.

Traced : Type → Type → Type Traced E A = E → A extractᵀ : ⦃ _ : Monoid E ⦄ → Traced E A → A extractᵀ xs = xs ε duplicateᵀ : ⦃ _ : Monoid E ⦄ → Traced E A → Traced E (Traced E A) duplicateᵀ xs e₁ e₂ = xs (e₁ ∙ e₂)

# Reifying Traced

The second observation we made about streams was that they had an
isomorphic representation which didn’t need coinduction. What we can see
above, with `Traced`

, is a representation that *also*
doesn’t need coinduction. So what is the corresponding coinductive
representation? What does a generalised *reified* stream look
like?

So the first approach to reifying a function to a data structure is to simply represent the function as a list of pairs.

C-Traced : Type → Type → Type C-Traced E A = Stream (E × A)

This representation obviously isn’t ideal: it isn’t possible to
construct an isomorphism between `C-Traced`

and
`Traced`

. We can—kind of—go in one direction, but even that
function isn’t terminating:

{-# NON_TERMINATING #-} lookup-env : ⦃ _ : IsDiscrete E ⦄ → C-Traced E A → Traced E A lookup-env xs x = if does (x ≟ xs .head .fst) then xs .head .snd else lookup-env (xs .tail) x

I’m not too concerned with being fast and loose with termination and isomorphisms for the time being, though. At the moment, I’m just interested in exploring the relationship between streams and the indexing functions.

As a result, let’s try and push on this representation a little and
see if it’s possible to get something interesting and *almost*
isomorphic.

# Segmented Streams

To get a slightly nicer representation we can exploit the monoid a
little bit. We can do this by storing *offsets* instead of the
absolute indices for each entry. The data structure I have in mind here
looks a little like this:

┏━━━━━━━━━━┳━━━━━━┳━━━━━━┉ ┃x ┃y ┃z ┉ ┡━━━━━━━━━━╇━━━━━━╇━━━━━━┉ ╵⇤a╌╌╌╌╌╌╌⇥╵⇤b╌╌╌⇥╵⇤c╌╌╌╌┈

Above is a stream containing the values `x`

,
`y`

, and `z`

. Instead of each value corresponding
to a single entry in the stream, however, they each correspond to a
*segment*. The value `x`

, for instance, labels the
first segment in the stream, which has a length given by `a`

.
`y`

labels the second segment, with length `b`

,
`z`

with length `c`

, and so on.

The `Traced`

version of the above structure might be
something like this:

```
str :: Traced m a
| i < a = x
str i | i < a + b = y
| i < a + b + c = z
| ...
```

So the index-value mapping is also segmented. The stream, in this way, is kind of like a ruler, where different values mark out different quantities along the ruler, and the index function takes in a quantity and tells you which entry in the ruler that quantity corresponds to.

In code, we might represent the above data structure with the following type:

record Segments (E : Type) (A : Type) : Type where field length : E label : A next : Segments E A open Segments

The question is, then, how do we convert *this* structure to
an `Traced`

representation?

# Monuses

We need some extra operations on the monoid in the segments in order
to enable this conversion to the `Traced`

representation. The
extra operations are encapsulated by the monus algebra: I wrote about
this in the paper I submitted with Nicolas Wu to ICFP last year (2021). It’s a
simple algebra on monoids which basically encapsulates monoids which are
ordered in a sensible way.

The basic idea is that we construct an order on monoids which says “x is smaller than y if there is some z that we can add to x to get to y”.

_≼_ : ⦃ _ : Monoid A ⦄ → A → A → Type _ x ≼ y = ∃ z × (y ≡ x ∙ z)

A monus is a monoid where we can extract that `z`

, when it
exists. On the monoid `(ℕ, +, 0)`

, for instance, this order
corresponds to the normal ordering on `ℕ`

.

Extracting the `z`

above corresponds to a kind of
difference operator:

_∸_ : ℕ → ℕ → ℕ x ∸ zero = x suc x ∸ suc y = x ∸ y _ ∸ _ = zero

This operator is sometimes called the monus. It is a kind of partial, or truncating, subtraction:

_ : 5 ∸ 2 ≡ 3 _ = refl _ : 2 ∸ 5 ≡ 0 _ = refl

And, indeed, this operator “extracts” the `z`

, when it
exists.

∸‿is-monus : ∀ x y → (x≼y : x ≼ y) → y ∸ x ≡ fst x≼y ∸‿is-monus zero _ (z , y≡0+z) = y≡0+z ∸‿is-monus (suc x) (suc y) (z , y≡x+z) = ∸‿is-monus x y (z , suc-inj y≡x+z) ∸‿is-monus (suc x) zero (z , 0≡x+z) = ⊥-elim (zero≢suc 0≡x+z)

Our definition of a monus is simple: a monus is anything where the
order ≼, sometimes called the “algebraic preorder”, is total and
antisymmetric. This is precisely what lets us write a function which
takes the `Segments`

type and converts it back to the
`Traced`

type.

{-# NON_TERMINATING #-} Segments→Traced : ⦃ _ : Monus E ⦄ → Segments E A → Traced E A Segments→Traced xs i with xs .length ≤? i ... | yes (j , i≡xsₗ∙j) = Segments→Traced (xs .next) j ... | no _ = xs .label

This function takes an index, and checks if that length is greater than or equal to the first segment in the stream of segments. If it is, then it continues searching through the rest of the segments with the index reduced by the size of that first segment. If not, then it returns the label of the first segment.

Taking the old example, we are basically converting to ∸ from +:

```
str :: Traced m a
| i < a = x
str i | i ∸ a < b = y
| i ∸ a ∸ b < c = z
| ...
```

The first issue here is that this definition is not terminating. That might seem an insurmountable problem at first—we are searching through an infinite stream, after all—but notice that there is one paremeter which is decreasing on each recursive call: the index. Well, it only decreases if the segment is non-zero: this can be enforced by changing the definition of the segments type:

record ℱ-Segments (E : Type) ⦃ _ : Monus E ⦄ (A : Type) : Type where coinductive field label : A length : E length≢ε : length ≢ ε next : ℱ-Segments E A open ℱ-Segments

This type allows us to write the following definition:

module _ ⦃ _ : Monus E ⦄ (wf : WellFounded _≺_) where wf-index : ℱ-Segments E A → (i : E) → Acc _≺_ i → A wf-index xs i a with xs .length ≤? i ... | no _ = xs .label wf-index xs i (acc wf) | yes (j , i≡xsₗ∙j) = wf-index (xs .next) j (wf j (xs .length , i≡xsₗ∙j ; comm _ _ , xs .length≢ε)) ℱ-Segments→Traced : ℱ-Segments E A → Traced E A ℱ-Segments→Traced xs i = wf-index xs i (wf i)

# Trying to build an isomorphism

So the `ℱ-Segments`

type is interesting, but it only
really gives one side of the isomorphism. There is no way to write a
function `Traced E A → ℱ-Segments E A`

.

The problem is that there’s no way to get the “next” segment from a
function `E → A`

. We can find the label of the first segment,
by applying the function to `ε`

, but there’s no real way to
figure out the *size* of this segment. We can change
`Traced`

little to *provide* this size, though.

Ind : ∀ E → ⦃ _ : Monus E ⦄ → Type → Type Ind E A = E → A × Σ[ length ⦂ E ] × (length ≢ ε)

This new type will return a tuple consisting of the value indicated
by the supplied index, along with the distance to the next segment. For
instance, on the example stream given in the diagram earlier, supplying
an index `i`

that is bigger than `a`

but smaller
than `a + b`

, this function should return `y`

along with some `j`

such that `i + j ≡ a + b`

.
Diagrammatically:

╷⇤i╌╌╌╌╌╌╌╌⇥╷⇤j╌╌⇥╷ ┢━━━━━━━━┳━━┷━━━━━╈━━━━━━┉ ┃x ┃y ┃z ┉ ┡━━━━━━━━╇━━━━━━━━╇━━━━━━┉ ╵⇤a╌╌╌╌╌⇥╵⇤b╌╌╌╌╌⇥╵⇤c╌╌╌╌┈

This can be implemented in code like so:

module _ ⦃ _ : Monus E ⦄ where wf-ind : ℱ-Segments E A → (i : E) → Acc _≺_ i → A × ∃ length × (length ≢ ε) wf-ind xs i _ with xs .length ≤? i ... | no xsₗ≰i = let j , _ , j≢ε = <⇒≺ i (xs .length) xsₗ≰i in xs .label , j , j≢ε wf-ind xs i (acc wf) | yes (j , i≡xsₗ∙j) = wf-ind (xs .next) j (wf j (xs .length , i≡xsₗ∙j ; comm _ _ , xs .length≢ε)) ℱ-Segments→Ind : WellFounded _≺_ → ℱ-Segments E A → Ind E A ℱ-Segments→Ind wf xs i = wf-ind xs i (wf i)

Again, if the monus has finite descending chains, this function is terminating. And the nice thing about this is that it’s possible to write a function in the other direction:

Ind→ℱ-Segments : ⦃ _ : Monus E ⦄ → Ind E A → ℱ-Segments E A Ind→ℱ-Segments ind = let x , s , s≢ε = ind ε in λ where .label → x .length → s .length≢ε → s≢ε .next → Ind→ℱ-Segments (ind ∘ (s ∙_))

The problem here is that this isomorphism is only half correct. We
can prove that converting to `Ind`

and back is the identity,
but not the other direction. There are too many functions in
`Ind`

.

Nonetheless, it’s still interesting!

# State Comonad

There is a comonad on state (Waern 2018; Kmett
2018) that is different from store. Notice that above the
`Ind`

type has the same type (almost) as
`State E A`

.

This is interesting in two ways: first, it gives some concrete, spatial intuition for what’s going on with the state comonad.

Second, it gives a kind of interesting *monad* instance on the
stream. If we apply the `Ind→ℱ-Segments`

function to the
implementation of `join`

on state, we *should* get a
`join`

on `ℱ-Segments`

. And we do!

First, we need to redefine `Ind`

to the following:

𝒜-Ind : ∀ E → ⦃ _ : Monus E ⦄ → Type → Type 𝒜-Ind E A = (i : E) → A × Σ[ length ⦂ E ] × (i ≺ length)

This is actually isomorphic to the previous definition, but we return the absolute value of the next segment, rather than the distance to the next segment.

𝒜-iso : ⦃ _ : Monus E ⦄ → 𝒜-Ind E A ⇔ Ind E A 𝒜-iso .fun xs i = let x , s , k , s≡i∙k , k≢ε = xs i in x , k , k≢ε 𝒜-iso .inv xs i = let x , s , s≢ε = xs i in x , i ∙ s , s , refl , s≢ε 𝒜-iso .rightInv _ = refl 𝒜-iso .leftInv xs p i = let x , s , k , s≡i∙k , k≢ε = xs i in x , s≡i∙k (~ p) , k , (λ q → s≡i∙k (~ p ∨ q)) , k≢ε

The implemention of `join`

on this type is the
following:

𝒜-join : ⦃ _ : Monus E ⦄ → 𝒜-Ind E (𝒜-Ind E A) → 𝒜-Ind E A 𝒜-join xs i = let x , j , i<j = xs i y , k , k<j = x j in y , k , ≺-trans i<j k<j

This is the same definition of `join`

as for
`State`

, modulo the `<`

fiddling.

On a stream, this operation corresponds to taking a stream of streams and collapsing it to a single stream. It does this by taking a prefix of each internal stream equal in size to the segment of the outer entry. Diagrammatically:

┏━━━━━━━━━━┳━━━━━━┳━━━━━━┉ ┃xs ┃ys ┃zs ┉ ┡━━━━━━━━━━╇━━━━━━╇━━━━━━┉ ╵⇤a╌╌╌╌╌╌╌⇥╵⇤b╌╌╌⇥╵⇤c╌╌╌╌┈ ╱ ╲ ╱ ╲ ╱ ╲ ╱ ╲ ╱ ╲ ╷⇤b╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌⇥╷ ┢━━━━━━━┳━━━━━━┳━━━┷┉ ys = ┃xʸ ┃yʸ ┃zʸ ┉ ┡━━━━━━━╇━━━━━━╇━━━━┉ ╵⇤aʸ╌╌╌⇥╵⇤bʸ╌╌⇥╵⇤cʸ╌┈

Here we start with a stream consisting of the streams
`xs`

, `ys`

, and `zs`

, followed by some
other streams. Zooming in on `ys`

, we see that it is in a
segment of length `b`

, and consists of three values
`xʸ`

, `yʸ`

, and `zʸ`

, with segment
lengths `aʸ`

, `bʸ`

, and `cʸ`

,
respectively.

Calling `join`

on this stream will give us the following
stream:

┏━┉━┳━━━━┳━━━━┳━━━━━┳━━━━┉ ┃ ┉ ┃xʸ ┃yʸ ┃zʸ ┃ ┉ ┡━┉━╇━━━━╇━━━━╇━━━━━╇━━━━┉ │ │⇤aʸ⇥╵⇤bʸ⇥╵⇤╌╌┈⇥│ ╵⇤a⇥╵⇤b╌╌╌╌╌╌╌╌╌╌╌╌⇥╵⇤c╌╌┈

Again, we’re focusing on the `ys`

section here, which
occupies the segment from `a`

to `a ∙ b`

. After
`join`

, this segment is occupied by three elements,
`xʸ`

, `yʸ`

, and `zʸ`

.

Notice that this isn’t quite the normal `join`

on streams.
That `join`

takes a stream of streams, and turns the
`i`

th entry into the `i`

th entry in the underlying
stream. It’s a diagonalisation, in other words.

This one is kind of similar, but it takes chunks of the outer stream.

# Theory

All of this so far is very hand-wavy. We have an almost isomorphism (a split surjection, to be precise), but not much in the way of concrete theoretical insights, just some vague gesturing towards spatial metaphors and so on.

Thankfully, there are two seperate areas of more serious research that seem related to the stuff I’ve talked about here. The first is update monads and directed containers, and the second is graded comonads. I think I understand graded comonads and the related work better out of the two, but update monads and directed containers seems more closely related to what I’m doing here.

# Update Monads and Directed Containers

There are a few papers on this topic: Ahman, Chapman, and Uustalu (2012), Ahman and Uustalu (2013; Ahman and Uustalu 2014; Ahman and Uustalu 2016).

The first of these, “When Is a Container a Comonad?” constructs, as the title suggests, a class for containers which are comonads in a standard way.

Here’s the definition of a container:

Container : Type₁ Container = Σ[ Shape ⦂ Type ] × (Shape → Type) ⟦_⟧ : Container → Type → Type ⟦ S , P ⟧ X = Σ[ s ⦂ S ] × (P s → X)

Containers are a generic way to describe a class of well-behaved
functors. Any container is a pair of a shape and position. Lists, for
instance, are containers, where their shape is described by the natural
numbers (the shape here is the length of the list). The positions in
such a list are the numbers smaller than the length, in
dependently-typed programming we usually use the `Fin`

type
for this:

Fin : ℕ → Type Fin n = ∃ m × (m <ℕ n)

The container version of lists, then, is the following:

ℒ𝒾𝓈𝓉 : Type → Type ℒ𝒾𝓈𝓉 = ⟦ ℕ , Fin ⟧

Here’s the same list represented in the standard way, and as a container:

The benefit of using containers is that it gives a standard, generic, and composable way to construct functors that have some nice properties (like strict positivity). They’re pretty annoying to use in practice, though, which is a shame.

Directed containers are container that have three extra operations.

- A
`tail`

-like operation, where a position can be converted into the shape of containers that the suffic from that position. - A
`head`

-like operation, where you can always return the root position. - A
`+`

-like operation, where you take a position on some tail and translate it into a position on the original container, by adding it.

As the paper observes, these are very similar to a “dependently-typed” version of the monoid methods. This seems to me to be very similar to the indexing stuff we were doing earlier on.

The real interesting part is in the paper “Update Monads: Cointerpreting Directed Containers” (Ahman and Uustalu 2014). This paper presents a variant on state monads, called “update monads”.

These are monads that use a monoid action:

record RightAction (𝑃 : Type) (𝑆 : Type) : Type where infixl 5 _↓_ field ⦃ monoid⟨𝑃⟩ ⦄ : Monoid 𝑃 _↓_ : 𝑆 → 𝑃 → 𝑆 ↓-assoc : ∀ x y z → (x ↓ y) ↓ z ≡ x ↓ (y ∙ z) ↓-ε : ∀ x → x ↓ ε ≡ x

A (right) monoid action is a monoid along with a function
`↓`

that “acts” on some other set, in a way that coheres with
the monoid methods. The definition is given above. One way to think
about it is that if a monoid `𝑃`

has an action on
`𝑆`

it means that elements of `𝑃`

can kind of be
transformed into elements of `𝑆 → 𝑆`

.

Upd : (𝑃 𝑆 : Type) ⦃ _ : RightAction 𝑃 𝑆 ⦄ → Type → Type Upd 𝑃 𝑆 X = 𝑆 → 𝑃 × X η : ⦃ _ : RightAction 𝑃 𝑆 ⦄ → A → Upd 𝑃 𝑆 A η x s = ε , x μ : ⦃ _ : RightAction 𝑃 𝑆 ⦄ → Upd 𝑃 𝑆 (Upd 𝑃 𝑆 A) → Upd 𝑃 𝑆 A μ xs s = let p , x = xs s q , y = x (s ↓ p) in (p ∙ q , y)

It turns out that the dependently-typed version of this gives directed containers.

# Grading and the Cofree Comonad

I’m still in the early stages of understanding all of this material, but at the moment graded comonads and transformers are concepts that I’m much more familiar and comfortable with.

The idea behind graded monads and comonads is similar to the idea
behind any indexed monad: we’re adding an extra type parameter to the
monad or type, which can constrain the operations involved. The
*graded* monads and comonads use a monoid as that index. This
works particularly nicely, in my opinion: just allowing any index at all
sometimes feels a little unstructured. The grading construction seems to
constrain things to the right degree: the use of the monoid, as well,
works really well with comonads.

That preamble out of the way, here’s the definition of a graded comonad:

record GradedComonad (𝑆 : Type) ⦃ _ : Monoid 𝑆 ⦄ (𝐶 : 𝑆 → Type → Type) : Type₁ where field extract : 𝐶 ε A → A extend : (𝐶 y A → B) → 𝐶 (x ∙ y) A → 𝐶 x BThis also has a few laws, which are expressed cleaner using cokleisli composition:

_=<=_ : (𝐶 x B → C) → (𝐶 y A → B) → 𝐶 (x ∙ y) A → C (g =<= f) x = g (extend f x) field idˡ : (f : 𝐶 x A₀ → B₀) → PathP (λ i → 𝐶 (ε∙ x i) A₀ → B₀) (extract =<= f) f idʳ : (f : 𝐶 x A₀ → B₀) → PathP (λ i → 𝐶 (∙ε x i) A₀ → B₀) (f =<= extract) f c-assoc : (f : 𝐶 x C₀ → D₀) (g : 𝐶 y B₀ → C₀) (h : 𝐶 z A₀ → B₀) → PathP (λ i → 𝐶 (assoc x y z i) A₀ → D₀) ((f =<= g) =<= h) (f =<= (g =<= h))

This seems to clearly be related to the stream constructions. Grading is all about the monoidal information about a comonad: the streams above are a comonad which indexes its entries with a monoid.

There are now two constructions I want to show that suggest a link
betweent the stream constructions and graded comonads. First of these is
the *Cofree degrading comonad*:

record G-CofreeF (𝐹 : Type → Type) (𝐶 : 𝑆 → Type → Type) (A : Type) : Type where coinductive; constructor _◃_ field here : A step : 𝐹 (∃ w × 𝐶 w (G-CofreeF 𝐹 𝐶 A)) open G-CofreeF G-Cofree : ⦃ _ : Monoid 𝑆 ⦄ → (Type → Type) → (𝑆 → Type → Type) → Type → Type G-Cofree 𝐹 𝐶 A = 𝐶 ε (G-CofreeF 𝐹 𝐶 A)

This construction is similar to the cofree comonad transformer: it is
based on the cofree comonad, but with an extra (graded) comonad wrapped
around each level. For any functor 𝐹 and graded comonad 𝐶,
`G-Cofree 𝐹 𝐶`

is a comonad. The implementation of
`extract`

is simple:

extract′ : ⦃ _ : Monoid 𝑆 ⦄ ⦃ _ : GradedComonad 𝑆 𝐶 ⦄ → G-Cofree 𝐹 𝐶 A → A extract′ = here ∘ extract

`extend`

is more complex. First, we need a version of
`extend`

which takes a proof that the grade is of the right
form:

module _ { 𝐶 : 𝑆 → Type → Type } where extend[_] : ⦃ _ : Monoid 𝑆 ⦄ ⦃ _ : GradedComonad 𝑆 𝐶 ⦄ → x ∙ y ≡ z → (𝐶 y A → B) → 𝐶 z A → 𝐶 x B extend[ p ] k = subst (λ z → 𝐶 z _ → _) p (extend k)

Then we can implement the characteristic function on the free
comonad: `traceT`

. On graded comonads it has the following
form:

module Trace ⦃ _ : Monoid 𝑆 ⦄ ⦃ _ : GradedComonad 𝑆 𝐶 ⦄ ⦃ _ : Functor 𝐹 ⦄ where module _ {A B} where {-# NON_TERMINATING #-} traceT : (𝐶 ε A → B) → (𝐶 ε A → 𝐹 (∃ w × 𝐶 w A)) → 𝐶 ε A → G-Cofree 𝐹 𝐶 B traceT ϕ ρ = ψ where ψ : 𝐶 x A → 𝐶 x (G-CofreeF 𝐹 𝐶 B) ψ = extend[ ∙ε _ ] λ x → ϕ x ◃ map (map₂ ψ) (ρ x)

This function is basically the unfold for the free degrading comonad.
If `G-Cofree`

is a internally-labelled tree, then
`ϕ`

above is the labelling function, and `ρ`

is
the “next” function, returning the children for some root.

Using this, we can implement `extend`

:

extend′ : (G-Cofree 𝐹 𝐶 A → B) → G-Cofree 𝐹 𝐶 A → G-Cofree 𝐹 𝐶 B extend′ f = traceT f (step ∘ extract)

The relation between this and the stream is that the stream can be
defined in terms of this:
`Stream W = G-Cofree id (GC-Id W)`

.

Finally, the last construction I want to introduce is the following:

module _ ⦃ _ : Monus 𝑆 ⦄ where data Prefix-F⊙ (𝐹 : Type → Type) (𝐶 : 𝑆 → Type → Type) (i j : 𝑆) (A : Type) : Type where prefix : ((i≤j : i ≤ j) → A × 𝐹 (∃ k × 𝐶 k (Prefix-F⊙ 𝐹 𝐶 k (fst i≤j) A))) → Prefix-F⊙ 𝐹 𝐶 i j A Prefix⊙ : (𝐹 : Type → Type) (𝐶 : 𝑆 → Type → Type) (j : 𝑆) (A : Type) → Type Prefix⊙ 𝐹 𝐶 j A = 𝐶 ε (Prefix-F⊙ 𝐹 𝐶 ε j A) Prefix : (𝐹 : Type → Type) (𝐶 : 𝑆 → Type → Type) (A : Type) → Type Prefix 𝐹 𝐶 A = ∀ {i} → Prefix⊙ 𝐹 𝐶 i A

This type is designed to mimic sized type definitions. It has an
implicit parameter which can be set, by the user of the type, to some
arbitrary depth. Basically the parameter means “explore to this depth”;
by using the `∀`

we say that it is defined up to any
arbitrary depth.

When the `≺`

relation on the monus is well founded it is
possible to implement `traceT`

:

module _ ⦃ _ : GradedComonad 𝑆 𝐶 ⦄ ⦃ _ : Functor 𝐹 ⦄ (wf : WellFounded _≺_) {A B : Type} where traceT : (𝐶 ε A → B) → (𝐶 ε A → 𝐹 (∃ w × (w ≢ ε) × 𝐶 w A)) → 𝐶 ε A → Prefix 𝐹 𝐶 B traceT ϕ ρ xs = extend[ ∙ε _ ] (λ xs′ → prefix λ _ → ϕ xs′ , map (map₂ (ψ (wf _))) (ρ xs)) xs where ψ : Acc _≺_ y → (x ≢ ε) × 𝐶 x A → 𝐶 x (Prefix-F⊙ 𝐹 𝐶 x y B) ψ (acc wf) (x≢ε , xs) = extend[ ∙ε _ ] (λ x → prefix λ { (k , y≡x∙k) → ϕ x , map (λ { (w , w≢ε , xs) → w , ψ (wf k (_ , y≡x∙k ; comm _ _ , x≢ε)) (w≢ε , xs)}) (ρ x)}) xs

# Conclusion

Comonads are much less widely used than monads in Haskell and similar languages. Part of the reason, I think, is that they’re too powerful in a non-linear language. Monads are often used to model sublanguages where it’s possible to introduce “special” variables which interact with the monadic context.

```
= do
pyth <- [1..10]
x <- [1..10]
y <- [1..10]
z *x + y*y == z*z)
guard (xreturn (x,y,z)
```

The `x`

variable here semantically spans over the range
`[1..10]`

. In the following two examples we see the semantics
of state and maybe:

```
sum :: [Int] -> Int
sum xs = flip evalState 0 $ do
0
put $ \x -> do
for_ xs <- get
n + x)
put (n <- get
m return m
```

```
data E = Lit Int | E :+: E | E :/: E
eval :: E -> Maybe Int
Lit n) = n
eval (:+: ys) = do x <- eval xs
eval (xs <- eval ys
y return (x + y)
:/: ys) = do x <- eval xs
eval (xs <- eval ys
y /= 0)
guard (y return (x / y)
```

The variables `n`

and `m`

introduced in the
state example are “special” because their values depend on the
computations that came before. In the maybe example the variables
introduced could be `Nothing`

.

You can’t do the same thing with comonads because you’re always able
to extract the “special” variable with
`extract :: m a -> a`

. Instead of having special variable
*introduction*, comonads let you have special variable
*elimination*. But, since Haskell isn’t linear, you can always
just discard a variable so this isn’t much use.

Looking at the maybe example, we have a function
`eval :: E -> Maybe Int`

that introduces an
`Int`

variable with a “catch”: it is wrapped in a
`Maybe`

. We want to use the `eval`

function as if
it were a normal function `E -> Int`

, with all of the
bookkeeping managed for us: that’s what monads and do notation (kind of)
allow us to do.

An analagous example with comonads might be having a function
`consume :: m V -> String`

. This “handles” a
`V`

value, but the “catch” is that it needs an `m`

context to do so. If we want to treat the `consume`

function
as if it were a normal function `V -> String`

then
comonads (and
codo notation Orchard and Mycroft 2013) would be a perfect
fit.

The reason that this analagous case doesn’t arise very often is that
we don’t have many handlers that look like `m V -> String`

in Haskell. Why? Because if we want to “handle” a `V`

we can
just discard it: as a non-linear language, you do not need to perform
any ceremony to discard a variable in Haskell.

Graded comonads, though, seem to be much more useful than normal
comonads. I think it is becuase they basically get rid of the
`m a -> a`

function, changing it into a much more
restricted form. In this way, they give a kind of small linear language,
but just for the monoidal type parameter.

And there are a lot of uses for the graded comonads. Above we’ve used
them for termination checking. A recursive function might have the form
`a -> b`

, where `a`

is the thing being recursed
on. If we’re using well-founded recursion to show that it’s terminating,
though, we add an extra parameter, an `Acc _<_`

proof,
turning this function into `Acc _<_ w × a -> b`

. The
`Acc _<_`

here is the graded comonad, and this recursive
function is precisely the “handler”.

Other examples might be privacy or permissions: a function might be
able to work on some value, but only if it has particular
*permission* regarding that value. The permission here is the
monoid.

There are other examples I’m sure, those are just the couple that I have been thinking about.

# References

*Foundations of Software Science and Computational Structures*, 74–88. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg. doi:10.1007/978-3-642-28729-9_5.

*Progress in Informatics*(10) (March): 3. doi:10.2201/NiiPi.2013.10.2.

*Proceedings of the ACM on Programming Languages*5 (ICFP) (August): 72:1–72:30. doi:10.1145/3473577.

*The Comonad.Reader*. http://comonad.com/reader/2018/the-state-comonad/.

*Implementation and Application of Functional Languages*, ed by. Ralf Hinze, 1–17. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer. doi:10.1007/978-3-642-41582-1_1.

*reddit.com/r/haskell*. https://www.reddit.com/r/haskell/comments/7oav51/i_made_a_monad_that_i_havent_seen_before_and_i/.