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

[Andreas Abel]

Holes in a mixfix declaration have at least two interpretations:

A) If I write

      _op_ : A -> B -> C

    I mean that the first _ is a placeholder for the A and the second _ 
is the placeholder for the B.  That is what pumpkingod suggested in 
issue 632 and I am leaning towards this interpretation as the most 
sensible one.

B) If I write

      _op_ : ...

    then the first _ is a placeholder for the first argument that op 
receives and the second _ for the second argument, whatever they may be. 
  This is what Agda currently implements.

B) leads to the strange effects with parametrized modules.

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.

Digression:

I think there is an oddity with parametrized modules and hiding anyway. 
  In the absence of hiding issues

   module L (A : Set) where
     data List : Set where
       []   : List
       _::_ : A -> List -> List
   open L

and

   data List (A : Set) : Set where
     []   : List A
     _::_ : A -> List A -> List A

are the same.  In the Coq, this is exploited a lot using the Section 
mechanism.  Hiding information can be given separately.

In Agda, one has only the choice of letting A be hidden in every 
declared identifier (bad for List) or none (bad for [] and _::_).  This 
is limiting the use of parametrized modules.  Special treatment is 
applied data and record parameter telescope to break up the scheme.

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.

Agda currently recalculates positivity whenever you instantiate a module.

Cheers,
Andreas

On 14.05.12 1:54 PM, Ulf Norell wrote:
>
> On Mon, May 14, 2012 at 11:59 AM, Nils Anders Danielsson
> <nad at chalmers.se <mailto:nad at chalmers.se>> wrote:
>
>     On 2012-05-14 08:51, Andreas Abel wrote:
>
>         This could be mended if for fixops we would consider all module
>         parameters hidden, whether they are declared as such or not.
>
>
>     I think we should strive for simplicity and avoid special cases like
>     this. Perhaps you /can/ currently write A + true, but do you?
>
>     I think the main problem is that the pretty-printer sometimes writes
>     A + true. Perhaps we can improve the pretty-printer.
>
>
> I agree with Nisse here. I think any change to the language would be
> complicating things unduly. Changing the pretty printer to not print
> A + true, on the other hand, sounds like a reasonable thing to do.
>
> / Ulf

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/