[Agda] A type for positive type functors?

[Thorsten Altenkirch]

> 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.

I was just remarking that we can express the type of strictly positive functors as containers.

> 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.

I understand what you mean but I think there are too many potentially desirable refinements of function types to result in a type theory which is still comprensible or usable. Another interesting option is coercion space corresponding to coercive subtyping, or your parametric function space, not to forget the injective function space and obviously the annotations one needs for type-based termination. 

I am not sure the monster we will end up could be called "well designed".

Type Theory is rich enough to express these conditions semantically. What we need is an easy way to combine the convenient syntax we want to use with the semantic conditions they refer to. The soundness proof is then replaced by the elaboration of the syntax.

Cheers,
Thorsten
> 
> 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
>> 
>> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101119/1f677e35/attachment.html