[Agda] defining coinductive types

[Aaron Stump]

Dear Agda community,

I am wondering why primitive notions (♭ ♯ ∞, or co-patterns) are used in
Agda for coinductive types, instead of defining coinductive types based on
an inductive types of observers.  On this latter view, a piece of
coinductive data is a function defined by recursion on the structure of an
observer.  The observer is just a finite request for information about the
coinductively defined object.  I understand this is similar in spirit to
the co-patterns approach proposed by Andreas and Brigitte, but the point
here is that this can all defined in basic Agda, with no special extensions
for coinduction.

Below I have an example of how this can be done for streams in Agda (I am
using version 2.3.2).  This is quite a pleasant way to work with
coinductive data, with no new primitive notions beyond inductive datatypes
and recursion.  It also seems to support bisimulation (not included below).
 The paper "Inductive and Coinductive types with Iteration and Recursion"
by H. Geuvers (available on Citeseer) has got a similar translation showing
how coinduction can be simulated by induction only, though I did not absorb
all the details yet.

Probably there is some good reason this approach is not followed.  I would
be very curious to know why not.

Cheers,
Aaron

module stdlib-alt-stream where

open import Level hiding (suc)
open import Data.List hiding (zipWith ; take)
open import Data.Nat hiding (_⊔_)

----------------------------------------------------------------------
-- datatypes
----------------------------------------------------------------------

data 𝕊-observer{ℓ ℓ'} (A : Set ℓ)(R : Set ℓ') : Set (ℓ ⊔ ℓ') where
observe-head : (A → R) → 𝕊-observer A R
observe-tail : 𝕊-observer A R → 𝕊-observer A R

-- streams map stream observers to results
𝕊 : ∀{ℓ}→ Set ℓ → Set (Level.suc ℓ)
𝕊{ℓ} A = ∀ {R : Set ℓ} → 𝕊-observer A R → R

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

infixr 5 _+𝕊ℕ_

----------------------------------------------------------------------
-- operations
----------------------------------------------------------------------

head : ∀{ℓ}{A : Set ℓ} → 𝕊 A → A
head s = s (observe-head (λ x → x))

tail : ∀{ℓ}{A : Set ℓ} → 𝕊 A → 𝕊 A
tail s o = s (observe-tail o)

repeat : ∀{ℓ}{A : Set ℓ} → (a : A) → 𝕊 A
repeat a (observe-head f) = f a
repeat a (observe-tail o) = repeat a o

nats-from : ℕ → 𝕊 ℕ
nats-from n (observe-head f) = f n
nats-from n (observe-tail o) = nats-from (n + 1) o

nats = nats-from 0

map𝕊 : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → (A → B) → 𝕊 A → 𝕊 B
map𝕊 f xs (observe-head g) = g (f (head xs))
map𝕊 f xs (observe-tail o) = (map𝕊 f (tail xs) o)

zipWith : ∀ {ℓ} {A B C : Set ℓ} → (A → B → C) → 𝕊 A → 𝕊 B → 𝕊 C
zipWith _f_ xs ys (observe-head g) = g ((head xs) f (head ys))
zipWith _f_ xs ys (observe-tail o) = zipWith _f_ (tail xs) (tail ys) o

_+𝕊ℕ_ : 𝕊 ℕ → 𝕊 ℕ → 𝕊 ℕ
_+𝕊ℕ_ = zipWith _+_

take : ∀{ℓ}{A : Set ℓ} → ℕ → 𝕊 A → List A
take 0 xs = []
take (suc n) xs = (head xs) ∷ (take n (tail xs))

-- normalize to see the first 10 even numbers:
test = take 10 (nats +𝕊ℕ nats)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131216/3b7a7abc/attachment.html