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

[Andreas Abel]

Hello all,

this is a question of language design where all of you might have an 
opinion.  Consider this parametrized module:

   module M (A : Set) where

     infix _+_ 4

     _+_ : Bool → Bool → Bool
     true  + x = true
     false + x = x

     if_then_else_ : Bool → A → A → A
     if true  then a else b = a
     if false then a else b = b

   open M

Since M has a non-hidden parameter, _+_ and if_then_else_ get another 
argument A, which shifts all the argument positions.  So now we can write

   testM : (A : Set) → A + true ≡ λ x → x

   testIf : (A : Set)(a : A) → if A then false else a ≡ λ b → b

which of course looks utterly wrong.  The question is whether the 
semantics of fixops should be changed so that the argument positions 
indicated by _ are not context sensitive, i.e., do not get shifted when 
the extra argument A is added in the front.

This could be mended if for fixops we would consider all module 
parameters hidden, whether they are declared as such or not.  Then we 
would get

   if : {A : Set} -> Bool -> A -> A -> A

which would leave the _-indicated positions in their original place.

It would then destroy the following use pattern: Define

     record State (S A : Set) : Set where
       field
         _runState_ : S -> A * S

   then we can write

     r runState s

   for r : State S A.

Here, the shift resulting from the add the "self" argument

   (r : State S A)

is calculated in to obtain an infix op.

What is your opinion on this from your experience with Agda?  How would 
you fixops expect to work?  Should records behave differently than modules?

Cheers,
Andreas


-- 
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/