[Agda] Recursive types for free?

[Anthony de Almeida Lopes]

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's been going on regarding
(co)inductive and all of the modern alternatives to Wadler's idea.

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't been keeping up.
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.

- Anthony
p.s. I just pulled up the miniAgda paper and I see they reference CIC^, I'll
have to check this out.


2011/5/29 Dan Doel <dan.doel at gmail.com>

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110529/44d4e5b7/attachment-0001.html