bidi-lookup.md

In Agda, I can write many different records with a lookup field.

record DVec (n : ℕ) (A : Fin n → Set) : Set where
  constructor tabulate
  field lookup : (i : Fin n) → A i
open DVec public

record DMat (m n : ℕ) (A : Fin m → Fin n → Set) : Set where
  constructor tabulate
  field lookup : (i : Fin m) (j : Fin n) → A i j
open DMat public

Then, when I use lookup in some later code, the scope checker will pick out that it's a field, but not what record it's a field for. That information comes from whatever term lookup is applied to (noticed at type checking time). Intuitively, we have the following two typing rules:

e ∈ DVec n A   Fin n ∋ i     e ∈ DMat m n A   Fin m ∋ i   Fin n ∋ j
------------------------     --------------------------------------
    lookup e i ∈ A i                  lookup e i j ∈ A i j

(We may also curry away i and j.) This is to say, when synthesising a type for lookup e, we first synthesise a type for e, and based on that we decide how to continue.

However, once we introduce a function lookup, all of this falls flat.

-- Vec from Data.Vec

lookup : Vec A n → Fin n → A
lookup (x ∷ xs) zero = x
lookup (x ∷ xs) (suc i) = lookup xs i

Being a function, this is subject to the usual function type synthesising rule:

f ∈ (x : A) → B x   A ∋ s
-------------------------
        f s ∈ B s

That's to say, when lookup takes the place of f, we expect it to synthesise its own type, with subsequent arguments only checked. This basically means that function names have to be unique, so we know what type to synthesise.

Allowing function names to be declared eliminators (or field accessors, if you prefer) would allow the kind of overloading we had with record fields before for arbitrary functions. We could also imagine similar for constructors, letting us overload tabulate, even if we want to use the tabulate from Data.Vec (a function). The goal of all this is to make programming with derived operations as easy as programming with constructors and eliminators, given that complex problems usually end up being filled with derived operations.