[Agda] Agda's coinduction incompatible with initial algebras

[Dan Doel]

On Tue, Oct 4, 2011 at 2:07 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> But the principle of sized types can also be applied to coinduction, under
> the interpretation of "size" as "depth", i.e., number of guarding
> constructors.  Corecursion is sound if it increases the guardedness of the
> result in the body surrounding the recursive call (rather than increasing
> the size of the function argument as in the recursion case).
>
> Yet that does not happen here.

It doesn't appear to happen anywhere to me. The sized type checker
doesn't seem to recognize Agda's coinductive definitions at all
(currently). You just get whatever is better at the time. If you write
an obviously guarded corecursive definition, it's accepted by the
guardedness checker. If you write a size-decreasing function, it's
also accepted, even though the type may be coinductive due to the
presence of the built-in.

So, one could probably argue that the bug is in assuming that Mu F is
an initial algebra without knowing what F is. Knowing only that it is
a functor is not enough in Agda. You need to know whether or not it's
a magic functor that turns things into codata.

I'm not particularly happy that things work that way. But I don't
think it's possible to exhibit this without using the sized-type
checker to assume things are data when they may not be (that is, the
checker can't know whether it should be doing termination or
guardedness checking without knowing what F is, but it assumes
termination). Your argument for your various definitions is how things
work in the literature, and how I'd like things to work in Agda, but
it is not how things do work, and so I don't think it's inconceivable
to suggest the error is in the sized types checker's not appropriately
handling Agda's conventions.

> Martin Escardo wrote:
> It seems that you have shown that this extension of Agda with co-inductive types
> is actually an algebraicly compact extension of Agda.
> ...
> (I am glad that I didn't define the co-natural numbers by co-induction in my Agda
> proof of their omniscience (I was tempted to). :-) )

I'm skeptical that it's possible to recreate this example without
sized types enabled and used. So unless you were planning on using
both coinduction and sized types, you'd probably have been safe.

For instance, it's possible to write a type of codes for
strictly-positive functors, and index a Mu type by those. If you try
to include the magic coinductive 'functor' in your codes, you will be
unable to construct the catamorphism without sized types, whereas
without such a code, it is possible (though, not fun).

-- Dan