[Agda] Recursive types for free?

[Thorsten Altenkirch]

Thank you, Dan for summarizing the issues so well.

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. 

Cheers,
Thorsten

On 29 May 2011, at 16:25, Dan Doel wrote:

> On Fri, May 27, 2011 at 5:49 PM, Anthony de Almeida Lopes
> <anthony.de.almeida.lopes at falsifiable.net> wrote:
>> Does anyone know why Wadler's "Recursive Types for Free" techniques are not
>> used more widely, for example in Agda? Is it because of the inefficiency of
>> execution?
> 
> There are additional issues.
> 
> First, the encoding requires impredicativity for it to be useful. If
> you don't have impredicativity, your datatypes end up being one level
> higher than they can eliminate over, so they can't eliminate over
> themselves. This would mean, for instance, that you can't define
> multiplication of naturals by iterated addition, you have to instead
> work with the underlying representation.
> 
> Another problem with impredicativity is that it only the lowest level
> of a universe hierarchy may be impredicative without introducing
> inconsistency (at best). So, you cannot use this encoding for any data
> structures you want to use together with types and such, if you want
> them to be able to compute with themselves, as mentioned.
> 
> A second problem is that you need to internalize parametricity to get
> strong induction principles for these encoded datatypes. I think this
> corresponds to weakly initial algebras vs. initial algebras, which
> Wadler talks about. However, how to incorporate parametricity into a
> theory is still a research question, and the only person I know making
> headway on it is Jean-Philipe Bernardy (who hangs out here
> occasionally).
> 
> A third problem is that there's no obvious way to do large elimination
> for this encoding. If natural numbers are:
> 
>  (R : Set) -> R -> (R -> R) -> R
> 
> then you cannot eliminate into Set. If you choose:
> 
>  (R : Set1) -> R -> (R -> R) -> R
> 
> then you need to have cumulativity for normal functioning, and you
> can't eliminate into Set2. Etc. And if you try:
> 
>  (i : Level) -> (R : Set i) -> R -> (R -> R) -> R
> 
> well, no one knows if it's safe to stick that sort of thing into Set
> impredicatively.
> 
> And if you are trying to get large elimination, here's some food for
> thought: strong, impredicative sums are known to be inconsistent. You
> probably can't have all three of the above together without
> introducing partiality.
> 
> So, there are a lot of issues before you even get to the fact that
> these encodings are asymptotically slower for a lot of uses.
> 
> -- Dan
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda