Subject: Agda goes coinductive Newsgroups: gmane.comp.lang.agda Date: Thursday 5th June 2008 11:04:42 UTC (over 10 years ago) 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 |
|||