<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 &quot;Inductive and Coinductive types with Iteration and Recursion&quot; 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{ℓ ℓ&#39;} (A : Set ℓ)(R : Set ℓ&#39;) : Set (ℓ ⊔ ℓ&#39;) 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𝕊 : ∀ {ℓ ℓ&#39;} {A : Set ℓ} {B : Set ℓ&#39;} → (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>