<br><br><div class="gmail_quote">On Tue, Oct 4, 2011 at 11:18 PM, Dan Doel <span dir="ltr"><<a href="mailto:dan.doel@gmail.com">dan.doel@gmail.com</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 Tue, Oct 4, 2011 at 2:07 PM, Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>> wrote:<br>
> But the principle of sized types can also be applied to coinduction, under<br>
> the interpretation of "size" as "depth", i.e., number of guarding<br>
> constructors. Corecursion is sound if it increases the guardedness of the<br>
> result in the body surrounding the recursive call (rather than increasing<br>
> the size of the function argument as in the recursion case).<br>
><br>
> Yet that does not happen here.<br>
<br>
</div>It doesn't appear to happen anywhere to me. The sized type checker<br>
doesn't seem to recognize Agda's coinductive definitions at all<br>
(currently). You just get whatever is better at the time. If you write<br>
an obviously guarded corecursive definition, it's accepted by the<br>
guardedness checker. If you write a size-decreasing function, it's<br>
also accepted, even though the type may be coinductive due to the<br>
presence of the built-in.<br>
<br>
So, one could probably argue that the bug is in assuming that Mu F is<br>
an initial algebra without knowing what F is. Knowing only that it is<br>
a functor is not enough in Agda. You need to know whether or not it's<br>
a magic functor that turns things into codata.<br></blockquote><div><br></div><div>This. The problem isn't allowing co to be a functor, you can do this with</div><div>only sanctioned uses of co (only applied to recursive occurrences of the</div>
<div>type(s) we are defining):</div><div><br></div><div><div> -- Streams of alternating ⊤ and A</div><div> data Stream′ A : Set</div><div> data Stream A : Set</div><div><br></div><div> data Stream′ A where</div><div>
_∷_ : A → co (Stream A) → Stream′ A</div>
<div> data Stream A where</div><div> _∷_ : ⊤ → co (Stream′ A) → Stream A</div><div><br></div><div> map : ∀ {A B : Set} → (A → B) → Stream A → Stream B</div><div> map′ : ∀ {A B : Set} → (A → B) → Stream′ A → Stream′ B</div>
<div> map f (_ ∷ xs) = _ ∷ ♯ map′ f (♭ xs)</div><div> map′ f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)</div><div><br></div><div> boos : Stream (Mu Stream ∞)</div><div> boo : Mu Stream ∞</div><div> boos = _ ∷ (♯ (boo ∷ ♯ boos))</div>
<div> boo = inn boos</div><div><br></div><div> hd′ : ∀ {A} → Stream′ A → A</div><div> hd′ (x ∷ _) = x</div><div><br></div><div> hd : ∀ {A} → Stream A → A</div><div> hd (_ ∷ xs) = hd′ (♭ xs)</div><div><br></div><div>
false : ⊥</div>
<div> false = iter map hd boo</div></div><div><br></div><div>Basically, the way things currently work in Agda, Mu will be</div><div>inductive or coinductive depending on the choice of F, but the</div><div>sized types machinery treats it as always inductive.</div>
<div><br></div><div>/ Ulf</div></div>