<div dir="ltr"><div>Dear Agda community,<br></div><div><br></div><div>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. </div>
<div><br></div><div>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.</div>
<div><br></div><div>Probably there is some good reason this approach is not followed. I would be very curious to know why not.</div><div><br></div><div>Cheers,</div><div>Aaron </div><div><br></div><div>module stdlib-alt-stream where<br>
<br>open import Level hiding (suc)<br>open import Data.List hiding (zipWith ; take)<br>open import Data.Nat hiding (_⊔_)<br><br>----------------------------------------------------------------------<br>-- datatypes<br>----------------------------------------------------------------------<br>
<br>data 𝕊-observer{ℓ ℓ'} (A : Set ℓ)(R : Set ℓ') : Set (ℓ ⊔ ℓ') where<br> observe-head : (A → R) → 𝕊-observer A R<br> observe-tail : 𝕊-observer A R → 𝕊-observer A R<br><br>-- streams map stream observers to results<br>
𝕊 : ∀{ℓ}→ Set ℓ → Set (Level.suc ℓ)<br>𝕊{ℓ} A = ∀ {R : Set ℓ} → 𝕊-observer A R → R<br><br>----------------------------------------------------------------------<br>-- syntax<br>----------------------------------------------------------------------<br>
<br>infixr 5 _+𝕊ℕ_<br><br>----------------------------------------------------------------------<br>-- operations<br>----------------------------------------------------------------------<br><br>head : ∀{ℓ}{A : Set ℓ} → 𝕊 A → A<br>
head s = s (observe-head (λ x → x))<br><br>tail : ∀{ℓ}{A : Set ℓ} → 𝕊 A → 𝕊 A<br>tail s o = s (observe-tail o)<br><br>repeat : ∀{ℓ}{A : Set ℓ} → (a : A) → 𝕊 A<br>repeat a (observe-head f) = f a<br>repeat a (observe-tail o) = repeat a o<br>
<br>nats-from : ℕ → 𝕊 ℕ<br>nats-from n (observe-head f) = f n<br>nats-from n (observe-tail o) = nats-from (n + 1) o<br><br>nats = nats-from 0<br><br>map𝕊 : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → (A → B) → 𝕊 A → 𝕊 B<br>
map𝕊 f xs (observe-head g) = g (f (head xs))<br>map𝕊 f xs (observe-tail o) = (map𝕊 f (tail xs) o)<br><br>zipWith : ∀ {ℓ} {A B C : Set ℓ} → (A → B → C) → 𝕊 A → 𝕊 B → 𝕊 C<br>zipWith _f_ xs ys (observe-head g) = g ((head xs) f (head ys))<br>
zipWith _f_ xs ys (observe-tail o) = zipWith _f_ (tail xs) (tail ys) o<br><br>_+𝕊ℕ_ : 𝕊 ℕ → 𝕊 ℕ → 𝕊 ℕ<br>_+𝕊ℕ_ = zipWith _+_ <br><br>take : ∀{ℓ}{A : Set ℓ} → ℕ → 𝕊 A → List A<br>take 0 xs = []<br>take (suc n) xs = (head xs) ∷ (take n (tail xs))<br>
</div><div><br></div><div>-- normalize to see the first 10 even numbers:<br>test = take 10 (nats +𝕊ℕ nats)<br><br></div></div>