Problems with using of dependent pairs in Agda

Question

I'm learning Agda by tutorial, and now I'm reading about dependent pairs.

So, this is the fragment of code:

data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (a : A) → (b : B a) → Σ A B

infixr 4 _,_

Σprojₗ : {A : Set}{B : A → Set} → Σ A B → A
Σprojₗ (a , b) = a

data _∈_ {A : Set}(x : A) : List A → Set where
  first : {xs : List A} → x ∈ x ∷ xs
  later : {y : A}{xs : List A} → x ∈ xs → x ∈ y ∷ xs

infix 4 _∈_

_!_ : ∀{A : Set} → List A → ℕ → Maybe A
  [] ! _           = nothing
  x ∷ xs ! zero    = just x
  x ∷ xs ! (suc n) = xs ! n

infix 5 _!_

lookup : ∀ {A}{x : A}(xs : List A) → x ∈ xs → Σ ℕ (λ n → xs ! n ≡ just x)

_,_ is a constructor of dependent pair, Σprojₗ returns first part of pair, _∈_ is a relation of membership, lst ! i returns just $(i-th element) if list's length is greater or equal than i, nothing — otherwise. I want to write a lookup function which takes list xs, proof of membership x ∈ xs, and returns dependent pair of natural number and function which for natural number n returns proof (or disproof) of the fact that n-th element of list is just x. Now the function looks like

lookup : ∀ {A}{x : A}(xs : List A) → x ∈ xs → Σ ℕ (λ n → xs ! n ≣ just x)
lookup {A} {x} .(x ∷ xs) (inHead {xs}) = 0 , refl
lookup .(y ∷ xs) (inTail {y} {xs} proof) = (1 + Σprojₗ (lookup xs proof)) , ?

I suppose that I should write some function like Σprojᵣ (it should return second element of pair, function with signature A → Set) for filling the hole, but I have no idea how to write it. The only variant which was typechecked is

Σprojᵣ : {A : Set}{B : A → Set} → Σ A B → (A → Set)
Σprojᵣ {A} {B} (a , b) = B

, but I didn't managed how to finish lookup function with this. How do I solve this exercise?

Answer 1

Indeed, assuming that Σprojᵣ projects the second element of the pair, Σprojᵣ (lookup xs proof) is correct solution which fits into the hole. The question is, how to write this projection?

---

If we had ordinary non-dependent pairs, writing both projections is easy:

data _×_ (A B : Set) : Set where
  _,′_ : A → B → A × B

fst : ∀ {A B} → A × B → A
fst (a ,′ b) = a

snd : ∀ {A B} → A × B → B
snd (a ,′ b) = b

What makes it so hard when we use dependent pair? The hint is hidden in the very name: the second component depends on the value of first and we have to somehow capture this in our type.

So, we start with:

data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (a : A) → B a → Σ A B

Writing the projection for the left component is easy (note that I'm calling it proj₁ instead of Σprojₗ, that's what the standard library does):

proj₁ : {A : Set} {B : A → Set} → Σ A B → A
proj₁ (a , b) = a

Now, the second projection should look a bit like this:

proj₂ : {A : Set} {B : A → Set} → Σ A B → B ?
proj₂ (a , b) = b

But B what? Since the type of the second component depends on the value of the first one, we somehow need to smuggle it through B.

We need to be able to refer to our pair, let's do it:

proj₂ : {A : Set} {B : A → Set} (pair : Σ A B) → B ?

And now, the first component of our pair is proj₁ pair, so let's fill that in:

proj₂ : {A : Set} {B : A → Set} (pair : Σ A B) → B (proj₁ pair)

And indeed, this typechecks!

---

There are, however, easier solutions than writing proj₂ by hand.

Instead of defining Σ as a data, we can define it as a record. Records are special case of data declarations that have only one constructor. The nice thing is that records give you the projections for free:

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ  -- opens the implicit record module

This (among other useful things) gives you projections proj₁ and proj₂.

---

We can also deconstruct the pair with with statement and avoid this proj bussiness altogether:

lookup : ∀ {A} {x : A}(xs : List A) → x ∈ xs → Σ ℕ (λ n → xs ! n ≡ just x)
lookup {x = x} .(x ∷ xs) (first {xs}) = 0 , refl
lookup         .(y ∷ xs) (later {y} {xs} p) with lookup xs p
... | n , p′ = suc n , p′

with allows you to pattern match not only on the arguments of the function, but also on intermediate expressions. If you are familiar with Haskell, it's something like a case.

---

Now, this is almost ideal solution, but still can be made a bit better. Notice that we have to bring the implicit {x}, {xs} and {y} into scope just so we can write down the dot pattern. Dot patterns do not participate in pattern matching, they are used as assertions that this particular expression is the only one which fits.

For example, in the first equation, the dot pattern tells us that the list must have looked like x ∷ xs - we know this because we pattern matched on the proof. Since we only pattern match on the proof, the list argument is a bit redundant:

lookup : ∀ {A} {x : A} (xs : List A) → x ∈ xs → Σ ℕ (λ n → xs ! n ≡ just x)
lookup ._ first = 0 , refl
lookup ._ (later p) with lookup _ p
... | n , p′ = suc n , p′

The compiler can even infer the argument to the recursive call! If the compiler can figure this stuff on its own, we can safely mark it implicit:

lookup : ∀ {A} {x : A} {xs : List A} → x ∈ xs → Σ ℕ (λ n → xs ! n ≡ just x)
lookup first = 0 , refl
lookup (later p) with lookup p
... | n , p′ = suc n , p′

Now, the final step: let's bring in some abstraction. The second equation takes the pair apart, applies some functions (suc) and reconstructs the pair - we map functions over the pair!

Now, the fully dependent type for map is quite complicated. Don't be discouraged if you don't understand! When you come back with more knowledge later, you'll find it fascinating.

map : {A C : Set} {B : A → Set} {D : C → Set}
      (f : A → C) (g : ∀ {a} → B a → D (f a)) →
      Σ A B → Σ C D
map f g (a , b) = f a , g b

Compare with:

map′ : {A B C D : Set}
       (f : A → C) (g : B → D) →
       A × B → C × D
map′ f g (a ,′ b) = f a ,′ g b

And we conclude with the very concise:

lookup : ∀ {A} {x : A} {xs : List A} → x ∈ xs → Σ ℕ (λ n → xs ! n ≡ just x)
lookup first     = 0 , refl
lookup (later p) = map suc id (lookup p)

That is, we map suc over the first component and leave the second one unchanged (id).