agda – 如何使用依赖对

假设我有一个函数(它真的做了名字所说的)：

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

现在,我想以某种方式使用我返回的依赖对.我写了简单的头部功能：

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

这当然是完美的.但它让我想知道：有什么方法我可以确定,该功能只能在n≥1时调用吗？

理想情况下,我想制作函数头：∀{A}→∃(λn→Vec A n)→IsTrue(n≥succzero)→A;但是失败了,因为当我在IsTrue中使用它时,n超出了范围.

谢谢你的时间！

IsTrue是这样的：

data IsTrue : Bool → Set where
  check : IsTrue true

我认为这是一个关于不发生的问题.标准库提供了不受干扰
产品功能,见 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-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