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

[Gabriel Scherer]

It is not realistic to expect a single choice to work well both when
opening the parametrized module (open M), and when opening the module
applied to some parameter (open M A). The parametrized module M (A :
Set) in your example is clearly designed to be opened once the
parameter have been applied, while you could design cases where the
infix choices are made precisely to account for this additional
parameter -- the module derived from the record State is one such
example.

I believe the problem in the "module M" case is to expect something
usable to be produced out of mifix operators when using "open M". If
you want to use those mixfix operators, you should have the discipline
to use "open M A" instead. If the library author wishes to facilitate
programming in the parametrized setting, he/she should explicitely
provide [_]_+_ convenience functions, like Thorsten demonstrated,
outside the module definition.

In my view, there should therefore be no ad-hoc choice for infix
operators. It should follow the simple and regular parametrization
rules of modules (parameters keep their impliciteness, and the
argument corresponding to the record value remains explicit), so that
library authors can make their own choice of style (favoring
parametrized or non-parametrized opening) without surprising the
users.

On Mon, May 14, 2012 at 10:18 AM, Altenkirch Thorsten
<psztxa at exmail.nottingham.ac.uk> wrote:
> 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.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>