haskell - 在 Haskell 中评估函数 a -> () 有什么规则？

Question

正如标题所说:有什么保证可以评估 Haskell 函数返回单元？有人会认为在这种情况下不需要运行任何类型的评估，编译器可以立即用 () 替换所有此类调用。值，除非存在明确的严格要求，在这种情况下，代码可能必须决定是否应该返回 ()或底部。
我在 GHCi 中对此进行了实验，但似乎发生了相反的情况，即似乎对这样的函数进行了评估。一个非常原始的例子是

f :: a -> ()
f _ = undefined

评估 f 1由于存在 undefined 引发错误，所以肯定会发生一些评估。不过，目前尚不清楚评估的深度。有时，它似乎深入到评估所有对返回 () 的函数的调用所必需的程度。 .例子:

g :: [a] -> ()
g [] = ()
g (_:xs) = g xs

如果显示 g (let x = 1:x in x)，此代码将无限循环。 .但是之后

f :: a -> ()
f _ = undefined
h :: a -> ()
h _ = ()

可以用来表示h (f 1)返回 () ，因此在这种情况下，并非所有单位值子表达式都被计算。这里的一般规则是什么？

ETA:我当然知道懒惰。我在问是什么阻止了编译器编写者使这种特殊情况比通常可能的更懒惰。

ETA2:示例摘要:GHC 似乎可以治疗 ()与任何其他类型完全一样，即好像存在关于应该从函数返回哪个类型的常规值的问题。优化算法似乎没有(ab)使用只有一个这样的值这一事实。

ETA3:当我说 Haskell 时，我指的是 Haskell-as-defined-by-the-Report，而不是 Haskell-the-H-in-GHC。似乎是一个没有像我想象的那样广泛共享的假设(这是“100% 的读者”)，或者我可能能够提出一个更清晰的问题。即便如此，我还是很遗憾更改了问题的标题，因为它最初询问了调用这样的函数有什么保证。

ETA4:看来这个问题已经结束了，我认为它没有答案。 (我一直在寻找一个“关闭问题”功能，但只找到了“回答你自己的问题”，由于无法回答，我没有走那条路。)没有人从报告中提出任何可以决定它的东西，我很想将其解释为一个强有力但不确定的“不能保证这种语言”的答案。我们所知道的是，当前的 GHC 实现不会跳过对此类函数的评估。

在将 OCaml 应用程序移植到 Haskell 时，我遇到了实际问题。原始应用程序具有多种类型的相互递归结构，并且代码声明了许多称为 assert_structureN_is_correct 的函数。对于 1..6 或 7 中的 N，如果结构确实正确，则每个都返回单位，如果不正确则抛出异常。此外，这些函数在分解正确性条件时相互调用。在 Haskell 中，最好使用 Either String 来处理。 monad，所以我是这样转录的，但是作为一个理论问题的问题仍然存在。感谢所有输入和回复。

Answer 1

您似乎来自 () 类型的假设。只有一个可能的值，() ，因此期望任何函数调用返回类型为 () 的值应该自动假定确实产生了值 () .

这不是 Haskell 的工作方式。在 Haskell 中，每种类型都有一个值，即无值、错误或所谓的“底部”，由 undefined 编码.因此，实际上正在进行评估:

main = print (f 1)

相当于核心语言的

main = _Case (f 1) _Of x -> print x   -- pseudocode illustration

甚至(*)

main = _Case (f 1) _Of x -> putStr "()"

和Core的_Case是 forcing :

"Evaluating a %case [expression] forces the evaluation of the expression being tested (the “scrutinee”). The value of the scrutinee is bound to the variable following the %of keyword, ...".

该值被强制为弱头正常形式。这是语言定义的一部分。

Haskell 不是一种声明式编程语言。

(*) print x = putStr (show x)和 show () = "()" ，所以 show call 可以完全编译掉。

该值确实提前知道为 () ，甚至 show () 的值提前被称为 "()" .仍然公认的 Haskell 语义要求 (f 1) 的值在继续打印预先知道的字符串 "()" 之前，被强制转换为弱头正常形式.

编辑:考虑concat (repeat []) .应该是[] ，还是应该是无限循环？

“声明性语言”对此的回答很可能是 [] . Haskell 的答案是无限循环。

懒惰是“穷人的声明式编程”，但它仍然不是真正的东西。

编辑2:print $ h (f 1) == _Case (h (f 1)) _Of () -> print ()并且只有 h是强制的，而不是 f ;并给出答案h根据其定义 h _ = () 不必强加任何东西.

临别感言:懒惰可能有存在的理由，但这不是它的定义。懒惰就是这样。它被定义为所有值最初都是根据来自 main 的要求强制为 WHNF 的 thunk。 .如果它有助于根据其具体情况在某种特定情况下避免触底，那么它确实如此。如果不是，则不是。就这些。

它有助于以您最喜欢的语言自己实现它，以感受它。但是我们也可以通过仔细naming all interim values 来跟踪任何表达式的求值。当它们出现时。

通过 the Report ， 我们有

f :: a -> ()
f = \_ -> (undefined :: ())

然后

print (f 1)
 = print ((\ _ ->  undefined :: ()) 1)
 = print          (undefined :: ())
 = putStrLn (show (undefined :: ()))

与

instance Show () where
    show :: () -> String
    show x = case x of () -> "()"

它继续

 = putStrLn (case (undefined :: ()) of () -> "()")

现在，3.17.3 Formal Semantics of Pattern Matching 部分报告说

The semantics of case expressions [are given] in Figures 3.1–3.3. Any implementation should behave so that these identities hold [...].

和案例(r)在 Figure 3.2状态

(r)     case ⊥ of { K x1 … xn -> e; _ -> e′ } =  ⊥
        where K is a data constructor of arity n 

()是 arity 0 的数据构造函数，所以它与

(r)     case ⊥ of { () -> e; _ -> e′ } =  ⊥

因此，评估的总体结果是⊥ .