4

假设我有一个函数（它确实像名字所说的那样）：

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
4

4 回答 4

3

我认为这是一个关于 uncurrying 的问题。标准库为产品提供了 uncurrying 函数，请参阅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

现在，您想要的函数只是使用上面定义的 first-argument-implicit-uncurrying 函数对可能头函数进行非柯里化：

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
于 2012-03-14T10:14:45.370 回答
1

在玩了一段时间之后，我想出了类似于我最初想要的功能的解决方案：

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
  ...
于 2012-03-09T18:34:34.633 回答
1

最好的方法可能是首先解构依赖对，这样您就可以编写：

head :: ∀ {A n} → Vec A (S n) → A

然而，如果你真的想在函数签名中保持依赖对的完整性，你可以编写一个谓词 PosN 来检查对的第一个元素并检查它是否为正：

head :: ∀ {A p} → PosN p -> A

或类似的。我将把 PosN 的定义作为练习留给读者。本质上这就是 Vitus 的回答已经做了，但是可以定义一个更简单的谓词。

于 2012-03-09T21:31:01.620 回答
0

这就像head.Vec

head' : ∀ {α} {A : Set α} → ∃ (λ n → Vec A (suc n)) → A
head' (_ , x ∷ _) = x
于 2014-07-09T19:17:16.740 回答