Thank you, Dan. That was a better response than I had hoped for. I figured there had to be more to it since this publication has been in draft for years. This explains the more recent research that&#39;s been going on regarding (co)inductive and all of the modern alternatives to Wadler&#39;s idea. <div>
<br><div>Although I am not done, I began reading the draft of the completed CIC^. Has anyone else seen that? I saw Andreas Abel did a presentation on sized types in Agda quite a while ago and I think I remember work on the subject going into miniAgda but I haven&#39;t been keeping up.<div>
Anyway, thanks again for the response, these type of things have been on my mind quite a lot recently :) I really like the idea of getting away from an external termination checker and still preserving strong normalisation.</div>
<div><br></div><div>- Anthony</div><div>p.s. I just pulled up the miniAgda paper and I see they reference CIC^, I&#39;ll have to check this out.</div><div><br><br><div class="gmail_quote">2011/5/29 Dan Doel <span dir="ltr">&lt;<a href="mailto:dan.doel@gmail.com">dan.doel@gmail.com</a>&gt;</span><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><div><div></div><div class="h5">On Fri, May 27, 2011 at 5:49 PM, Anthony de Almeida Lopes<br>
&lt;<a href="mailto:anthony.de.almeida.lopes@falsifiable.net">anthony.de.almeida.lopes@falsifiable.net</a>&gt; wrote:<br>
&gt; Does anyone know why Wadler&#39;s &quot;Recursive Types for Free&quot; techniques are not<br>
&gt; used more widely, for example in Agda? Is it because of the inefficiency of<br>
&gt; execution?<br>
<br>
</div></div>There are additional issues.<br>
<br>
First, the encoding requires impredicativity for it to be useful. If<br>
you don&#39;t have impredicativity, your datatypes end up being one level<br>
higher than they can eliminate over, so they can&#39;t eliminate over<br>
themselves. This would mean, for instance, that you can&#39;t define<br>
multiplication of naturals by iterated addition, you have to instead<br>
work with the underlying representation.<br>
<br>
Another problem with impredicativity is that it only the lowest level<br>
of a universe hierarchy may be impredicative without introducing<br>
inconsistency (at best). So, you cannot use this encoding for any data<br>
structures you want to use together with types and such, if you want<br>
them to be able to compute with themselves, as mentioned.<br>
<br>
A second problem is that you need to internalize parametricity to get<br>
strong induction principles for these encoded datatypes. I think this<br>
corresponds to weakly initial algebras vs. initial algebras, which<br>
Wadler talks about. However, how to incorporate parametricity into a<br>
theory is still a research question, and the only person I know making<br>
headway on it is Jean-Philipe Bernardy (who hangs out here<br>
occasionally).<br>
<br>
A third problem is that there&#39;s no obvious way to do large elimination<br>
for this encoding. If natural numbers are:<br>
<br>
  (R : Set) -&gt; R -&gt; (R -&gt; R) -&gt; R<br>
<br>
then you cannot eliminate into Set. If you choose:<br>
<br>
  (R : Set1) -&gt; R -&gt; (R -&gt; R) -&gt; R<br>
<br>
then you need to have cumulativity for normal functioning, and you<br>
can&#39;t eliminate into Set2. Etc. And if you try:<br>
<br>
  (i : Level) -&gt; (R : Set i) -&gt; R -&gt; (R -&gt; R) -&gt; R<br>
<br>
well, no one knows if it&#39;s safe to stick that sort of thing into Set<br>
impredicatively.<br>
<br>
And if you are trying to get large elimination, here&#39;s some food for<br>
thought: strong, impredicative sums are known to be inconsistent. You<br>
probably can&#39;t have all three of the above together without<br>
introducing partiality.<br>
<br>
So, there are a lot of issues before you even get to the fact that<br>
these encodings are asymptotically slower for a lot of uses.<br>
<br>
-- Dan<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div></div></div>