18
$\begingroup$

One could define streams in the following manner

Section stream.
  Variable A : Type.

  CoInductive stream : Type :=
  | Cons : A -> stream -> stream.
End stream.

But as far as I can tell, such a coinductive stream is isomorphic to a function nat -> A. Arguably, working with the coinductive definition is harder.

What is an example of a situation where working with a coinductive type is a more intuitive option to express a certain object? When is it more convenient to use a coinductive proof? What are some instances when the coinductive proof/value makes the most sense?

$\endgroup$

1 Answer 1

17
$\begingroup$

First a note: you are using the syntax for so-called "positive" coinductive types, which makes them look like inductive types, defined by "constructors". This has various problems: it's not well-justified semantically, and syntactically it breaks "subject reduction". Modern versions of Coq also support "negative" coinductive types, which look like record types rather than inductive types, defined by "fields", and are much better-behaved, so it is suggested to use those instead. See the reference manual.

As for the actual question, I believe one place that coinduction is valuable is when computational behavior matters. An infinite list represented by a function nat -> A is "random access": you can ask it for f n whenever you wish, and it doesn't in principle need to know anything about f k for k < n to compute f n. Whereas the elements of a coinductive stream must be computed in order. This certainly makes the function-representation easier to reason about.

However, if your "infinite list" has the property that in practice we have to compute all the f k for k < n in order to find f n, then working with the coinductive version respects this, and encourages the user to take account of it. Given a stream we can turn it into a function where f n is computed by pulling off n elements of the stream and returning the last one, but this performs a lot of computation if n is large, and if we call f a lot of times it could be very inefficient. A coinductive data representation encourages the writing of corecursive functions, which force us to deal with this kind of stepwise-computed list more efficiently.

Streams are arguably a bit too simple for this behavior to be clearly visible. I like to think of a general coinductive type as a "server", in line with Conor McBride's comment in Let's see how things unfold:

As a total programmer, I am often asked 'how do I implement a server as a program in your terminating language?', and I reply that I do not: a server is a coprogram in a language guaranteeing liveness.

An element of a coinductive "server type" represents the server in a particular state. When we call its destructor, we pass it some request from a client, and it returns a response to the client and also the new state of the server. By contrast, using the corresponding "functional" representation, in order to compute the response of the server to any query we would have to replay the entire history of interaction of all clients with the server up to that point. Clearly this is inefficient, and also a bad representation of how a real-world server actually works.

Coinductive types can also be valuable in situations where type dependency makes it tricky to even come up with a functional representation, and if you do come up with one it's more awkward. I'm most familiar with this in the case of homotopy theory and higher category theory. For instance, a "globular set" can be defined coinductively as a set $A$ together with a family of globular sets indexed by $A\times A$:

CoInductive GSet : Type := {
  carr : Type;
  hom : carr -> carr -> GSet;
}.

The corresponding functional representation is much less clear. This can be enhanced to deal with infinite-dimensional categories in a surprisingly clean way.

$\endgroup$
2
  • $\begingroup$ Last example: wow! Is there some text to read about this in more detail? I mean, how to actually work with it, and also whether one can similarly define other things like simplicial sets, etc? $\endgroup$ Apr 1 at 10:20
  • 1
    $\begingroup$ @მამუკაჯიბლაძე Not that I know of; that work in Coq was sort of stalled a while ago, but mainly because it wasn't clear whether it was the most practical version. Simplicial sets don't work, as far as anyone knows. And saying "infinite-dimensional categories" is maybe a bit misleading to people who actually know what that means -- it's not known how to get all the coherence, only finite fragments of it. $\endgroup$ Apr 1 at 15:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.