Как использовать зависимые пары

Question

Предположим, у меня есть функция (она действительно выполняет то, что говорит название):

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

Теперь я хотел бы как-то поработать с зависимой парой, которую я возвращаю.Я написал простую head функцию:

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

, которая, конечно, прекрасно работает.Но это заставило меня задуматься: могу ли я быть уверенным, что функцию можно вызывать только с n ≥ 1?

В идеале я хотел бы сделать функцию head : ∀ {A} → ∃ (λ n → Vec A n) → IsTrue (n ≥ succ zero) → A;но это терпит неудачу, потому что n выходит за рамки, когда я использую его в IsTrue.

Спасибо за ваше время!

---

IsTrue что-то вроде:

data IsTrue : Bool → Set where
  check : IsTrue true

Answer 1

Я думаю, что это вопрос о неспешности.Стандартная библиотека предоставляет функции для быстрого вывода продуктов, см. uncurry .В вашей ситуации было бы более полезно иметь функцию uncurry, в которой первый аргумент скрыт, поскольку функция head обычно принимает индекс длины в качестве неявного аргумента.Мы можем написать функцию uncurry следующим образом:

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

Функция, которая возвращает заголовок вектора, если он есть, кажется, не существует в стандартной библиотеке, поэтому мы пишем один:

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

Теперь желаемая функция - это просто вопрос выполнения функции Maybe-Head с помощью функции first-arguments-implicit-uncurry, определенной выше:

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

Вывод: зависимые продукты с удовольствием каррируют и не работаюткак и их независимые версии.

Не обращая внимания, функция, которую вы хотите написать с сигнатурой типа

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

Может быть записана как:

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

Answer 2

Лучшим способом, вероятно, является сначала деструктурировать зависимую пару, так что вы можете просто написать:

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

Однако, если вы действительно хотите сохранить зависимую пару нетронутой в сигнатуре функции, вы можете написать предикат PosN, который проверяет первый элемент пары и проверяет его положительность:

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

или аналогичный. Я оставлю определение PosN как упражнение для читателя. По сути, это то, что ответ Витуса уже делает, но вместо этого можно определить более простой предикат.

Answer 3

Поработав некоторое время, я нашел решение, которое в первую очередь напоминает функцию, которую я хотел:

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

Если кто-нибудь придумает лучшее (или более общее) решение, я с радостью приму их ответ. Комментарии тоже приветствуются.

---

Вот более общий предикат, который я придумал:

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

Это похоже на обычную функцию head для Vec.

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