[Agda] defining coinductive types

[Andreas Abel]

Hi Aaron,

this looks like a kind of negative translation to me:

       nu X. A * X
   --> forall R. ((nu X. A * X) -> R) -> R
   --> forall R. (mu X. (A -> R) + X) -> R

Might be a way to work with coinductive types.  A bit of an 
inconvenience is that thus encoded coinductive types "up" the universe 
level.

Here a small (and old) challenge:  write the Hamming stream...

Cheers,
Andreas

On 16.12.2013 18:48, Aaron Stump wrote:
> 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)
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/