颠倒荒谬的功能

Question

是否与absurd函数相反Data.Void？

如果它存在,它是如何实现的以及它用于什么？

Answer 1

此功能不存在.(假设严格的语义)

查看类型的代数,函数类型等效于取幂.

现在函数absurd,其类型Void -> a对应于a ^ 0等于的操作1.这意味着只有一个实现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.嗯,那令人兴奋......还有,恭喜你,你死了!

Hask(Haskell类型的类别,Haskell函数作为态射)是具有初始对象的bicartesian封闭类.初始对象的定义是,对于任何类型,只存在一个函数- 这些函数是实例.双重地,只存在一个函数,因为它是终端对象 - 任何这样的函数都等价于. VoidAVoid -> Aabsurd :: Void -> aB -> ()()const ()

现在,假设drusba :: () -> Void,我们会

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

因为只能有一个功能Void -> Void,我们知道id是一个功能; 和

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

出于同样的原因.IOW,drusba并且absurd确实是彼此正确的反转,这意味着()并且Void是同构的.

但是从这个它会遵循任何类型A实际上是同构既()和Void,因为那里将存在恰好一个功能() -> A及A -> ().

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

^† _{当然,如果你忽视⊥,这一切都只有.}