<br><div class="gmail_quote">On Tue, Oct 4, 2011 at 6:26 PM, Andreas Abel <span dir="ltr">&lt;<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>&gt;</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} -&gt; (A -&gt; B) -&gt; F A -&gt; F B<br>
<br>
to have an initial algebra Mu F with<br>
<br>
  introduction :  inn  : F (Mu F) -&gt; Mu F<br>
  elimination  :  iter : {A : Set} -&gt; (F A -&gt; A) -&gt; Mu F -&gt; 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 -&gt; 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&#39;s first argument to things that are smaller than the second argument. That simply doesn&#39;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>