<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">&lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt;</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>
  --&gt; forall R. ((nu X. A * X) -&gt; R) -&gt; R<br>
  --&gt; forall R. (mu X. (A -&gt; R) + X) -&gt; 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&#39;s why I was surprised I hadn&#39;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 &quot;up&quot; the universe level.<br></blockquote><div><br></div><div>I see.  That&#39;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&#39;s Bachelor&#39;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&#39; ∷ xs)) with extract-min (x&#39; ∷ xs)<br>
... | _ , (y ∷ ys) with x &lt;ℕ 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&#39;) = hammingh ((map (_*_ 2) xs) ++ (map (_*_ 3) xs) ++ (map (_*_ 5) xs) ++ xs&#39;) 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 &quot;Inductive and Coinductive types with<br>
Iteration and Recursion&quot; 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{ℓ ℓ&#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>
<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  &lt;&gt;&lt;      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>