荒谬函数的逆

Question

Data.Void 中的 absurd 函数是否存在反函数？

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

Answer 1

此函数不存在。（假设语义严格）

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

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

反转箭头，得到a -> Void类型，对应0 ^ a或0，表示所需功能不存在。

---

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

True -> False

这是假的，因此没有函数a -> Void可以存在。

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

Answer 2

这取决于你的意思。 absurd 见证了同构 Void = forall a.a 的一侧，从那个角度来看，有一个逆向

void :: (forall a.a) -> Void
void x = x

这确实是同构。

类型没有全函数

 forall a.a -> Void

在偏函数中也没有与 absurd 的任何逆类型。

Answer 3

很直观，这个函数不可能存在^†。假设我们有这样一个函数：

drusba :: a -> Void

那你就可以了

GHCi> drusba (5 :: Int)

...从而创建Void 类型的值。 Well, that's exciting... also, congratulations, you're dead!

Hask（Haskell 类型的范畴，以 Haskell 函数作为态射）是 bicartesian closed category 和 initial object Void。初始对象的定义是，对于任何类型的A，只存在一个函数Void -> A——这些函数是absurd :: Void -> a 的实例化。双重的，只有一个函数B -> ()，因为()是终端对象——任何这样的函数都等价于const ()。

现在，假设drusba :: () -> Void，我们将有

drusba . absurd :: Void -> Void
drusba . absurd ≡ id

因为Void -> Void只能有一个函数，而我们知道id是一个；和

absurd . drusba :: () -> ()
absurd . drusba ≡ id

出于同样的原因。 IOW，drusba 和 absurd 确实是彼此的正确逆，这意味着 () 和 Void 是同构的。

但由此可以得出 any 类型 A 实际上与 () 和 Void 同构，因为将只存在一个函数 () -> A 和 A -> ()。

所以基本上，如果存在一个函数drusba :: a -> Void，这意味着 Haskell 只有一种类型，它不包含任何值。那不会是一种特别有用的编程语言，不是吗？

---

^†_{当然，这一切只有在你无视⊥的情况下才成立。}