<div dir="ltr">Hi, Andreas.<br><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Dec 16, 2013 at 1:36 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Aaron,<br>
<br>
this looks like a kind of negative translation to me:<br>
<br>
nu X. A * X<br>
--> forall R. ((nu X. A * X) -> R) -> R<br>
--> forall R. (mu X. (A -> R) + X) -> R<br>
<br></blockquote><div><br></div><div>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.</div>
<div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Might be a way to work with coinductive types. A bit of an inconvenience is that thus encoded coinductive types "up" the universe level.<br></blockquote><div><br></div><div>I see. That's a good point. </div>
<div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Here a small (and old) challenge: write the Hamming stream...<br></blockquote><div><br></div><div>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 </div>
<div><br></div><div><a href="http://www.cs.uiowa.edu/~astump/agda-hamming/">http://www.cs.uiowa.edu/~astump/agda-hamming/</a></div><div><br></div><div>I did not verify anything about it (except totality, of course). I tested it, though. :-)</div>
<div><br></div><div>Cheers,</div><div>Aaron</div><div><br></div><div>extract-min : {n : ℕ} → Vec ℕ (suc n) → Σ ℕ (λ m → Vec ℕ (suc m))<br>extract-min (x ∷ []) = , [ x ]<br>extract-min (x ∷ (x' ∷ xs)) with extract-min (x' ∷ xs)<br>
... | _ , (y ∷ ys) with x <ℕ y<br>... | true = _ , (x ∷ y ∷ ys)<br>... | false with x =ℕ y<br>... | true = _ , (x ∷ ys)<br>... | false = _ , (y ∷ x ∷ ys)<br><br>hammingh : {n : ℕ} → Vec ℕ (suc n) → 𝕊 ℕ<br>hammingh xs (observe-head f) with extract-min xs <br>
... | _ , (m ∷ _) = f m<br>hammingh xs (observe-tail o) with extract-min xs <br>... | _ , (m ∷ xs') = hammingh ((map (_*_ 2) xs) ++ (map (_*_ 3) xs) ++ (map (_*_ 5) xs) ++ xs') o<br><br>hamming = hammingh [ 1 ]<br>
</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Cheers,<br>
Andreas<div><div class="h5"><br>
<br>
On 16.12.2013 18:48, Aaron Stump wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5">
Dear Agda community,<br>
<br>
I am wondering why primitive notions (♭ ♯ ∞, or co-patterns) are used in<br>
Agda for coinductive types, instead of defining coinductive types based<br>
on an inductive types of observers. On this latter view, a piece of<br>
coinductive data is a function defined by recursion on the structure of<br>
an observer. The observer is just a finite request for information<br>
about the coinductively defined object. I understand this is similar in<br>
spirit to the co-patterns approach proposed by Andreas and Brigitte, but<br>
the point here is that this can all defined in basic Agda, with no<br>
special extensions for coinduction.<br>
<br>
Below I have an example of how this can be done for streams in Agda (I<br>
am using version 2.3.2). This is quite a pleasant way to work with<br>
coinductive data, with no new primitive notions beyond inductive<br>
datatypes and recursion. It also seems to support bisimulation (not<br>
included below). The paper "Inductive and Coinductive types with<br>
Iteration and Recursion" by H. Geuvers (available on Citeseer) has got a<br>
similar translation showing how coinduction can be simulated by<br>
induction only, though I did not absorb all the details yet.<br>
<br>
Probably there is some good reason this approach is not followed. I<br>
would be very curious to know why not.<br>
<br>
Cheers,<br>
Aaron<br>
<br>
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>
<br>
-- normalize to see the first 10 even numbers:<br>
test = take 10 (nats +𝕊ℕ nats)<br>
<br>
<br>
<br></div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br><span class=""><font color="#888888">
</font></span></blockquote><span class=""><font color="#888888">
<br>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
</font></span></blockquote></div><br></div></div>