Indexed family of binary operators with infix notation

Question

Suppose you want to define a family of binary operators (indexed by sets, say) where the types of the arguments depends on the value of the index, and the index is passed explicitly. In addition, suppose you would like a member of the family to be usable in infix notation:

x <[A] y

A here is the index; the brackets [-] are supposed to indicate that A should be read as a subscript. Giving a type signature for such an operation compatible with this syntax is difficult because the type of x depends on the value A, and so A : Set must occur to the left of x : A in the definition of _<[_]_.

I've experimented with the following trick (hack?) based on syntax declarations:

cmp : (A : Set) → A → A → Set
cmp = {!!}

syntax cmp A x y = x <[ A ] y

postulate C : Set
postulate c : C

x = c <[ C ] c

This seems to work, unless your binary operation uses implicit instances. If I try to add arguments of the form {{x}} to a syntax declaration, Agda complains. (Not unreasonably, perhaps.)

It seems one can adapt the idiom by introducing a version of cmp which takes the implicit instance explicitly, and then define a variant of the syntax which invokes that version:

postulate B : Set

-- Now expects an ambient B.
cmp : (A : Set) {{b : B}} → A → A → Set
cmp = {!!}

-- Version of cmp that makes implicit instance explicit.
cmp-explicit : (A : Set) (b : B) → A → A → Set
cmp-explicit A b = cmp A {{b}}

syntax cmp A x y = x <[ A ] y
syntax cmp-explicit A b x y = x <[ A at b ] y

postulate C : Set
postulate c : C
postulate b : B

x = c <[ C ] c       -- pick up ambient B
y = c <[ C at b ] c  -- pass B explicitly

(Since syntax doesn't appear to support {{x}} arguments, one cannot just inline cmp into cmp-explicit, without giving up the ability to pick up an ambient B entirely.)

Is this a hack? Is there another way to flip arguments x and y when the type of y depends on the value of x, and x is passed explicitly?

Naturally, defining

_<′[_]_ = λ x A y → cmp A x y

causes Agda to complain when typechecking x.

Answer 1

You can't really flip the arguments in a way that A : Set comes after x : A.

You already mentioned syntax, which I think is the best solution. This works because Agda will transform x <[ A ] y into cmp A x y and that's fine with the type checker.

Here's another (rather ugly and hacky) approach. Let's say we have:

_<[_]_ : {A : Set} → A → ? → A → Set

Here we can exploit unification a bit: by using something that mentions A in the ? hole, we can force the type checker to fill in the implicit A in front. But as far as I know, there's no simple type we can use in place of ?, so that we get the required x <[ A ] y. But to finish the thought, here's one thing that works:

data Is : Set → Set₁ where
  is : (A : Set) → Is A

_<[_]_ : {A : Set} → A → Is A → A → Set
x <[ is A ] y = cmp A x y

Yes, this is fairly ugly and I would recommend against it.

---

But back to your question about syntax: I would not consider syntax to be a hack in any way. In fact, the standard library uses syntax in roughly the same way in one place (Data.Plus to be exact):

syntax Plus R x y = x [ R ]⁺ y

Even having cmp-explicit around is useful. I would even go as far as to suggest you make two extra versions:

cmp-syntax          =         cmp
cmp-explicit-syntax = λ A b → cmp A {{b}}

syntax cmp-syntax          A   x y = x <[ A      ] y
syntax cmp-explicit-syntax A b x y = x <[ A at b ] y

If the user of your module does not want to use the syntactic shortcut (for example, he imports another module that defines _<[_]_), he can simply choose to not import it and still have cmp around.

Again, standard library does this with the syntactic shortcut for Σ. The shortcut allows you to write:

open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality

x : Σ[ n ∈ ℕ ] n + 2 ≡ 4
x = 2 , refl

And if you do not want it, then you simply:

open import Data.Product
  hiding (Σ-syntax)