Home
Reading
Searching
Subscribe
Sponsors
Statistics
Posting
Contact
Spam
Lists
Links
About
Hosting
Filtering
Features Download
Marketing
Archives
FAQ
Blog
 
Gmane
From: Ulf Norell <ulfn-AL6yYQ2bq2Cci/EUP2OQSw <at> public.gmane.org>
Subject: Agda goes coinductive
Newsgroups: gmane.comp.lang.agda
Date: Thursday 5th June 2008 11:04:42 UTC (over 8 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
 
CD: 3ms