Como usar pares dependentes

Question

Suponha que eu tenha uma função (ela realmente faz o que o nome diz):

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

Agora, gostaria de trabalhar de alguma forma com o par dependente que retorno.eu escrevi simples head função:

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

o que obviamente funciona perfeitamente.Mas isso me fez pensar:existe alguma maneira de ter certeza de que a função só pode ser chamada com n ≥ 1?

Idealmente, eu gostaria de fazer funcionar head : ∀ {A} → ∃ (λ n → Vec A n) → IsTrue (n ≥ succ zero) → A;mas isso falha, porque n está fora do escopo quando eu o uso em IsTrue.

Obrigado pelo seu tempo!

---

IsTrue é algo como:

data IsTrue : Bool → Set where
  check : IsTrue true

Answer 1

Acho que esta é uma questão sobre não curry.A biblioteca padrão fornece uncurrying funções para produtos, consulte sem curry.Para a sua situação, seria mais benéfico ter uma função uncurry onde o primeiro argumento é oculto, uma vez que uma função head normalmente tomaria o índice de comprimento como um argumento implícito.Podemos escrever uma função sem curry assim:

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

A função que retorna a cabeça de um vetor, se houver um, não parece existir na biblioteca padrão, Então escrevemos um:

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

Agora sua função desejada é apenas uma questão de desvendar o função talvez-cabeça com o primeiro-argumento-implícito-uncurrying função definida acima:

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

Conclusão:produtos dependentes curry e uncurry de bom grado como suas versões não dependentes.

Deixando de lado a curiosidade, a função que você deseja escrever com assinatura de tipo

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

Pode ser escrito como:

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

Answer 2

A melhor maneira é provavelmente desestruturar primeiro o par dependente, para que você possa simplesmente escrever:

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

Entretanto, se você realmente quiser manter o par dependente intacto na assinatura da função, você pode escrever um predicado PosN que inspeciona o primeiro elemento do par e verifica se ele é positivo:

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

ou similar.Deixarei a definição de PosN como exercício para o leitor.Essencialmente é isso que a resposta de Vitus já faz, mas em vez disso pode ser definido um predicado mais simples.

Answer 3

Depois de brincar com ele por algum tempo, descobri uma solução que se assemelha à função que eu queria em primeiro 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

Se alguém encontrar uma solução melhor (ou mais geral), aceitarei com prazer a resposta.Comentários também são bem-vindos.

---

Aqui está um predicado mais geral que criei:

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

Isso é como de costume head função para Vec.

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