[Agda] Recursive types for free?

[Anthony de Almeida Lopes]

Thorsten, if by a good idea you mean intuitiveness, readaibility and ease of
manipulation, I would agree that the alternatives clearly make more sense.

2011/5/30 Thorsten Altenkirch <txa at cs.nott.ac.uk>

> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110530/2c362fe6/attachment.html