伊德里斯急切评价

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内核的一部分,并使用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上使用运行时评估,那将会更难(尽管不是不可能),在lambdas下不会减少.