3

我正在尝试创建一个函数

import Language.Reflection
foo : Type -> TT

我使用以下reflect策略进行了尝试：

foo = proof
  {
    intro t
    reflect t
  }

但这反映在变量t本身上：

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

1 回答 1

3

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

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

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

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

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

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

所以我想总结是，伊德里斯不能做你想做的事，而且它可能永远也做不到，但你也许可以通过另一种方式取得进展。

于 2015-01-26T04:29:36.513 回答