How to use dependent pairs

Question

Suppose I have a function (it really does what the name says):

filter : ∀ {A n} → (A → Bool) → Vec A n → ∃ (λ m → Vec A m)

Now, I'd like to somehow work with the dependent pair I return. I wrote simple head function:

head :: ∀ {A} → ∃ (λ n → Vec A n) → Maybe A
head (zero   , _ )       = nothing
head (succ _ , (x :: _)) = just x

which of course works perfectly. But it made me wonder: is there any way I can make sure, that the function may only be called with n ≥ 1?

Ideally, I'd like to make function head : ∀ {A} → ∃ (λ n → Vec A n) → IsTrue (n ≥ succ zero) → A; but that fails, because n is out of scope when I use it in IsTrue.

Thanks for your time!

---

IsTrue is something like:

data IsTrue : Bool → Set where
  check : IsTrue true

Answer 1

I think this is a question about uncurrying. The standard library provides uncurrying functions for products, see uncurry. For your situation, it would be more beneficial to have a uncurry function where the first argument is hidden, since a head function would normally take the length index as an implicit argument. We can write an uncurry function like that:

uncurryʰ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : (a : A) → B a → Set c} →
           ({x : A} → (y : B x) → C x y) →
           ((p : Σ A B) → uncurry C p)
uncurryʰ f (x , y) = f {x} y

The function that returns the head of a vector if there is one does not seem to exist in the standard library, so we write one:

maybe-head : ∀ {a n} {A : Set a} → Vec A n → Maybe A
maybe-head []       = nothing
maybe-head (x ∷ xs) = just x

Now your desired function is just a matter of uncurrying the maybe-head function with the first-argument-implicit-uncurrying function defined above:

maybe-filter-head : ∀ {A : Set} {n} → (A → Bool) → Vec A n → Maybe A
maybe-filter-head p = uncurryʰ maybe-head ∘ filter p

Conclusion: dependent products gladly curry and uncurry like their non-dependent versions.

Uncurrying aside, the function you want to write with type signature

head : ∀ {A} → ∃ (λ n → Vec A n) → IsTrue (n ≥ succ zero) → A

Can be written as:

head : ∀ {A} → (p : ∃ (λ n → Vec A n)) → IsTrue (proj₁ p ≥ succ zero) → A

Answer 2

The best way is probably to destructure the dependent pair first, so that you can just write:

head :: ∀ {A n} → Vec A (S n) → A

However, if you really want to keep the dependent pair intact in the function signature, you can write a predicate PosN which inspects the first element of the pair and checks that it is positive:

head :: ∀ {A p} → PosN p -> A

or similar. I'll leave the definition of PosN as an exercise to the reader. Essentially this is what Vitus' answer already does, but a simpler predicate can be defined instead.

Answer 3

After playing with it for some time, I came up with solution that resembles the function I wanted in first place:

data ∃-non-empty (A : Set) : ∃ (λ n → Vec A n) → Set where
  ∃-non-empty-intro : ∀ {n} → {x : Vec A (succ n)} → ∃-non-empty A (succ n , x)

head : ∀ {A} → (e : ∃ (λ n → Vec A n)) → ∃-non-empty A e → A
head (zero   , [])       ()
head (succ _ , (x :: _)) ∃-non-empty-intro = x

If anyone comes up with better (or more general) solution, I'll gladly accept their answer. Comments are welcome, too.

---

Here's more general predicate I came up with:

data ∃-succ {A : Nat → Set} : ∃ A → Set where
  ∃-succ-intro : ∀ {n} → {x : A (succ n)} → ∃-succ (succ n , x)

-- or equivalently
data ∃-succ {A : Nat → Set} : ∃ (λ n → A n) → Set where
  ...

Answer 4

This is just like the usual head function for Vec.

head' : ∀ {α} {A : Set α} → ∃ (λ n → Vec A (suc n)) → A
head' (_ , x ∷ _) = x