Cómo utilizar pares dependientes

Question

Supongamos que tengo una función (realmente hace lo que dice el nombre):

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

Ahora, me gustaría trabajar de alguna manera con la pareja dependiente que regreso.escribí sencillo head función:

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

que por supuesto funciona perfectamente.Pero me hizo preguntarme:¿Hay alguna manera de asegurarme de que la función solo pueda llamarse con n ≥ 1?

Idealmente, me gustaría hacer funcionar head : ∀ {A} → ∃ (λ n → Vec A n) → IsTrue (n ≥ succ zero) → A;pero eso falla, porque n está fuera de alcance cuando lo uso en IsTrue.

¡Gracias por tu tiempo!

---

IsTrue es algo como:

data IsTrue : Bool → Set where
  check : IsTrue true

Answer 1

Creo que esta es una pregunta sobre no cursar.La biblioteca estándar proporciona funciones incansables para productos, ver sin cursar.Para su situación, sería más beneficioso tener una función sin crianza donde se oculta el primer argumento, ya que una función de la cabeza normalmente tomaría el índice de longitud como un argumento implícito.Podemos escribir una función no curry como esa:

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

La función que devuelve la cabeza de un vector si hay una no parece existir en la biblioteca estándar, por lo que escribimos uno:

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

Ahora su función deseada es solo una cuestión de desinvertir la función tal vez con la función de insulto de primer argumento definida anteriormente:

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

Conclusión:Los productos dependientes se curry y uncurry con gusto como sus versiones no dependientes.

Dejando de lado la función que desea escribir con firma tipográfica

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

Se puede escribir como:

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

Answer 2

Probablemente, la mejor manera sea desestructurar primero el par dependiente, de modo que pueda escribir:

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

Sin embargo, si realmente desea mantener intacto el par dependiente en la firma de la función, puede escribir un predicado PosN que inspecciona el primer elemento del par y verifica que sea positivo:

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

o similar.Dejaré la definición de PosN como ejercicio al lector.Esencialmente, esto es lo que ya hace la respuesta de Vitus, pero en su lugar se puede definir un predicado más simple.

Answer 3

Después de jugar con él durante algún tiempo, se me ocurrió una solución que se parece a la función que quería en primer lugar:

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

Si a alguien se le ocurre una solución mejor (o más general), aceptaré con gusto su respuesta.Los comentarios también son bienvenidos.

---

Aquí hay un predicado más general que se me ocurrió:

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

Esto es como lo de siempre head función para Vec.

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