What does a nontrivial comonoid look like?

Question

Comonoids are mentioned, for example, in Haskell's `distributive` library docs: Due to the lack of non-trivial comonoids in Haskell, we can restrict ourselves to requiring a Functor rather than some Coapplicative class. After a little searching I found a StackOverflow answer that explains this a bit more with the laws that comonoids would have to satisfy. So I think I understand why there's only one possible instance for a hypothetical Comonoid typeclass in Haskell. Thus, to find a nontrivial comonoid, I suppose we'd have to look in some other category. Surely, if category theorists have a name for comonoids, then there are some interesting ones. The other answers on that page seem to hint at an example involving `Supply`, but I couldn't figure one out that still satisfies the laws. I also turned to Wikipedia: there's a page for monoids that doesn't reference category theory, which seems to me as an adequate description of Haskell's `Monoid` typeclass, but "comonoid" redirects to a ca…

Accepted Answer

As Phillip JF mentioned, comonoids are interesting to talk about in substructural logics. Let's talk about linear lambda calculus. This is much like your normal typed lambda calculus except that every variable must be used exactly once.

To get a feel, let's count linear functions of given types, i.e.

```
a -> a
```

has exactly one inhabitant, `id`. While

```
(a,a) -> (a,a)
```

has two, `id` and `flip`. Note that in regular lambda calculus `(a,a) -> (a,a)` has four inhabitants

```
(a, b) ↦ (a, a)
(a, b) ↦ (b, b)
(a, b) ↦ (a, b)
(a, b) ↦ (b, a)
```

but the first two require that we use one of the arguments twice while discarding the other. This is exactly the essence of linear lambda calculus—disallowing those kinds of functions.

As a quick aside, what's the point of linear LC? Well, we can use it to model linear effects or resource usage. If, for instance, we have a file type and a few transformers it might look like

```
data File
open  :: String -> File
close :: File   -> ()      -- consumes a file, but we're ignoring purity right now
t1    :: File -> File
t2    :: File -> File
```

and then the following are valid pipelines:

```
close . t1 . t2 . open
close . t2 . t1 . open
close . t1      . open
close . t2      . open
```

but this "branching" computation isn't

```
let f1 = open "foo"
    f2 = t1 f1
    f3 = t2 f1
in close f3
```

since we used `f1` twice.

Now, you might be wondering something at this point about what things must follow the linear rules. For instance, I decided that some pipelines don't have to include both `t1` and `t2` (compare the enumeration exercise from before). Further, I introduced the `open` and `close` functions which happily create and destroy the `File` type despite that being a violation of linearity.

Indeed, we might posit the existence of functions which violate linearity—but not all clients may. It's much like the `IO` monad—all of the secrets live inside the implementation of `IO` so that users work in a "pure" world.

And this is where `Comonoid` comes in.

```
class Comonoid m where
  destroy :: m -> ()
  split   :: m -> (m, m)
```

A type that instantiates `Comonoid` in a linear lambda calculus is a type which has carry-along destruction and duplication rules. In other words, it's a type which isn't very much bound by linear lambda calculus at all.

Since Haskell doesn't implement the linear lambda calculus rules at all, we can always instantiate `Comonoid`

```
instance Comonoid a where
  destroy a = ()
  split a   = (a, a)
```

Or, perhaps the other way to think of it is that Haskell is a linear LC system that just happens to instantiate `Comonoid` for every type and applies `destroy` and `split` for you automatically.

What does a nontrivial comonoid look like?

Solution

Problem

Related problems