Abstract
The3rd lecture introduced inductive types and predicates, a general mechanism for defining and reasoning about finite data structures. How can we do the same for potentially infinite data structures, such asstreams or graphs seen as infinite trees ? In such cases, we speak of coinductive types and predicates.
In the classical ensemblist presentation, coinductive types correspond to larger fixed points of increasing operators, while inductive types are smaller fixed points. Type theory follows a different presentation, in terms of well-founded trees (any branch is finite) for the inductive case and possibly ill-founded trees (with infinite branches) for the coinductive case. A guard criterion guarantees the correct formation of definitions: structural recursions for the inductive case, productive corecursions for the coinductive case.
A more modern, algebraic presentation characterizes inductive types as generated by their constructors(nil and cons for lists), and coinductive types as generated by their observations (projections)(head and tail for streams). This presentation led to an elegant programming style based on cofiltration and copatterns (Abel et al., 2013).
The lecture presented two of the many applications of coinduction : the partiality monad (Capretta, 2005), which allows us to define general type-theoretic recursions and reason coinductively about their termination or divergence, and the modeling of reactive programming using causal functions on data streams.
