伊德里斯热切评价

In Haskell，我可能会实施if像这样：

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

This 行为符合我的预期:

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

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

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

This 行为符合我的预期:

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

In 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

This 行为让我感到惊讶:

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

我期望 Irdis 表现得像 Racket，两个参数都是 评价。但事实并非如此！

伊德里斯如何决定何时评估事物？

我们说 Idris 具有严格的评估，但这是针对其运行时语义的。

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

为了方便起见，REPL 使用编译时求值概念。因此，您的“旋转 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 下不会减少。