<br><br><div class="gmail_quote">On Tue, Oct 4, 2011 at 1:25 PM, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@chalmers.se">nad@chalmers.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im">On 2011-10-04 12:26, Andreas Abel wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I'd like to open a new round of false-golfing, below is my entry to the<br>
tournament. My favorite target is Agda's coinduction mechanism.<br>
Partially it's flaws are known, but I cannot remember anyone presenting<br>
an outright proof of the absurdity.<br>
</blockquote>
<br></div>
Cool. However, you've only established that the present mechanism is<br>
incompatible with sized types (and the usual kind of semantics of data<br>
types, but this is not surprising). Can you do this without using sized<br>
types?<br></blockquote><div><br></div><div>I'm challenging the claim that sized types is not at fault. You don't _need_ sized</div><div>types to work with initial algebras. Here's the standard trick (specialising map</div>
<div>to iter):</div><div><br></div><div>module NoInf where</div><div> -- Just an ordinary datatype.</div><div> data ∞ (A : Set) : Set where</div><div> ♯_ : A → ∞ A</div><div> ♭ : {A : Set} → ∞ A → A</div><div> ♭ (♯ x) = x</div>
<div><br></div><div> data Mu : Set where</div><div> inn : ∞ Mu → Mu</div><div><br></div><div> -- Not using coinduction. Passes termination checking (as expected).</div><div> iter : ∀ {A : Set} → (∞ A → A) → Mu → A</div>
<div> map-iter : ∀ {A : Set} → (∞ A → A) → ∞ Mu → ∞ A</div><div><br></div><div> iter s (inn t) = s (map-iter s t)</div><div> map-iter f (♯ a) = ♯ iter f a</div><div><br></div><div>However, trying the same trick on the coinductive version doesn't pass termination/productivity:</div>
<div><br></div><div>module Inf where</div><div> open import Coinduction</div><div> data Mu : Set where</div><div> inn : ∞ Mu → Mu</div><div><br></div><div> -- Using coinduction. Doesn't pass (which it shouldn't).</div>
<div> iter : ∀ {A : Set} → (∞ A → A) → Mu → A</div><div> map-iter : ∀ {A : Set} → (∞ A → A) → ∞ Mu → ∞ A</div><div><br></div><div> iter s (inn t) = s (map-iter s t)</div><div> map-iter s a = ♯ iter s (♭ a)</div><div>
</div><div>The problem, as I see it, is that sized types doesn't work with coinduction, which we already knew.</div><div><br></div><div>/ Ulf</div></div>