伊德里斯真的“严格评估”吗？答案

【问题标题】：Is Idris really "strictly evaluated?"伊德里斯真的“严格评估”吗？
【发布时间】：2015-12-30 18:10:07
【问题描述】：

来自 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 repl，并再次运行myFact 5，期待无限递归。令我惊讶的是，它仍然以同样的方式工作！

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

我使用的是 Idris 0.9.15，从现在到链接的注释都没有发布说明，请提及任何更改。

【问题讨论】：

【解决方案1】：

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

但是，这里还有更多事情要做。 Idris 发现 myIf 是一个非常小的函数，并决定内联它。所以编译时myFact实际上有一个看起来有点像的定义：

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

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

【讨论】：

这种内联优化在改变语义时是否正确？
它没有改变语义。无论您采用哪种方式，所有输入都会得到相同的答案。
但是它改变了整体，这很难理解，特别是当用户切换到一些相似的编码风格时（例如一些改变使得代码不再小到可以内联），期望不会改变程序行为，但程序可能不再工作..
它不会改变整体... 编辑：啊，当然你的意思是它改变了这个特定表达式的终止，所以我应该详细说明一下：伊德里斯会想，不管它做什么优化，“myFact”不是全部。而且，无论如何，由于它不是全部，因此在类型检查时不会对其进行评估。有一个合理的论点是，它应该只在定义完整时才进行这种内联。