agda - 如何使用依赖对

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 的问题。标准库提供 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

现在你想要的功能只是一个 uncurrying 的问题
具有第一个参数-隐式非柯里化(Currying)的可能头函数
上面定义的函数:

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

结论:依赖产品很乐意像它们的非依赖版本一样 curry 和 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