[Agda] Agda's coinduction incompatible with initial algebras

[Dan Doel]

On Wed, Oct 5, 2011 at 12:13 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> Not in Agda.  Try MiniAgda.  Or read the literature.

Oh, okay.

> The (non-sized) termination and guardedness checker of Agda is not
> compositional.  Ulf has demonstrated how to do initial algebras in current
> Agda:  You need to define iter and a specialized version of map mutually.
>  Compositionally is precious, not only to write better code, but also when
> you try to give a formal semantics of your language.

Yeah, I've certainly experienced the limitations of the current
checker---it's even more obvious when you try to write corecursive
programs, I think.

> Well, then things should change.

Okay. I think I'm on record as saying I think we should have
coinductive families that look a lot like records do now. But a fair
number of people seemed to want to stick with the current constructor
+ delay/box approach.

> As long as F is (strictly) positive, I can form an initial algebra.  I do
> not want to care about more.  F is positive as witnessed by map. Ralph
> Matthes has shown that every monotone F has a least fixed point, the
> existence of map is enough.  (Search for "monotone inductive types").

I don't think this is true if you want a (typical) set theoretic
semantics. Fixed points of functors like:

    K R A = (A -> R) -> R

only exist in categories of domains and the like as I recall (and my
skimming of Matthes' paper didn't suggest any different). Assuming
anyone cares about that.

I'd probably be interested in having these, though. I've seen papers
on induction principles for, say, hyperfunctions (Hyper A B ~ (Hyper A
B -> A) -> B), and I've not really seen anything wrong with them
besides, "they're not set theoretic." And it'd end a long-standing
wonder of mine about 'why can we only do strictly positive types?' The
standard line you find in the literature is 'negative types are bad,'
but that doesn't address non-strictly positive types. It may make Agda
anti-classical in some way, though.

> Well, what exactly Agda's conventions are, is under dispute.

I don't think what they _are_ is in dispute. Agda clearly implements
codata using the weird Pi-Sigma-like boxing stuff. Which, to my
knowledge, has no heavy theoretical groundwork (as I think Pi-Sigma is
geared toward being an efficiently implementable intermediate
language, not a rigorous categorical justification or anything).

I'll gladly dispute whether this is what Agda _should_ do, though. And
as I said, I'd like coinductive families that look categorically
motivated and such.

> Thorsten Altenkirch wrote:
>
> Sized types are one solution but I am not sure they are the best one. I'd hope
> that we can extend the current termination checker to deal with nested mu-nu.

nu-mu vs. mu-nu isn't really the only problem with the current
checker. I get more day-to-day grief from dealing with the lack of
factoring it affords. It sometimes even gets in the way of simple
conveniences that would be nice to lift from Haskell, like ∘ or $.
It's not uncommon for my Agda code to require more parentheses,
because the checker can't see through simple combinators like these.

I expect sized types can easily deal with these cases. How much
smarter would the non-sized checker have to get to match them?

-- Dan