了解 Agda 中的 unquoteDecl答案

【问题标题】：Understanding unquoteDecl in Agda了解 Agda 中的 unquoteDecl
【发布时间】：2017-08-26 00:12:10
【问题描述】：

我试图理解 Agda 内置的反射机制，所以我决定编写一个简单的函数，它接受一个字符串作为标识符，一个带引号的类型和一个带引号的术语，并简单地定义具有给定字符串标识符的给定类型的术语。因此，我写了以下内容：

testDefineName' : String → TC Type → TC Term → TC ⊤
testDefineName' s t a =
   bindTC (freshName s)
     (λ n → bindTC t
     (λ t' → bindTC a
     (λ a' → (bindTC (declareDef (arg (arg-info visible relevant) n) t')
     (λ _ → defineFun n ((clause [] a') ∷ []))))))

unquoteDecl = (testDefineName' "test" (quoteTC ℕ) (quoteTC zero))

这种类型检查，但是，当我尝试在其他地方使用“测试”时，我得到一个 Not in scope: test 错误。

unquoteDecl 的 documentation 有点不透明。显然声明应采用以下形式

unquoteDecl x_1 x_2 ... x_n = m

其中x_i 是Names，而m 的类型为TC \top，所以也许我试图做的实际上是不可能的，但我仍然不明白这个机制是如何工作的：如果m 必须是TC ⊤ 类型，因此不能是名称x_1 x_2 ... x_n 的函数，我根本看不出如何使用unquoteDecl 将任何新名称带入范围！

所以，总结一下：

是否可以使用 Agda 的反射机制定义像我这样的函数，以便我可以使用 String 参数将新名称带入范围？我想要的是这样的：

<boilerplate code for unquoting> testDefineName' "test" (quoteTC ℕ) (quoteTC zero)
test' : ℕ
test' = test

编译（即我实际上可以使用新名称“test”）

如果不是，m 可以通过什么机制使用名称x_1 ... x_n？与文档相反，m 真的可以有像 List Name → TC ⊤ 这样的类型吗？

【问题讨论】：

请在此类帖子中包含导入语句列表。

标签： agda

【解决方案1】：

基于the way Ulf uses unquoteDecl，我的印象是您需要在 LHS 上列出将扩大范围的名称。

您的设置的问题是您不知道Name，因为您从String 生成一个新的并且无法获得它AFAIK。我的印象是freshName 只应该用于从战术内部生成内部名称。

如果您将testDefineName' 设为Name 而不是String，则一切正常：

testDefineName' : Name → TC Type → TC Term → TC ⊤
testDefineName' n t a = bindTC t
               $ λ t' → bindTC a
               $ λ a' → bindTC (declareDef (arg (arg-info visible relevant) n) t')
               $ λ _  → defineFun n ((clause [] a') ∷ [])

unquoteDecl test = testDefineName' test (quoteTC ℕ) (quoteTC zero)

【讨论】：