haskell - Control.Exception.evaluate 对等效函数生成的 thunk 的处理方式不同

Question

这里有两个等价的偏函数：

• \True -> \() -> ()
• \True () -> ()

应用任何一个都False应该引发PatternMatchFail异常。

当我使用Control.Exception.evaluate强制从前者到 WHNF 的 thunk 时，它会强制PatternMatchFail异常：

ghci> _ <- evaluate $ (\True -> \() -> ()) False
*** Exception: <interactive>:10:18-35: Non-exhaustive patterns in lambda

当我使用后一种形式时，它不会：

ghci> _ <- evaluate $ (\True () -> ()) False

为什么不？

（在 GHC-8.0.1 上）

Answer 1

来自 Haskell 2010 年的报告：

以下身份成立：

\ p1 … pn -> e    =   \ x1 … xn -> case (x1, …, xn) of (p1, …, pn) -> e

https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-260003.3

所以\True () -> e去糖\x y -> case (x, y) of (True, ()) -> e，在部分应用之后False是\y -> case (False, y) of ...一个函数抽象，所以这不是底部。

相反，\True -> f(where f = \() -> e) 脱糖为\x -> case x of True -> ...，但也有例外。