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 Data.Product

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