Coinductive Type

Idea

A coinductive type is the natural dual notion to inductive types. Rather than being the least fixed point closed under constructors, it is the greatest fixed-point closed under destructors.

They are can loosely be regarded as an extension of inductive types with the well-foundedness criteria lifted. From one perspective they can be seen as potentially non-terminating non-deterministic computational process.

Copatterns

See abel2013-copatterns.

$$\begin{array}{rlrlr}& \mathrm{State}SA& & =& S\to A\times S\\ & \mathrm{return}& & :& A\to \mathrm{State}SA\\ & \mathrm{return}as& & =& (a,s)\\ & m>>=k& & =& \text{let (a,s′)=m s in k a s′}\end{array}$$

Guarded Corecursion

See nakano2000-guarded-modality.