[Agda] Agda's coinduction incompatible with initial algebras

[Dan Doel]

On Thu, Oct 6, 2011 at 4:47 PM, Peter Hancock <hancock at spamcop.net> wrote:
> What does strictly positive mean? Does it mean: isomorphic
> to a coproduct of hom-functors of some kind, like a container?

Strictly positive is also often referred to, I think, as polynomial.
In the type:

    A -> B

A is in the negative position, and B is in the positive position.
Double negation results in a positive, but doubly negated positions
are not strictly positive. And this of course generalizes to pi types.

Agda's datatypes assert that all functors whose actions are strictly
positive have initial algebras.  Accepting all positive types would
include initial algebras of functors like:

    DP X = (X -> 2) -> 2

but there is no classical set that is isomorphic to its own double
exponential like that. However, in an anti-classical constructive
mathematics, one could have such things. For instance, the naturals
may be an example of such a set:

    http://math.andrej.com/2009/10/12/constructive-gem-double-exponentials/

However, fiddling with this a bit, it seems the termination checker
can't really even handle the eliminator of such a type. The
definition:

    cata : ∀{R Z} → (K Z R → R) → P Z → R
    cata alg (roll x) = alg (λ k → x (λ y → k (cata alg y)))

is pink, since it doesn't recognize y as smaller than roll x. So it's
not merely a matter of extending the positivity checker.

> Do you think IR-functors, with large decode ("D") types, are
> positive, strictly or otherwise?
> They don't have a Sigma-Pi normal form.

Induction-recursion is not (from what I've read) justified by functors
over the category of types, but by functors over a related category.
But their actions are supposed to be strictly positive there, I
believe.

-- Dan