<div dir="ltr"><div>Thanks, Thierry, for the response about normalization with positive recursive types.</div><div><br></div><div>One more update on the "sized observers" approach I am proposing: here is the Hamming stream example, written in the same compact style. This was harder to do, because of the need to reason about the depth of observations. (Note that I'm writing this with my own library, not the standard library.) The code for merge is as expected, though the type is interesting. But then the code for hamming is written in the desired style. </div>
<div><br></div><div>merge : {n m : ℕ} → 𝕊 ℕ n → 𝕊 ℕ m → {k : ℕ} → k ≤ min n m ≡ tt → 𝕊 ℕ k<br><br>hamming : {n : ℕ} → 𝕊 ℕ n<br>hamming (ohead f) = f 1<br>hamming {suc n} (otail o) = <br> merge (map𝕊 (_*_ 2) (hamming{n}))<br>
(merge (map𝕊 (_*_ 3) (hamming{n}))<br> (map𝕊 (_*_ 5) (hamming{n})) <br> {min n n} (≤-refl (min n n))) lem o<br> where lem : n ≤ min n (min n n) ≡ tt<br> lem rewrite min-same n | <-irrefl n | ≤-refl n = refl<br>
</div><div><br></div><div>It seems to run fast, too. If you want to see all the details, you can find dev/hamming-stream.agda and lib/ in my svn repo:</div><div><br></div><div><a href="https://svn.divms.uiowa.edu/repos/clc/class/111-spring14">https://svn.divms.uiowa.edu/repos/clc/class/111-spring14</a></div>
<div><br></div><div>Use username "guest" and password "guest" if needed.</div><div><br></div><div>Cheers,</div><div>Aaron</div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">
On Wed, Dec 18, 2013 at 11:31 AM, Thierry Coquand <span dir="ltr"><<a href="mailto:Thierry.Coquand@cse.gu.se" target="_blank">Thierry.Coquand@cse.gu.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div style="word-wrap:break-word">
<div><br>
</div>
<div> At least in an impredicative metatheory, the usual normalization argument should extend</div>
<div>to the addition of such positive recursive types in Agda (using Tarski's fixed point theorem</div>
<div>to define the computability at these types).</div>
<div><br>
</div>
<div> Best regards,</div>
<div> Thierry</div>
<div><br>
</div>
PS: This would be however incompatible with the addition of an impredicative universe U,
<div>
<div>since one can then form</div>
<div><br>
</div>
<div> R = mu X. (X-> U) -> U</div>
<div><br>
</div>
<div>and derive a contradiction from this following Reynolds' proof that there is no set theoretical</div>
<div>model of system F. </div>
<div><br>
</div>
<div><div><div class="h5">
<div>On Dec 18, 2013, at 6:22 PM, Aaron Stump wrote:</div>
<br>
</div></div><blockquote type="cite"><div><div class="h5">
<div dir="ltr">
<div>Dear Wojtek,<br>
</div>
<div><br>
</div>
<div>Yes, I know about this example for recursive types which contain negative occurrences of the recursively defined type. But I am asking about positive but not strictly positive recursive types. An example is a type like the one Nils mentioned:</div>
<div><br>
</div>
<div>μA.∀R. (μX. (A → R) + X) → R</div>
<div><br>
</div>
<div>Here, the type variable A occurs to the left of an even number of arrows. This makes it positive (the even number of negations cancel out), but not strictly positive.</div>
<div><br>
</div>
<div>Cheers,</div>
<div>Aaron</div>
<div><br>
</div>
<div><br>
</div>
</div>
<div class="gmail_extra"><br>
<br>
<div class="gmail_quote">On Wed, Dec 18, 2013 at 11:14 AM, Wojciech Jedynak <span dir="ltr">
<<a href="mailto:wjedynak@gmail.com" target="_blank">wjedynak@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hello,<br>
<div><br>
> Ok, I see. Is it known that supporting non-strictly positive types would<br>
> have bad consequences in Agda? Not that I am suggesting it -- I am just<br>
> curious about what might be possible.<br>
<br>
</div>
Yes, it's possible to write a non-terminating expression using such a<br>
type. For instance, take a look here:<br>
<<a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.BadInHaskell" target="_blank">http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.BadInHaskell</a>><br>
<br>
Best,<br>
Wojtek<br>
</blockquote>
</div>
<br>
</div></div></div><div class="im">
_______________________________________________<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>
</div></blockquote>
</div>
<br>
</div>
</div>
</blockquote></div><br></div>