[Agda] A type for positive type functors?

[Andreas Abel]

Hi Thorsten,

I think the problem is not about positive functors not having a fixed 
point but about strictly positive functors not recognized by the Agda 
positivity checker.

About you complaint on how many function types we might get...

I think a language is well-designed if it has all the abstractions.  Or 
stated differently, the user should be able to roll his own constructs 
which are analogous to those he finds in the system.  Otherwise there 
will be always frustrating limits, like:

* The language has built-in infix operators but I cannot define my own.
   Solved by Haskell.

* The language has its own special forms (like short-cut binary ops) but
   I cannot define my own because of call-by-value.
   Solved by Haskell's call-by-need.

* I can define my own special forms but not give them a nice syntax like
   if_then_else_
   Solved by Agda's mixfix operators.

* I can define strictly positive functors but not abstract over them.
   Solved by MiniAgda's polarities.

* I can build data structures but not abstract over them.
   Solved by ML's functors.
   Solved somewhat by Haskell's type classes.
   Solved somewhat by Agda's records
   (what is missing here are abstract reductions).

We've come far, but not far enough.

Cheers,
Andreas

On 11/19/10 11:05 AM, Thorsten Altenkirch wrote:
> 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
>
>