lazy-evaluation - idris 真的是 "strictly evaluated?"

Question

来自 Haskell，我正在阅读 Idris 关于懒惰(非严格)的故事。我翻了翻最近的发行说明，还有 found code类似于以下

myIf : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a
myIf True t e = t
myIf False t e = e

我写了一个简单的阶乘函数来测试它

myFact : Int -> Int
myFact n = myIf (n == 1) 1 (n * myFact (n-1))

我跑了它，它奏效了!

> myFact 5
120 : Int

我决定通过改变 myIf 的类型签名来打破它到

myIf : (b : Bool) -> a -> a -> a

我重装了 idris复制，然后运行 ​​ myFact 5再次期待无限递归。令我惊讶的是，它仍然以同样的方式工作!

idris 能弄清楚什么时候应该避免严格吗？为什么这不会永远递归？

我正在使用 Idris 0.9.15 并且从现在到链接的注释之间没有任何发行说明，提及任何更改。

Answer 1

解释在这里:http://docs.idris-lang.org/en/latest/faq/faq.html#evaluation-at-the-repl-doesn-t-behave-as-i-expect-what-s-going-on

编译时和运行时评估语义是不同的(必然如此，因为在编译时类型检查器需要在存在未知值的情况下评估表达式)，并且 REPL 使用编译时概念，既是为了方便，也是因为它对查看表达式如何在类型检查器中减少。

然而，这里还有一些事情要做。 idris 发现了 myIf是一个非常小的函数，并决定内联它。所以编译时myFact实际上有一个看起来有点像的定义:

myFact x = case x == 1 of
                True => 1
                False => x * myFact (x - 1)

所以通常你可以编写像 myIf 这样的控制结构。不用担心做东西 Lazy ，因为无论如何 Idris 都会将它们编译成您想要的控制结构。同样适用于，例如 &&和 ||和短路。