什么是空虚？

Question

考虑到Void的类型是无人居住的，它能被看作是一种类型的“构造函数”吗？或者这仅仅是一个快速的“黑客”，能够安全地忽略/禁用功能，而我是否对此看得太深了？

Answer 1

这是一种类型的*，就像Int，Bool或()一样。它只是碰巧有0值，而不是1或2或更多。

这不是黑客，而是Haskell类型系统的基本部分。它对()的1起0的作用，当我们把类型看作命题时，Void对应于命题"false“，它也是和类型(Either)的恒等式，就像()是乘积类型的恒等式：Either a Void与a同构。

在实践中，它常常充当()的双重角色；我在喉管中看到的最好的例子是在喉管中，()用于标记不接受输入的东西，而Void (命名为X)用于标记不产生输出的事物。(请参阅本教程中的附录:类型。)

这是一种将事物标记为不可能或缺失的方式，但它绝不是一次黑客攻击。

Answer 2

关于这个问题的另一个角度:假设我要求您编写一个类型为a -> b的有保证的终止函数。

aintGonnaWork :: a -> b
aintGonnaWork a = _

希望您能知道，编写这样的函数是不可能的。因此，类型a -> b没有定义值。还请注意，这类a -> b是*。

(->)   :: * -> * -> *
a      :: *
b      :: *
---------------------
a -> b :: *

我们有了它:一种由“香草”Haskell元素(没有“hack”)构建的*，但是它没有定义的值。因此，像Void这样的类型的存在已经隐含在"vanilla“Haskell中；显式Void类型所做的只是提供了一个标准，名为one。

最后，我将根据上面的内容简单地实现Void类型；唯一需要的扩展是RankNTypes。

{-# LANGUAGE RankNTypes #-}

newtype Void = Void (forall a b. a -> b)

absurd :: Void -> a
absurd (Void f) = f f

Answer 3

路易斯·卡西利亚斯( Luis )表明，香草Haskell的多态型可能无人居住。但也有一些无人居住的单形类型。经典的一个看起来是这样的：

data Void = Void !Void

absurd :: Void -> a
absurd (Void x) = absurd x

想象一下，试图构造Void类型的东西。

void :: Void
void = Void _

你需要一些Void类型的东西来填补这个洞。因为这就是void的全部要点，所以唯一明智的选择是

void :: Void
void = Void void

如果Void构造函数是惰性的，那将是一个周期性的结构Void (Void (Void ...))。但是由于它是严格的，所以void可以等效地写成

void = void `seq` Void void

显然是不会飞的。