什么是虚空？
看到Void的types是无人居住的，它可以被看作是一个“构造函数”types吗？ 或者，这只是一个快速的“黑客”，能够安全地忽略/禁用function，我看起来太深了？
0曾经不被认为是一个数字。 “怎么可能是什么东西？” 但是随着时间的推移，我们接受了0作为一个数字，注意到它的属性和用处。 今天，0 不是数字的想法和2000年前的想法一样荒谬。
Void是一个types相同的方式0是一个数字。 它的types是* ，就像所有其他types一样。 Vik和0之间的相似度相当深，因为Tikhon Jelvis的回答开始显示。 在types和数字之间有一个很强的math类比，它们Either扮演着加法的angular色(,)扮演乘法的angular色，函数(-> ）指数（ a -> b表示b a ）， () （发音“unit”）为1， Void为0。
types可能需要的值的数量是types的数字解释。 所以
Either () (Either () ())
被解释为
1 + (1 + 1)
所以我们应该期待三个价值观。 确实有三个。
Left () Right (Left ()) Right (Right ())
同样的，
(Either () (), Either () ())
被解释为
(1 + 1) * (1 + 1)
所以我们应该期望四个值。 你能列出他们吗？
回到Void ，你可以说有Either () Void ，它将被解释为1 + 0.这个types的构造函数是Left ()和Right v对于Voidtypes的每个值v而言，没有Voidtypes的值，所以Either () Void的唯一构造函数是Left () 。 而1 + 0 = 1，所以我们得到了我们的预期。
练习 ： Maybe a的math解释应该是什么？ Maybe Void有多less个值 – 是否符合解释？
笔记
- 我忽略了这种治疗的偏好，假装Haskell是完全的。 从技术上来说，
undefined可以有Voidtypes，但是我们喜欢使用忽略这些的快速和宽松的推理。 - 在基于C的语言中使用
void的方式实际上比Haskell的()更像Haskell的Void。 在Haskell中，返回Void的函数根本就不能返回，而在C语言中，返回void的函数可以返回，但是返回值是无趣的 – 只有一件事情可以这样，为什么呢？
这是一种types*就像Int ， Bool或() 。 它恰好有0个值，而不是1或2或更多。
这不是破解，而是Haskelltypes系统的一个基本部分。 它扮演0到() 1的angular色，如果我们把types看作命题，虚拟对应于命题“假”。 它也是一个和types相同的标识（ Either ），就像()是一个产品types的标识一样： Either a Void同构于a 。
在实践中，它经常作为()对偶。 这个我见过的最好的例子是在pipe道 where ()用于标记不需要input的事物，而Void （名为X ）用于标记不产生输出的事物。 （请参阅附录：教程中的types 。）
这是标记事物不可能或缺失的一种方式，但绝不是黑客行为。
在这个问题上的另一个angular度：假设我要求你写一个types为a -> b的保证终止函数：
aintGonnaWork :: a -> b aintGonnaWork a = _
希望你能说出来，写这样一个函数是不可能的。 由此得出，typesa -> b没有定义的值。 还要注意， a -> b的种类是* ：
(->) :: * -> * -> * a :: * b :: * --------------------- a -> b :: *
我们有它：一种types* ，由“香草”哈斯克尔元素（没有“黑客”）构build，但没有定义的值。 所以类似Void的存在已经隐含在“香草”哈斯克尔中; 所有显式的Voidtypes都提供了一个标准的命名。
我将以上述方式简单地实现Voidtypes; 唯一需要的扩展是RankNTypes 。
{-# LANGUAGE RankNTypes #-} newtype Void = Void (forall a b. a -> b) absurd :: Void -> a absurd (Void f) = ff
