对 Idris 中的惰性求值感到困惑

Question

阅读和尝试官方 Idris 教程中的一些示例让我对惰性求值有点困惑。

正如教程中所述，Idris 使用急切求值，他们继续给出了一个不合适的示例

ifThenElse : Bool -> a -> a -> a
ifThenElse True  t e = t
ifThenElse False t e = e

然后他们继续展示使用惰性求值的示例

ifThenElse : Bool -> Lazy a -> Lazy a -> a
ifThenElse True  t e = t
ifThenElse False t e = e

我喜欢边看书边尝试，所以我创建了一个低效的斐波那契函数来测试非懒惰和懒惰ifThenElse。

fibo : Nat -> Nat
fibo Z = Z
fibo (S Z) = S Z
fibo (S(S Z)) = S(S Z)
fibo (S(S(S n))) = fibo (S(S n)) + fibo (S n)

-- the non lazy
ifThenElse1 : Bool -> (t: a) -> (f: a) -> a
ifThenElse1 False t f = f
ifThenElse1 True t f = t

-- should be slow when applied to True
iftest1 : Bool -> Nat
iftest1 b = ifThenElse1 b (fibo 5) (fibo 25)

-- the lazy
ifThenElse2 : Bool -> (t: Lazy a) -> (f: Lazy a) -> a
ifThenElse2 False t f = f
ifThenElse2 True t f = t

-- should be fast when applied to True
iftest2 : Bool -> Nat
iftest2 b = ifThenElse2 b (fibo 5) (fibo 25)

鉴于 Idris 应该执行急切的评估，我预计 iftest1 的执行速度会减慢 (fibo 25)，即使应用于 True。但是，iftest1 和 iftest2 在应用于 True 时执行得非常快。所以也许我对 lazyness/eagerness 的理解存在根本性的缺陷？

观察 Idris 中懒惰和急切之间区别的一个很好的例子是什么？

Answer 1

您可能尝试了 Idris REPL 中的 iftest1 和 iftest2。 The REPL uses different evaluation order than compiled code:

Being a fully dependently typed language, Idris has two phases where it evaluates things, compile-time and run-time. At compile-time it will only evaluate things which it knows to be total (i.e. terminating and covering all possible inputs) in order to keep type checking decidable. The compile-time evaluator is part of the Idris kernel, and is implemented in Haskell using a HOAS (higher order abstract syntax) style representation of values. Since everything is known to have a normal form here, the evaluation strategy doesn’t actually matter because either way it will get the same answer, and in practice it will do whatever the Haskell run-time system chooses to do.

The REPL, for convenience, uses the compile-time notion of evaluation.

对 Idris 中的惰性求值感到困惑

confused about lazy evaluation in Idris

idris