[Agda] initial T-algebra for an endofunctor T, via sized types

[Andrew Pitts]

Hi Wouter.

> On 7 Nov 2019, at 16:18, Swierstra, W.S. (Wouter) <W.S.Swierstra at uu.nl> wrote:
> 
> Dear Andy,
> 
>> Did I somehow over-complicate things? Am I re-inventing a construction that already exists?
> 
> I'm not sure what your goal is exactly -- and I may be answering a
> different question entirely -- but one approach that might work for
> you would be to *not* try to take the fixpoint of some arbitrary T :
> Set -> Set, but instead define a universe of well-behaved functors,
> closed under identity, coproducts, products, etc.

Yes, if one assumes more about the endofunctor as you suggest (it can be built up using certain functorial constructions) then I’m sure one can prove the existence of initial algebras; and one probably doesn’t need sized types to do that (recurse over the structure of codes instead). 

However, I was more interested in trying to get a feel for the power of sized types (for inductive things): given that sized types are available, what do we have to assume about an endofunctor in order to use them to construct an initial algebra in Agda as the size-indexed “colimit” of approximations to it? The answer (slightly surprising to me) was: nothing other than telling Agda about its strictly positive polarity.

> Agda is just about smart enough to let you can define the
> corresponding initial algebra, maps and folds for the functors that
> inhabit this universe. I haven't tried doing all the proofs -- some
> will probably require function extensionality -- but I've sketched the
> main ideas in the attached .agda file. I learned of the definition of
> 'foldMap' -- that passes Agda's termination checker -- from Ulf
> Norell's lecture notes on Agda. This trick might work for your
> development too, but I haven't tried it.

Thank you for telling me about foldMap!

Best wishes,

Andy