reflection - 反射(reflect)类型参数

Question

我正在尝试创建一个函数

import Language.Reflection
foo : Type -> TT

我尝试使用reflect 策略:

foo = proof
  {
    intro t
    reflect t
  }

但这反射(reflect)在变量 t 本身上:

*SOQuestion> foo
\t => P Bound (UN "t") (TType (UVar 41)) : Type -> TT

Answer 1

Idris 中的反射是一个纯句法的、仅编译时的特性。要预测它将如何工作，您需要了解 Idris 如何将您的程序转换为其核心语言。重要的是，您将无法像使用 Lisp 那样在运行时获取反射项并重建它们。以下是您的程序的编译方式:

1. 在内部，Idris 创建了一个孔，该孔将期望类型为 Type -> TT。
2. 它在此状态下运行 foo 的证明脚本。我们从没有假设和 Type -> TT 类型的目标开始。也就是说，正在构造一个看起来像 ?rhs : Type => TT 的术语。右侧。 ?foo : ty => body 语法显示有一个名为 foo 的漏洞，其最终值将在 body 中可用。
3. 步骤 intro t 创建了一个函数，其参数是 t : Type - 这意味着我们现在有一个像 ?foo_body : TT 这样的术语。\t : 输入 => foo_body。
4. 然后，reflect t 步骤通过获取右侧的项并将其转换为 TT 来填充当前的空洞。该术语实际上只是对函数参数的引用，因此您得到了变量 t。 reflect 与所有其他证明脚本步骤一样，只能访问在编译时直接可用的信息。因此，用t项的反射(reflect)填充foo_body的结果是P Bound (UN "t") (TType (UVar (-1)) )。

如果您可以在这里做您想做的事，那么对于理解 Idris 代码和高效运行它都会产生重大影响。

理解上的损失将来自无法使用参数化来推理基于函数类型的函数的行为。所有函数都将有效地成为潜在的临时多态性，因为它们可以(比如说)在字符串列表和整数列表上以不同的方式运行。

性能损失将来自表示足够的类型信息来进行反射。编译 Idris 代码后，其中没有类型信息(不像在 JVM 或 .NET 等系统或 Python 等动态类型系统中，类型具有代码可以访问的运行时表示)。在 Idris 中，类型可以非常大，因为它们可以包含任意程序 - 这意味着必须维护更多的信息，并且还必须在运行时保留和重复发生在类型级别的计算。

如果您想在编译时反射(reflection)类型的结构以进一步证明自动化，请查看applyTactic 策略。它的参数应该是一个函数，它接受一个反射的上下文和目标并返回一个新的反射策略脚本。可以看一个例子in the Data.Vect source .

所以我想总结一下，Idris 不能做你想做的事，它可能永远也做不到，但你可以通过其他方式取得进步。