如何使用依赖对

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

我认为这是一个关于uncurrying的问题。标准库提供了非货币化 产品功能，请参阅 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函数带有第一个参数-隐式-uncurrying 上面定义的函数:

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

结论:依赖产品欣然咖喱和uncurry喜欢他们的非依赖版本。

撇开不谈，你想用类型签名写的函数

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的定义留给读者.本质上这就是Vitus的答案已经做的，但是可以定义一个更简单的谓词。

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