[Agda] Recursive types for free?

[Dan Doel]

Well, another issue is that you may want to explain the natural
numbers using as weak a system as possible, and System F and beyond
are not that system. For one, it exposes your work to as few
philosophical objections as possible ("I don't accept
impredicativity"). For two, it makes your work as widely applicable as
possible.

System F and beyond is a bit like ZF set theory. It has very few
building blocks, but they are very powerful, and sufficient to make a
wide class of things you'd have to add to other theories. But the
building blocks are walking a thin line, and aren't always as elegant
as a direct presentation (although I like F better than ZF, of course
:)).

On Mon, May 30, 2011 at 1:43 PM, Anthony de Almeida Lopes
<anthony.de.almeida.lopes at falsifiable.net> wrote:
> 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
>
>