[Agda] Agda's coinduction incompatible with initial algebras

[Thorsten Altenkirch]

The issue is that currently Agda doesn't handle mu-nu nesting properly. Any datatype is viewed as a nu-mu.

This is not what we want, because as you say it is not compositional.

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.

While we haven't got a solution we can all agree on yet, it may be a good idea not to jump too quickly. The current algorithm is an approximation which works in most cases.
Also I do think it is sound even though not compositional as you say.

Cheers,
Thorsten


On 5 Oct 2011, at 19:13, Andreas Abel wrote:

> On 04.10.11 11:18 PM, Dan Doel wrote:
>> 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.
> 
> Not in Agda.  Try MiniAgda.  Or read the literature.
> 
>> 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.
> 
> These two systems have not been integrated, since there is a history of dispute stretching several years what we should go for.  [With a current cease-fire, but no peace treaty.  Maybe I should not have touched this issue.]
> 
> I have embraced sized types since the are compositional.  Meaning you can abstract code out and still retain termination.  This enables me, in the given example, to write iter for a generic initial algebra.
> 
> 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.
> 
>> 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 do not want magic functors.  At least the type system should distinguish them from ordinary functors.  But as of now, attempts to give a semantics of co per se have failed, also as a magic functor.
> 
>> I'm not particularly happy that things work that way.
> 
> Well, then things should change.
> 
>> 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).
> 
> 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").
> 
>> 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.
> 
> Well, what exactly Agda's conventions are, is under dispute.
> 
> We are not faced with a God-given system called Agda to which we have to bow and accept whatever it grants us.  We are building a system called Agda, and we want to apply the best principles to it.  Compositionality is a principle I am not sacrificing to limitations of an implementation.  Good theoretical justification is another principle I am not sacrificing.  There are 4 PhD theses on sized types in the context of type theory, and there are more than a dozen papers.  These give models that show consistency and prove strong normalization.  Point me to a foundation of "how things work in Agda", I would be grateful, since I am not aware of any.
> 
> I am getting tired of defending sized types against non-scientific arguments.  Do the hard science, or let it be.
> 
> Please excuse my impatience, there is a history to this dispute,
> 
> Andreas
> 
> -- 
> Andreas Abel  <><      Du bist der geliebte Mensch.
> 
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
> 
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda