Idris热切评价

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表现得像球拍一样，这两个参数都会被评估。但事实并非如此！

Idris是如何决定何时对事物进行评估的？

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中使用运行时评估，这将更加困难(虽然不是不可能)，因为REPL不会减少lambda下的运行时评估。