Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: functions on inductive types are coinductive?

Mike Shulman (Feb 17 2021 at 15:35):

One of the most basic inductive types is the type $\mathbb{N}$ of natural numbers. One of the most basic coinductive types is the type $\mathsf{Stream}(A)$ of streams (with values in some $A$, say). In fact we have $\mathsf{Stream}(A) \cong A^{\mathbb{N}}$; and moreover, the iterator $\mathsf{iter} : A \to (A\to A) \to (\mathbb{N}\to A)$ can easily be defined by replacing its codomain with streams: $\mathsf{iter}' : A \to (A\to A) \to \mathsf{Stream}(A)$ has copattern matches $\mathsf{head}(\mathsf{iter}'(a,g)) = a$ and $\mathsf{tail}(\mathsf{iter}'(a,g)) = \mathsf{iter}'(g(a),g)$. (This can be easily modified to derive the recursion principle as well; I don't know about the dependently typed induction principle.)

How generic is this? Is the type of functions out of some inductive type always equivalent to some coinductive type?

I know that for a fixed polynomial functor, the initial algebra sits inside the terminal coalgebra as the "well-founded" elements. I also know that all coinductive types can be constructed from the natural numbers. But neither of those seem to be quite what's going on here... are they?

Jacques Carette (Feb 18 2021 at 17:29):

Bumping this question up, as I'd like to know the answer to this as well!

Nathanael Arkor (Feb 18 2021 at 18:56):

I know that for a fixed polynomial functor, the initial algebra sits inside the terminal coalgebra as the "well-founded" elements. I also know that all coinductive types can be constructed from the natural numbers. But neither of those seem to be quite what's going on here... are they?

My impression was that this is exactly what's going on here. Every data type signature in the metatheory represents an inductive type and a coinductive type, as the initial algebra and terminal coalgebra. Assuming you have all inductive types, you also have coinductive types, because given any signature, you can form the coinductive type by considering functions $m : \mathbb N \to M$, where $m(n)$ represents the corresponding inductive type for the signature, truncated to height $n$. If you perform this construction with the signature corresponding to solely the $\mathsf{cons} : A \times \mathsf L(A) \to \mathsf L(A)$ operator (i.e. the signature of lists without $\mathsf{nil}$), you get the coinductive type of streams, represented concretely by a function type from $A^\mathbb N$.

Mike Shulman (Feb 18 2021 at 19:09):

That's all true, but I don't think it's what I described. If it is, can you explain how?

Nathanael Arkor (Feb 18 2021 at 19:14):

You mean that you don't think the coinduction principle generated by this method matches the one you defined? (Or even that the type for streams defined by this method doesn't match your type of streams?)

Nathanael Arkor (Feb 18 2021 at 19:19):

I had assumed that the characterisation of $\mathsf{Stream}(A)$ as a function type $A^{\mathbb N}$ was explained by the construction of coinductive types from inductive types, meaning that there was no a priori reason to expect that the characterisation might generalise to inductive types other than $\mathbb N$ (though whether it does is still an interesting question). But I didn't check the details, so maybe this turns out not to be the case.

Jacques Carette (Feb 18 2021 at 20:53):

$\mathsf{Stream}$ is quite special. It's really not clear that what works for it, generalizes. I think the question is, what's true in a reasonably general setting, about general inductive types and their 'corresponding' coinductive versions. Thus the 'generic' part of the original question.

Nathanael Arkor (Feb 18 2021 at 21:10):

@Jacques Carette: could you clarify which property of $\mathsf{Stream}$ you think is special, and won't be recovered with the existing construction of coinductive types as functions out of $\mathbb N$? I think I must simply be misunderstanding.

Jacques Carette (Feb 18 2021 at 21:21):

Take $\mathsf{Rose}$ trees as an example of a more complicated inductive type. I don't think the steps you go through to generalize from $\mathbb{N}$ to $\mathsf{Stream}(A)$ would go through smoothly.

Nathanael Arkor (Feb 18 2021 at 21:25):

I'm not trying to generalise $\mathbb N$ to another inductive type (which is to say, I'm not trying to answer the part of Mike's question about whether the construction does generalise to other inductive types). But I am saying that you will get a characterisation of (possibly infinite) rose trees as functions $X^{\mathbb N}$ for some type $X$, just like streams (though potentially with some restriction on the inhabitants of the type).

Mike Shulman (Feb 19 2021 at 01:58):

Nathanael Arkor said:

I'm not trying to generalise $\mathbb N$ to another inductive type (which is to say, I'm not trying to answer the part of Mike's question about whether the construction does generalise to other inductive types).

That is the only part of my question. (-:

Nathanael Arkor (Feb 19 2021 at 14:44):

Okay, I misunderstood; I thought you were asking how one can observe this relationship from a more general principle, but you are specifically interested in when the more general principle is "taking inductive types as exponents". (That is, it seems to me that your observation about streams can be understood from two different perspectives, that then generalise in different ways.)