[Agda] A type for positive type functors?

[Nicolas Pouillard]

On Thu, 18 Nov 2010 19:55:07 +0100, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> Hi Dominique,
> 
> in your case, I am afraid, you have to turn off the positivity checker. 
>   Agda checks positivity by unfolding definitions, this is why the 
> concrete version with Maybe works.  However, if you abstract Maybe to a 
> variable M, positivity hold only if M is positive itself.
> 
> Currently Agda cannot handle this.  In my toy language MiniAgda it 
> works, because you can declare M to be strictly positive as follows:
> 
>    data EventHandlerMonad ++(M : Set -> Set) (E : Set) (A : Set) : Set ...
> 
> telling the positivity checker that M is assumed to be strictly positive 
> and can only be instantiated with strictly positive type functions.

This would be a very nice addition to Agda! In the same vein being able to
abstract over injective functions/constructors would be really helpful.

Actually any syntactic criterion could be equiped with a way to abstract over
things having this criterion.

-- 
Nicolas Pouillard
http://nicolaspouillard.fr