[Agda] Agda goes coinductive
Ulf Norell
ulfn at cs.chalmers.se
Thu Jun 5 13:04:42 CEST 2008
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080605/b55bf2bd/attachment.html
More information about the Agda
mailing list