How to inspect the value inside a product (Σ)?

Question

I am trying to wrap my head around the Σ type by playing with a filterVec function, analogous to the filter function available for lists. See my implementation below:

-- Some imports we will need later
open import Data.Bool
open import Data.Nat
open import Data.Product
open import Data.Vec

-- The filterVec function
filterVec : {n : ℕ} -> (ℕ -> Bool) -> Vec ℕ n -> Σ ℕ (λ length → Vec ℕ length)
filterVec _ [] = 0 , []
filterVec f (x ∷ xs) with filterVec f xs
... | length , filtered = if f x then (suc length , x ∷ filtered) else (length , filtered)

Happy with my function, I decided to test it

dummyVec : Vec ℕ 5
dummyVec = 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []

dummyFn : Vec ℕ 5
dummyFn with filterVec (λ _ → true) dummyVec
dummyFn | length , xs = {!!} -- I would like to return xs here, but Agda throws a type error

For some reason, Agda is unable to tell that length is 5, so it doesn't allow me to return xs. However, the code below does work:

open import Relation.Binary.PropositionalEquality
dummyProof : proj₁ (filterVec (λ _ → true) dummyVec) ≡ 5
dummyProof = refl

I am utterly confused by this behavior. In the case of dummyFn, Agda cannot tell that the length is 5, but in the case of dummyProof, Agda proves it without any problem.

What am I missing? How can I get dummyFn to work?

user_3237465 · Answer

with binds a value to a name. If you want to compute, you can use let:

dummyFn′ : Vec ℕ 5
dummyFn′ = let length , xs = filterVec (λ _ → true) dummyVec
           in xs

Let's look at the following example:

dummy : Set
dummy with 5
dummy | x = {!!}

Should the x magically reduce to 5 in the hole? No. You've given 5 another name — x, and those expressions are neither judgementally nor propositionally equal.

Now in your example:

dummyFn : Vec ℕ 5
dummyFn with filterVec (λ _ → true) dummyVec
dummyFn | length , xs = {!!}

You've given the length name to the length of xs. And it does not reduce to 5. It's a name. If you want both to give a name and to remember what the name is for, there is the inspect idiom for this:

dummyFn′′ : Vec ℕ 5
dummyFn′′ with filterVec (λ _ → true) dummyVec | inspect (filterVec (λ _ → true)) dummyVec
dummyFn′′ | length , xs | [ refl ] = xs

How to inspect the value inside a product (Σ)?

1 Answers