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

Question

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

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

由于undefined 的存在，评估f 1 会引发错误，因此肯定会发生一些评估。不过，目前尚不清楚评估的深度。有时它似乎需要评估所有对返回()的函数的调用。示例：

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 时遇到了实际问题。原始应用程序具有多种类型的相互递归结构，并且代码在 1..6 或 7 中为 N 声明了许多称为 assert_structureN_is_correct 的函数，如果结构确实正确，则每个函数都返回单位，如果它不是。此外，这些函数在分解正确性条件时相互调用。在 Haskell 中，使用 Either String monad 可以更好地处理这个问题，所以我以这种方式转录它，但作为理论问题的问题仍然存在。感谢所有输入和回复。

Answer 1

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

这不是 Haskell 的工作方式。在 Haskell 中，每种类型都有一个值，即 no 值、错误或所谓的“底部”，由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：

“评估%case [表达式] 会强制评估正在测试的表达式（“审查员”）。审查员的值绑定到%of 关键字后面的变量，...”。

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

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

---

^(*)print x = putStr (show x) 和 show () = "()"，因此可以完全编译掉 show 调用。

这个值确实是提前知道的()，甚至show ()的值也提前知道是"()"。仍然接受的 Haskell 语义要求 (f 1) 的值在继续打印预先知道的字符串 "()" 之前被强制为弱头部正常形式。

---

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

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

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

edit2：print $ h (f 1) == _Case (h (f 1)) _Of () -> print () 并且只有h 是强制的，而不是f；并且根据h _ = () 的定义，产生its 答案h 不必强制执行任何操作。

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

您可以用您最喜欢的语言自己实现它，以感受一下。但是我们也可以仔细追踪任何表达式的求值，当它们出现时，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 部分说

case 表达式的语义[在图 3.1-3.3 中给出]。任何实现都应该表现得使这些身份保持[...]。

和(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′ } =  ⊥

因此评估的总体结果是⊥。