<br><div class="gmail_quote">On Tue, Oct 4, 2011 at 6:26 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
The only thing I am using sized types here is to establish a generic initial algebra for a functor F.<br>
<br>
If you believe that it makes sense for a functor F with functorial action<br>
<br>
map : {A B : Set} -> (A -> B) -> F A -> F B<br>
<br>
to have an initial algebra Mu F with<br>
<br>
introduction : inn : F (Mu F) -> Mu F<br>
elimination : iter : {A : Set} -> (F A -> A) -> Mu F -> A<br>
computation : iter s (inn t) = s (map (iter s) t)<br>
<br>
(I guess so far I am with the vast majority), and introduction is a *constructor*, then you can reconstruct my counterexample by setting F = co and there is no need for sized types whatsoever.<br>
<br>
Sized types come into the game because they are a means to persuade Agda that actually such initial algebras exist.<br>
<br>
So, I disagree (strongly) that sized types are to blame.<br>
<br>
The culprit is that co is treated as a functor. To fix the situation, we should no longer accept co as just a term of type Set -> Set (or the polymorphic version of it). If you look at the type of map for co,<br>
<br>
map : ∀ {A B : Set} → (A → B) → co A → co B<br>
map f a = ♯ f (♭ a)<br></blockquote><div><br></div><div>But the thing is, the only thing that lets you treat co as a functor is sized types. Termination of iter relies crucially on the fact that the map operation is applying it's first argument to things that are smaller than the second argument. That simply doesn't hold for map on co, which is revealed if you actually try to get it past the termination checker without resorting to sized types.</div>
<div><br></div><div>/ Ulf</div></div>