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]
alternating = True : False : 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:

ℕ-Stream : Type → Type
ℕ-Stream A = ℕ → A

ℕ-alternating : ℕ-Stream Bool
ℕ-alternating zero          = true
ℕ-alternating (suc zero)    = false
ℕ-alternating (suc (suc n)) = ℕ-alternating n

(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.

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:

1. Streams are coinductive. This requires a different termination checker in Agda, and a different evaluation model in strict languages.
2. They have an isomorphic representation based on indexing. This isomorphic representation doesn’t need coinduction or laziness.
3. 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
str i | i < a         = x
      | 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:

_ :  ∸  ≡ 
_ = refl

_ :  ∸  ≡ 
_ = 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
str i | i         < a = x
      | 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 ith entry into the ith 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:

someBools : List Bool
someBools = true ∷ true ∷ false ∷ true ∷ []

someBools′ : ℒ𝒾𝓈𝓉 Bool
someBools′ .fst = 
someBools′ .snd ( , _) = true
someBools′ .snd ( , _) = true
someBools′ .snd ( , _) = false
someBools′ .snd ( , _) = true

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 “Updated 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  _↓_
  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 B

  _=<=_ : (𝐶 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.

pyth = do
  x <- [1..10]
  y <- [1..10]
  z <- [1..10]
  guard (x*x + y*y == z*z)
  return (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
  put 0
  for_ xs $ \x -> do
    n <- get
    put (n + x)
  m <- get
  return m

data E = Lit Int | E :+: E | E :/: E

eval :: E -> Maybe Int
eval (Lit n) = n
eval (xs :+: ys) = do x <- eval xs
                      y <- eval ys
                      return (x + y)
eval (xs :/: ys) = do x <- eval xs
                      y <- eval ys
                      guard (y /= 0)
                      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 provacy 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