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

[Altenkirch Thorsten]

Indeed I run into this problem when defining setoid like structures with

record Setoid : Set₁  where
field
  set : Set₀
  _~_ : set → set → Propoid


A way out of this (suggested by Darin Morrison) is to use instead

  [_]_~_ : set → set → Propoid

but then we need to fix this for the declarations of refl, sym and trans.

...
_~_ : set → set → Propoid
_~_ = [_]_~_
  field
  refl : (x : set) → prf (x ~ x)
  trans : ∀ {x}{y}{z} → prf (y ~ z) → prf (x ~ y) → prf (x ~ z)
  sym : ∀ {x}{y} → prf (x ~ y) → prf (y ~ x)

but it would be better if one wouldn't need to do this. However, I am not
sure wether it is safe to assume that the hidden parameter can always be
inferred. And the change would break the [_]_~_ declaration.

Hmm I guess we could still define

[ A ]_~_ = _~_ {A}


Thorsten




On 14/05/2012 07:51, "Andreas Abel" <andreas.abel at ifi.lmu.de> wrote:

>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/
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda


This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.