Thorsten, if by a good idea you mean intuitiveness, readaibility and ease of manipulation, I would agree that the alternatives clearly make more sense.<br><br><div class="gmail_quote">2011/5/30 Thorsten Altenkirch <span dir="ltr"><<a href="mailto:txa@cs.nott.ac.uk">txa@cs.nott.ac.uk</a>></span><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">Thank you, Dan for summarizing the issues so well.<br>
<br>
One additional remark on a foundational level that it is not clear wether it is a good idea to "explain" e.g. the natural numbers via higher order functions and impredicative quantification.<br>
<br>
Cheers,<br>
<font color="#888888">Thorsten<br>
</font><div><div></div><div class="h5"><br>
On 29 May 2011, at 16:25, Dan Doel wrote:<br>
<br>
> On Fri, May 27, 2011 at 5:49 PM, Anthony de Almeida Lopes<br>
> <<a href="mailto:anthony.de.almeida.lopes@falsifiable.net">anthony.de.almeida.lopes@falsifiable.net</a>> wrote:<br>
>> Does anyone know why Wadler's "Recursive Types for Free" techniques are not<br>
>> used more widely, for example in Agda? Is it because of the inefficiency of<br>
>> execution?<br>
><br>
> There are additional issues.<br>
><br>
> First, the encoding requires impredicativity for it to be useful. If<br>
> you don't have impredicativity, your datatypes end up being one level<br>
> higher than they can eliminate over, so they can't eliminate over<br>
> themselves. This would mean, for instance, that you can'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's no obvious way to do large elimination<br>
> for this encoding. If natural numbers are:<br>
><br>
> (R : Set) -> R -> (R -> R) -> R<br>
><br>
> then you cannot eliminate into Set. If you choose:<br>
><br>
> (R : Set1) -> R -> (R -> R) -> R<br>
><br>
> then you need to have cumulativity for normal functioning, and you<br>
> can't eliminate into Set2. Etc. And if you try:<br>
><br>
> (i : Level) -> (R : Set i) -> R -> (R -> R) -> R<br>
><br>
> well, no one knows if it's safe to stick that sort of thing into Set<br>
> impredicatively.<br>
><br>
> And if you are trying to get large elimination, here's some food for<br>
> thought: strong, impredicative sums are known to be inconsistent. You<br>
> probably can'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>
<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>
</div></div></blockquote></div><br>