haskell - absurd 函数的逆

Question

absurd 是否存在相反的情况？函数来自 Data.Void ?

如果存在，它是如何实现的，它的用途是什么？

Answer 1

该功能不存在。 (假设严格语义)

看类型的代数，函数类型等价于求幂。

现在函数 absurd ，其类型为 Void -> a对应于操作a ^ 0等于 1 .这意味着 absurd 的实现只有一个。 ，可在 Data.Void 中找到.

反转箭头，您会得到类型 a -> Void ，对应于 0 ^ a或 0 ，这意味着所需的功能不存在。

您也可以使用 Curry-Howard 同构来证明这一点。由于函数类型对应于 bool 函数“隐含”，因此您得到以下术语:

True -> False

这是错误的，因此没有功能 a -> Void可以存在。

由于我刚开始学习范畴论，因此鼓励由于不精确的语言进行更正。