## Stream: general

### Topic: coinductive types

#### Kevin Buzzard (Feb 28 2018 at 09:07):

Can someone (@Simon Hudon ?) explain what a coinductive type is and, more specifically, whether a mathematician would ever need them?

#### Kevin Buzzard (Feb 28 2018 at 09:10):

As to the comments about them made here and linked to here, this might be another of those "perfect is the enemy of good" situations where we could either have Simon's "does the job to a certain extent", or the observation that one could do this much better if only we could find a Lean C++ hacker that just sat down and wrote a bunch of complicated working code, I would vote for Simon any day of the week.

#### Mario Carneiro (Feb 28 2018 at 09:14):

We don't need a C++ hacker for this one. I hope to implement the next version of (co)inductive types in lean

#### Sean Leather (Feb 28 2018 at 09:14):

@Kevin Buzzard: Non-wellfounded Set Theory might help.

#### Mario Carneiro (Feb 28 2018 at 09:15):

Mathematically, the theory of coinductive types is very elegantly dual to the theory of inductive types. A simple example of a coinductive type is the type of "possibly infinite lists", which is defined with the same clauses as list

#### Mario Carneiro (Feb 28 2018 at 09:16):

This is a type that contains the empty list, finite lists, as well as all infinite lists (a.k.a "streams")

#### Mario Carneiro (Feb 28 2018 at 09:19):

(These are often called llist or "lazy lists" for reasons to come.) The type llist has a cases_on, i.e. you can ask for any llist whether it is nil or a cons of an element and a llist, but there is no rec, because a llist is not well founded

#### Simon Hudon (Feb 28 2018 at 19:15):

There's also:
@Tim Carstens

terminal co-algebra of an endofunctor, instead of initial algebra of an endofunctor

if you want to look at them in terms of category theory

#### Simon Hudon (Feb 28 2018 at 19:18):

llist are easy enough without coinductive types but I imagine if you care about (possibly) infinite objects such as trees, it will be hard to study them without coinductive types.

I personally care about them mostly for modelling programs that do not terminate such as operating systems, controllers for pacemakers or any internet protocol

#### Tim Carstens (Feb 28 2018 at 19:20):

maybe bass-serre theory, aka doing group theory by way of group actions on (infinite) trees

#### Tim Carstens (Feb 28 2018 at 19:21):

i'm struggling to think up examples from pure math where coinductives would be handy

#### Tim Carstens (Feb 28 2018 at 19:21):

it's a big world out there though

Last updated: May 10 2021 at 00:31 UTC