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

[Benja Fallenstein]

Hi Andreas!

On Mon, May 14, 2012 at 8:51 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> What is your opinion on this from your experience with Agda?  How would you
> fixops expect to work?  Should records behave differently than modules?

I'm kind of surprised I've never run into this... maybe I've
subconsciously shied away from infix record fields? Not sure.

Making module parameters of mixfix ops implicit feels right to me.
Although the _runState_ example has *some* appeal, it's actually
pretty ugly that the first parameter isn't displayed in the type
signature:

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

This doesn't look right... Also, of course, you can't correctly use it
infix *inside* the record module, and if you use it prefix, it again
looks weird because the _runState_ syntax makes you think that the
first argument passed to it should be the one that replaces the left
underscore. All in all, it doesn't seem worth it.

You can of course write

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

_runState_ = State.runState

which is annoyingly more verbose, but seems like a better balance.

BTW, have you thought about how 'rename' statements should interact
with this? One natural possibility would be to make the module
arguments implicit iff the new name is a mixfix op. (If you'd make it
implicit only if *both* the old and new names are mixfix, you could
write the above as

    open State renaming (runState to _runState_)

but on reflection I don't really think that would be a good idea...)


Thorsten writes:
> I am not sure wether it is safe to assume that the hidden parameter can always be inferred.

I've recently grappled with non-inferrable implicit parameters to
infix ops a couple of times. I'm wondering whether it would be worth
it to allow

x ~ {A} y

to mean _~_ {A} x y; given the behavior of {}, could presumably also be written

x ~{A} y

This doesn't look all that weird to me if I think of {...} as a
subscript, à la Epigram.

Cheers,
- Benja