伊德里斯是否真的"严格评估？"

Question

来自哈斯克尔,我正在阅读有关伊德里斯关于懒惰(非严格性)的故事.我拖着最近的发行说明,找到了代码类似于以下的

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

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

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

我重新加载了idrisrepl,并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上

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

但是,这里还有更多.伊德里斯发现这myIf是一个非常小的功能,并决定内联它.所以编译时myFact实际上有一个看起来有点像的定义:

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

所以一般来说你可以编写控制结构,myIf而不必担心制作东西Lazy,因为Idris会将它们编译成你想要的控制结构.同样适用于例如&&和||短路.