[Agda] Poll: Mixfix and parametrized modules --- which behavior
would you expect
Andreas Abel
andreas.abel at ifi.lmu.de
Mon May 14 08:51:50 CEST 2012
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/
More information about the Agda
mailing list