coinductive types

Stream: general

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

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]

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]

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

[Tim Carstens]

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

[Tim Carstens]

it's a big world out there though