<br><br><div class="gmail_quote">On Tue, Oct 4, 2011 at 1:25 PM, Nils Anders Danielsson <span dir="ltr">&lt;<a href="mailto:nad@chalmers.se">nad@chalmers.se</a>&gt;</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&#39;d like to open a new round of false-golfing, below is my entry to the<br>
tournament.  My favorite target is Agda&#39;s coinduction mechanism.<br>
Partially it&#39;s flaws are known, but I cannot remember anyone presenting<br>
an outright proof of the absurdity.<br>
</blockquote>
<br></div>
Cool. However, you&#39;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&#39;m challenging the claim that sized types is not at fault. You don&#39;t _need_ sized</div><div>types to work with initial algebras. Here&#39;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&#39;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&#39;t pass (which it shouldn&#39;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&#39;t work with coinduction, which we already knew.</div><div><br></div><div>/ Ulf</div></div>