伊德里斯热切评价

Question

在 Haskell 中，我可能会像这样实现 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

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

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

Answer 1

我们说 Idris 有严格的评估，但这是为了它的运行时语义。

作为一种完全依赖类型的语言，Idris 有两个阶段来评估事物，编译时和运行时。在编译时，它只会评估它知道的全部内容（即终止并覆盖所有可能的输入），以保持类型检查的可判定性。编译时评估器是 Idris 内核的一部分，并在 Haskell 中使用 HOAS（高阶抽象语法）样式的值表示来实现。由于这里的所有内容都具有范式，因此评估策略实际上并不重要，因为无论哪种方式它都会得到相同的答案，并且实际上它会执行 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 中使用运行时评估，这将更难（尽管并非不可能），这在 lambdas 下不会减少。