[Agda] A type for positive type functors?

[Dan Licata]

Hi Dominique,

The main problem here is that Agda does not allow you to take the fixed
point of an arbitrary functor, but only a *strictly positive* one.  For
example, the following definition is illegal:

  data C : Set where
    c : ((C -> Bool) -> Bool) -> C

As I understand it, the motivation for this is the desire for a model in
Sets: this datatype would be asking for a set C such that C is
isomorphic to its double-powerset, which cannot exist for size reasons.

You could look at the work by Altenkrich, Morris, et al. on "containers"
if you would like to pass around a representation of a strictly positive
functor.

-Dan

On Nov18, 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
>