[Agda] A type for positive type functors?

[Sam Staton]

I would find Andreas' types useful.

I don't think containers are sufficient to describe all strictly positive functors (unless Agda is made less intensional, which would be welcome).

For instance, the functor 
FX = X + 1
is not expressible as a container; the best you can do is
GX = X^1 + X^0
which is not isomorphic to F (in Agda).

So, in Agda, you cannot recover the type of natural numbers (mu X.FX) as a fixed point of a container.

Please correct me if I have missed something. It's because of things like this that I stick to informal pen-on-paper most of the time.

Sam.

PS. I can imagine a more sophisticated datatype of containers which would accommodate this better: where each shape has an arity (a natural number) as well as an optional set of positions. But that is getting quite complicated!




> Date: Fri, 19 Nov 2010 10:05:08 +0000
> From: Thorsten Altenkirch <txa at Cs.Nott.AC.UK>
> Subject: Re: [Agda] A type for positive type functors?
> To: Dominique Devriese <dominique.devriese at gmail.com>
> Cc: Agda at lists.chalmers.se
> Message-ID: <E04DB440-F37A-471E-90FA-0845D5650C8B at Cs.Nott.AC.UK>
> Content-Type: text/plain; charset=us-ascii
> 
> You cannot in general construct fixpoints of arbitrary functors, e.g. FX = (X->2)->2 hasn't got an initial algebra in Type Theory.
> 
> If you want to have fixpoints you should refer to containers, i.e. S : Set, P : S -> Set which give rise to the functor FX = Sigma S (\ s -> Ps -> X). The initial algebra of a container is given by the W-type W S P.
> 
> Cheers,
> Thorsten
> 
> On 19 Nov 2010, at 08:33, Dominique Devriese wrote:
> 
>> Thorsten,
>> 
>> 2010/11/18 Thorsten Altenkirch <txa at cs.nott.ac.uk>:
>>> I just wonder how many different functions spaces we'll end up with.
>>> 
>>> If one wants to quantify over functors why don't you just do that? I mean define Functor : Set1 as a record (extending RawFunctor from the library) and then show that it is closed under various operations?
>> 
>> I think I understand what you mean, but wouldn't this ultimately
>> require some form of collaboration from the positivity checker when
>> taking a data type fixpoint as in my EventHandlerMonad example above?
>> 
>> Dominique
> 
> 
> 
> ------------------------------
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 
> 
> End of Agda Digest, Vol 63, Issue 17
> ************************************