[Agda] Agda's coinduction incompatible with initial algebras

[Andreas Abel]

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/