Agda 函数，类型上的函数匹配 [英] Agda functions, function matching on types

问题描述

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

I want to create a helper function, that will take a term from a an indexed or parametrized type and return that type parameter.

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

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

这可能吗?(我可以看到 showType [] 可能有什么问题，但是当 Type 被索引时呢?)

Is this possible? (I can see how showType [] might have issues, but what about when the Type is indexed?)

推荐答案

如果去掉隐式参数，就可以很容易地实现:

If you get rid of the implicit arguments, you can implement this quite easily:

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

事实上，我们可以同时做到:

In fact, we can do both at once:

open import Data.Product

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

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

Now, implicit arguments are just like normal arguments save for the fact that compiler will try to fill them on its own. We can always override this behaviour if we want or need to.

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

If you want to implement a function that has hidden arguments and you somehow need to access them, you can do so by mentioning them inside curly braces, like this:

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

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

When you then want to call a function and need to specify a hidden argument, the process is similar:

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

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

Now, we just apply this to showBoth given above:

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

<小时>

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

---

Now, if your arguments happen to be in wrong order; for example you'd like to explicitly give the A argument but not the n argument, you'd have to do this:

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

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

Now, if you needed to fill in n-th implicit argument, this would get tedious very quickly. So, Agda gives us the option to refer to them by a name:

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

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

This uses the name given in the type signature. You can also use this when defining a function:

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

这篇关于Agda 函数，类型上的函数匹配的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！