假设我有一个函数(它真的做了名字所说的)：
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.
对于您的情况,在第一个函数中使用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
