[Agda] Recursive types for free?

[Dan Doel]

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