Agda 函数，类型上的函数匹配

Question

我想创建一个辅助函数，它将从索引或参数化类型中获取一个术语并返回该类型参数。

showLen : {len :  ℕ} {A : Set} -> Vec A len -> ℕ
showLen ? = len

showType : {len :  ℕ} {A : Set} -> Vec A len -> Set
showType ? = A

这可能吗？ （我可以看到showType [] 可能有问题，但是当 Type 被索引时呢？）

Answer 1

如果你去掉隐含的参数，你可以很容易地实现它：

showLen : (len : ℕ) (A : Set) → Vec A len → ℕ
showLen len _ _ = len

事实上，我们可以同时做到这两点：

open import @987654321@

showBoth : (len : ℕ) (A : Set) → Vec A len → ℕ × Set
showBoth len A _ = len , A

现在，隐式参数就像普通参数一样，除了编译器会尝试自己填充它们。如果我们愿意或需要，我们总是可以覆盖此行为。

如果您想实现一个具有隐藏参数的函数并且您需要以某种方式访问​​它们，您可以通过在花括号内提及它们来实现，如下所示：

replicate : {n : ℕ} {A : Set} → A → Vec A n
replicate {zero}  _ = []
replicate {suc _} x = x ∷ replicate x

当你想调用一个函数并需要指定一个隐藏参数时，过程类似：

vec : Vec ℕ 4
vec = replicate {4} 0

现在，我们只需将其应用于上面给出的showBoth：

showBoth : {len : ℕ} {A : Set} → Vec A len → ℕ × Set
showBoth {len} {A} _ = len , A

---

现在，如果你的论点碰巧有错误的顺序；例如，您想明确给出 A 参数而不是 n 参数，您必须这样做：

vec₂ : Vec ℕ 4
vec₂ = replicate {_} {ℕ} 0

现在，如果您需要填写第 n 个隐式参数，这将很快变得乏味。因此，Agda 为我们提供了通过名称引用它们的选项：

vec₃ : Vec ℕ 4
vec₃ = replicate {A = ℕ} 0

这使用类型签名中给出的名称。您也可以在定义函数时使用它：

showType : {len : ℕ} {A : Set} → Vec A len → Set
showType {A = Type} _ = Type