[Agda] Poll: Mixfix and parametrized modules --- which behavior would you expect

[Nils Anders Danielsson]

On 2012-05-14 20:33, Andreas Abel wrote:
> A) would require a change of implementation, but I think not a severe
> one. Basically, you have to store with each identifier how many
> arguments have been added by module telescopes in the front. If those
> contain any non-hidden ones, infix/mixfix notation is not printed nor
> parsed. I guess this is what Nisse and Ulf suggest, essentially.

I did not suggest changing the parser.

> The issue pops up for other argument decorations besides hiding.  For
> instance, positivity information cannot be computed once and for all
> for a parametrized module.  For instance, one could not have
>
>    module L (+A : Set) where  -- + shall mean that L is covariant in A
>      data List : Set where
>        []   : List
>        _::_ : A -> List -> List
>    open L
>
> because, while List is covariant in A, [] and _::_ are not.

What do you mean? AFAIU you could compute the information, but you
couldn't simply assign a unique positivity annotation to every
parameter. Would you want to disallow the module L?

-- 
/NAD