One of the code sprints in the recent Agda meeting was to add coinductive
datatypes to Agda. The syntax is very simple, coinductive datatypes are
declared with the codata keyword instead of data and corecursive functions
use ~ instead of =. For instance:

codata Conat : Set where
  zero : Conat
  suc  : Conat -> Conat

inf : Conat
inf ~ suc inf

A corecursive function is only unfolded if it's result is demanded, i.e. if
something is trying to pattern match on the result. Corecursive functions
must be productive. The productivity checker is integrated with the
termination checker so it is possible to combine inductive and coinductive
types in interesting ways. For instance, we can define the type of stream
processors:

module StreamEating where

-- Infinite streams

codata Stream (A : Set) : Set where
  _::_ : A -> Stream A -> Stream A

-- A stream processor SP A B consumes elements of A and produces elements
of
B.
-- It can only consume a finite number of A's before producing a B.

mutual
  data SP (A B : Set) : Set where
    get : (A -> SP A B) -> SP A B
    <_> : SP' A B -> SP A B

  codata SP' (A B : Set) : Set where
    put : B -> SP A B -> SP' A B

eat : {A B : Set} -> SP A B -> Stream A -> Stream B
eat (get f)      (a :: as) ~ eat (f a) as
eat < put b sp > as        ~ b :: eat sp as


/ Ulf