惰性求值环境下，Void与()类型是否同构？

我之前在Stack Exchange上提过相关问题，评论和回答暗示Void和()能扮演相同角色。我一直认为()是运行时不携带信息的实体，而Void是运行时无法存在的类型。讨论中提到了undefined，还指出惰性求值对二者行为等价性的重要性。

我的理解是：

• Void仅有一个值：undefined（或error ""这类异常值）
• ()有两个值：()本身和undefined
• 由于undefined的存在，二者无法被区分；对()类型的值进行模式匹配时，若传入undefined会导致运行时错误

请问二者是否本质等价？此处的“等价”指如同newtype Bar = Bar Foo这样的类型等价性。

我通过以下可正常编译运行的代码对此有一定认知，但仍对此概念存疑：

foo :: Void -> String
foo _ = "foo"

bar :: Void -> String
bar undefined = "bar"

baz :: () -> String
baz () = "baz"

qux :: () -> String
qux _ = "qux"

void2unit :: Void -> ()
void2unit _ = ()

unit2void :: () -> Void
unit2void () = undefined

main :: IO ()
main = do
  let unit = undefined in print $ foo unit
  let unit = undefined in print $ bar unit
  let unit = ()        in print $ baz unit
  let unit = undefined in print $ qux unit
  print $ void2unit $ unit2void -- not once
        $ void2unit $ unit2void -- not twice
        $ void2unit $ unit2void -- but thrice
        () -- prints () indeed

从类型理论的严格定义来看，Void和()完全不等价：

• Void是空类型，没有合法的构造器（所有被当作Void的值都是异常或未定义值）；而()是单位类型，有且仅有一个合法构造器()。
• 你提到的newtype等价是编译期的类型同构，底层运行时表示完全一致，但Void和()的合法值集合天差地别，不可能属于这种等价关系。

不过在Haskell的惰性求值运行时中，二者确实存在行为上的相似性：

1. 用undefined在两种类型间转换时不会立刻报错——惰性求值会推迟计算，直到必须获取具体值的时刻才会触发异常。比如unit2void () = undefined，只要不强迫这个Void值“暴露”构造器（而Void本来就没有构造器），程序就不会崩溃。
2. 在不区分合法值和异常值的场景下，两者的行为难以区分：比如用_匹配任意值时，不管是Void的undefined还是()的undefined，都会执行同一个分支。

但这种相似性只是运行时行为的近似，绝非类型层面的等价：

• 对()的合法值()做模式匹配，程序能正常执行；但你永远无法对Void的“合法值”做模式匹配（因为根本不存在）。
• 从语义意图看，Void的核心作用是标记“不可能发生的情况”（比如永远不会返回的函数），而()用来标记“没有额外信息”，二者的设计目的完全不同。

内容的提问来源于stack exchange，提问作者Enlico