agda – 如何使用依赖对

发布时间：2020-12-14 04:52:33 所属栏目：百科来源：网络整理

导读：假设我有一个函数(它真的做了名字所说的)： filter : ? {A n} → (A → Bool) → Vec A n → ? (λ m → Vec A m) 现在,我想以某种方式使用我返回的依赖对.我写了简单的头部功能： head :: ? {A} → ? (λ n → Vec A n) → Maybe Ahead (zero,_ ) = nothing

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

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

（编辑：李大同）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!