[Agda] Agda goes coinductive

[Edward Kmett]

Yes!! Thank you, thank you, thank you!

This is what I've been waiting for to be able to actually start using
Agda for real.

I started to port some category theory to Agda, but the lack of
coinductive types prevented me from getting far.

Well, that and a lack of universe polymorphism, but this takes me a
long way and type-in-type can bandaid the latter.

-Edward Kmett

On Thu, Jun 5, 2008 at 7:04 AM, Ulf Norell <ulfn at cs.chalmers.se> wrote:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>