Agda: Pair of vectors that have the same length

Question

In Agda, how can I define a pair of vectors that must have the same length?

-- my first try, but need to have 'n' implicitly  
b : ∀ ( n : ℕ ) → Σ (Vec ℕ n) (λ _ → Vec ℕ n) 
b 2 = (1 ∷ 2 ∷ []) , (3 ∷ 4 ∷ [])
b 3 = (1 ∷ 2 ∷ 3 ∷ []) , (4 ∷ 5 ∷ 6 ∷ [])
b _ = _

-- how can I define VecSameLength correctly?
VecSameLength : Set
VecSameLength = _

c : VecSameLength
c = (1 ∷ 2 ∷ []) , (1 ∷ 2 ∷ [])

d : VecSameLength
d = (1 ∷ 2 ∷ 3 ∷ []) , (4 ∷ 5 ∷ 6 ∷ [])

-- another try
VecSameLength : Set
VecSameLength = Σ (Vec ℕ ?) (λ v → Vec ℕ (len v)) 

Answer 1

If you want to keep the length as a part of the type, you just need to pack up two vectors with the same size index. Necessary imports first:

open import Data.Nat
open import Data.Product
open import Data.Vec

Nothing extra fancy: just as you would write your ordinary vector of size n, you can do this:

2Vec : ∀ {a} → Set a → ℕ → Set a
2Vec A n = Vec A n × Vec A n

That is, 2Vec A n is the type of pairs of vectors of As, both with n elements. Note that I took the opportunity to generalize it to arbitary universe level - which means you can have vectors of Sets, for example.

The second useful thing to note is that I used _×_, which is an ordinary non-dependent pair. It is defined in terms of Σ as a special case where the second component doesn't depend on the value of first.

And before I move to the example where we'd like to keep the size hidden, here's an example of a value of this type:

test₁ : 2Vec ℕ 3
-- We can also infer the size index just from the term:
-- test₁ : 2Vec ℕ _    
test₁ = 0 ∷ 1 ∷ 2 ∷ [] , 3 ∷ 4 ∷ 5 ∷ []

You can check that Agda rightfully complains when you attempt to stuff two vectors of uneven size into this pair.

Hiding indices is job exactly suited for dependent pair. As a starter, here's how you'd hide the length of one vector:

data SomeVec {a} (A : Set a) : Set a where
  some : ∀ n → Vec A n → SomeVec A

someVec : SomeVec ℕ
someVec = some _ (0 ∷ 1 ∷ [])

The size index is kept outside of the type signature, so we only know that the vector inside has some unknown size (effectively giving you a list). Of course, writing a new data type everytime we needed to hide an index would be tiresome, so standard library gives us Σ.

someVec : Σ ℕ λ n → Vec ℕ n
-- If you have newer version of standard library, you can also write:
-- someVec : Σ[ n ∈ ℕ ] Vec ℕ n
-- Older version used unicode colon instead of ∈
someVec = _ , 0 ∷ 1 ∷ []

Now, we can easily apply this to the type 2Vec given above:

∃2Vec : ∀ {a} → Set a → Set a
∃2Vec A = Σ[ n ∈ ℕ ] 2Vec A n

test₂ : ∃2Vec ℕ
test₂ = _ , 0 ∷ 1 ∷ 2 ∷ [] , 3 ∷ 4 ∷ 5 ∷ []

---

copumpkin raises an excellent point: you can get the same guarantee just by using a list of pairs. These two representations encode exactly the same information, let's take a look.

Here, we'll use a different import list to prevent name clashes:

open import Data.List
open import Data.Nat
open import Data.Product as P
open import Data.Vec as V
open import Function
open import Relation.Binary.PropositionalEquality

Going from two vectors to one list is a matter of zipping the two vectors together:

vec⟶list : ∀ {a} {A : Set a} → ∃2Vec A → List (A × A)
vec⟶list (zero  , []     , [])     = []
vec⟶list (suc n , x ∷ xs , y ∷ ys) = (x , y) ∷ vec⟶list (n , xs , ys)

-- Alternatively:
vec⟶list = toList ∘ uncurry V.zip ∘ proj₂

Going back is just unzipping - taking a list of pairs and producing a pair of lists:

list⟶vec : ∀ {a} {A : Set a} → List (A × A) → ∃2Vec A
list⟶vec [] = 0 , [] , []
list⟶vec ((x , y) ∷ xys) with list⟶vec xys
... | n , xs , ys = suc n , x ∷ xs , y ∷ ys

-- Alternatively:
list⟶vec = ,_ ∘ unzip ∘ fromList

Now, we know how to get from one representation to the other, but we still have to show that these two representations give us the same information.

Firstly, we show that if we take a list, convert it to vector (via list⟶vec) and then back to list (via vec⟶list), then we get the same list back.

pf₁ : ∀ {a} {A : Set a} (xs : List (A × A)) → vec⟶list (list⟶vec xs) ≡ xs
pf₁ []       = refl
pf₁ (x ∷ xs) = cong (_∷_ x) (pf₁ xs)

And then the other way around: first vector to list and then list to vector:

pf₂ : ∀ {a} {A : Set a} (xs : ∃2Vec A) → list⟶vec (vec⟶list xs) ≡ xs
pf₂ (zero  , []     , [])     = refl
pf₂ (suc n , x ∷ xs , y ∷ ys) =
  cong (P.map suc (P.map (_∷_ x) (_∷_ y))) (pf₂ (n , xs , ys))

In case you are wondering what cong does:

cong : ∀ {a b} {A : Set a} {B : Set b}
       (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

We've shown that list⟶vec together with vec⟶list form an isomorphism between List (A × A) and ∃2Vec A, which means that these two representations are isomorphic.