Idris 热心求值

Question

在Haskell中，我可能会这样实现if语句：if。

if' True  x y = x
if' False x y = y
spin 0 = ()
spin n = spin (n - 1)

这个表现符合我的预期：

haskell> if' True  (spin 1000000) ()  -- takes a moment
haskell> if' False (spin 1000000) ()  -- immediate

在Racket中，我可以像这样实现一个有缺陷的if：

(define (if2 cond x y) (if cond x y))
(define (spin n) (if (= n 0) (void) (spin (- n 1))))

这个 表现符合我的预期：

racket> (if2 #t (spin 100000000) (void))  -- takes a moment
racket> (if2 #f (spin 100000000) (void))  -- takes a moment

在Idris中，我可以这样实现if：

if' : Bool -> a -> a -> a
if' True  x y = x
if' False x y = y
spin : Nat -> ()
spin Z = ()
spin (S n) = spin n

这个行为让我感到惊讶：

idris> if' True  (spin 1000) ()  -- takes a moment
idris> if' False (spin 1000) ()  -- immediate

我原以为Idris会像Racket一样对两个参数都进行求值，但事实并非如此！

Idris是如何决定何时对事物进行求值的？

- Snowball

Answer 1

虽然我们说Idris具有严格的求值方式，但这只适用于其运行时语义。

作为一个完全依赖类型的语言，Idris在评估事物时有两个阶段，编译时和运行时。在编译时，它只会评估它知道是完全的（即终止并覆盖所有可能的输入）以保持类型检查的可决定性。编译时求值器是Idris内核的一部分，使用Haskell实现，使用HOAS（高阶抽象语法）样式表示值。由于这里已知每个值都有正常形式，所以求值策略实际上并不重要，因为无论如何都会得到相同的答案，在实践中它会执行Haskell运行时系统选择执行的操作。

为了方便起见，REPL使用编译时的求值方式。因此，“spin 1000”实际上从未被评估过。如果你用相同的代码生成可执行文件，我预计会看到非常不同的行为。

除了更易于实现（因为我们有可用的求值器），这也非常有用，可以显示类型检查程序的项如何进行求值。所以你可以看到：

Idris> \n, m => (S n) + m
\n => \m => S (plus n m) : Nat -> Nat -> Nat

Idris> \n, m => n + (S m)
\n => \m => plus n (S m) : Nat -> Nat -> Nat

如果我们在 REPL 中使用运行时评估，这将更加困难（尽管不是不可能），因为它不能在 lambda 下减少。

- Edwin Brady

---

谢谢！我不得不将 spin : Nat -> () 更改为 spin : Nat -> Bool（我猜想 Idris 意识到 () 只有一个 inhabitant 并优化了对 spin 的调用），但在那之后，无论进入 if 的哪个分支，可执行文件都需要一段时间才能运行。 - Snowball

是的，它会擦除括号中的内容。实际上，在当前的主分支中，它进行了更深入的擦除分析，因此您可能需要执行类似于打印自旋 n 的结果以确保其被评估的操作... - Edwin Brady

为什么即使已知spin 1000是终止的且没有副作用，这个表达式也不会在编译时被计算并在生成的代码中被其结果替换，以便两个版本的if行在运行时立即返回它们的结果呢？（Snowballs上面的评论表明它并没有这样做。） - Lii

确定编译时求值是否明智并不容易，即使知道某些东西是确定的 - 结果可能会比输入更大，或者复制一些中间值，例如。编译器可能可以做更多的事情，但通常内联需要细心处理。 - Edwin Brady