[Agda] A type for positive type functors?

[Andreas Abel]

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.

Cheers,
Andreas


On 11/18/10 3:51 PM, Dominique Devriese wrote:
> Hi,
>
> Is there anyway to represent a positive type functor in the Agda type
> system? I'm thinking of the following situation. I can encode a simple
> "event handler monad" over Maybe as the base monad as follows:
>
>     data EventHandlerMonad E A : Set where
>        mkM : Maybe (A × Maybe (E → EventHandlerMonad E ⊤)) →
> EventHandlerMonad E A
>
>     v : EventHandlerMonad ⊤ ⊤
>     v = mkM (just (tt , nothing ))
>     v2 : EventHandlerMonad ⊤ ⊤
>     v2 = mkM (just (tt , just (\_ → v) ))
>
> However, when I try to abstract from Maybe as the base monad like this:
>
>     data EventHandlerMonad M E A : Set where
>        mkM : M (A × Maybe (E → EventHandlerMonad M E ⊤)) →
> EventHandlerMonad M E A
>
>     v : EventHandlerMonad Maybe ⊤ ⊤
>     v = mkM (just (tt , nothing ))
>     v2 : EventHandlerMonad Maybe ⊤ ⊤
>     v2 = mkM (just (tt , just (\_ → v) ))
>
> I get an error saying that "EventHandlerMonad is not strictly
> positive, because it occurs in the second argument to Maybe in the 4th
> argument to Σ in an argument to a bound variable in the type of the
> constructor mkM in the definition of EventHandlerMonad."
>
> In my use case, M should be a monad, and I have the intuition that
> since M is a functor, then in its definition, the argument type cannot
> be used in "contravariant" positions, so M must be a positive functor?
> However, if this intuition is correct, then there does not seem any
> way to communicate this fact to Agda? Even if I require an argument of
> type (RawFunctor M), Agda will not notice that M is therefore
> positive?
>
> Are my intuitions wrong, or is there some way to achieve what I'm
> trying to do in Agda? Any interesting references perhaps?
>
> Thanks for your help,
> Dominique
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>