[Agda] Agda's coinduction incompatible with initial algebras

[Thorsten Altenkirch]

On 6 Oct 2011, at 05:20, Dan Doel wrote:

> 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.

I think we should separate the definitions of data types which provide a syntax to
define indexed coproducts and a more general record syntax which would allow 
us to define indexed records and the question of recursion / corecursion.

E.g. we may want to be able to define Vec using records using destructrs:

record Vec (A : Set) : ℕ → Set where
  destructor
    hd : ∀ {n} → Vec A (suc n) → A
    tl : ∀ {n} → Vec A (suc n) → Vec A n

But this is independent of the question wether Vec is inductive or coinductive.

> 
>> 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.

We should stick to things we understand intuitively. 

Btw, while we can show that having one universe closed under positive
definitions is sound in ZFC, it is not clear to me wether having 2 universes
with this feature is sound.

The reason for my question is that having Set0 closed under positive
definitions and Set1 impredicative is inconsistent.

Anyway, who needs non-strict positive definitions?

> 
> 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).

The lack of a sound foundation applies to a number of Agda features. 
I agree that this should be fixed though.

The problem we have has nothing to do with adopting the Pi-Sigma
approach which makes it much easier to work with mixed 
inductive-coinductive definitions. The problem is that the current 
termination checker doesn't handle nested coinduction properly.
This problem predates the move to \infty instead of codata.

It should be possible to be possible to fix this problem by labelling
\infty with the datatype it is supposed to guard and then apply an analysis 
based on parity games to implement the termination checker.

This analysis should correspond to an understanding of \infty by 
viewing each recursive datatype D = F(D) as a \nu X \mu Y.T(X,Y) 
where all  occurences of \infty D are translated to X and all others
to Y.

> 
> 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.

I agree.

> 
>> 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?

Good point.

We certainly want to have an extensible termination checker. 
I'd prefer to separate termination analysis from the type system.
I don't like sized types because they seem to complicate the type
structure and makes it harder to understand them intuitively.

Thorsten