[Agda] defining coinductive types

[Aaron Stump]

Hi, Andreas.


On Mon, Dec 16, 2013 at 1:36 PM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:

> 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
>
>
Exactly!  That is how I found this.  But as I said in my earlier email,
this approach already seems to be known.  It looks very similar to a
translation in the Geuvers paper I mentioned.  That's why I was surprised I
hadn't heard more about this approach, given the recent research interest
in coinduction.


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

I see.  That's a good point.


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

Great!  I did this now, with some help from van der Weegen's Bachelor's
Thesis (I see you and Nils have both done this example, using different
methods).  I am not sure you will be happy with my implementation, as it
does not seem very fancy: I just use an accumulator to build up the list of
the first few elements, while recursing through the observer.  The main
functions are shown below.  Complete source files at

http://www.cs.uiowa.edu/~astump/agda-hamming/

I did not verify anything about it (except totality, of course).  I tested
it, though.  :-)

Cheers,
Aaron

extract-min : {n : ℕ} → Vec ℕ (suc n) → Σ ℕ (λ m → Vec ℕ (suc m))
extract-min (x ∷ []) = , [ x ]
extract-min (x ∷ (x' ∷ xs)) with extract-min (x' ∷ xs)
... | _ , (y ∷ ys) with x <ℕ y
... | true = _ , (x ∷ y ∷ ys)
... | false with x =ℕ y
... | true = _ , (x ∷ ys)
... | false = _ , (y ∷ x ∷ ys)

hammingh : {n : ℕ} → Vec ℕ (suc n) → 𝕊 ℕ
hammingh xs (observe-head f) with extract-min xs
... | _ , (m ∷ _) = f m
hammingh xs (observe-tail o) with extract-min xs
... | _ , (m ∷ xs') = hammingh ((map (_*_ 2) xs) ++ (map (_*_ 3) xs) ++
(map (_*_ 5) xs) ++ xs') o

hamming = hammingh [ 1 ]


>
> 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/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131216/59f3f99b/attachment-0001.html