haskell - 虚空是什么样的？

Question

鉴于Void类型无人居住，是否可以将其视为类型“构造函数”？或者这只是一个快速的“黑客”，以便能够安全地忽略/禁用功能，而我是否对此研究得太深了？

Answer 1

0曾经不被认为是一个数字。 "How can nothing be something?"但随着时间的推移，我们开始接受 0 作为一个数字，注意到它的属性和用途。如今，认为 0 不是数字的想法与 2000 年前认为 0 是数字的想法一样 absurd 。

Void是一种类型，就像 0 是一个数字一样。它的种类是* ，就像所有其他类型一样。 Void之间的相似度正如 Tikhon Jelvis 的答案开始表明的那样，0 运行得很深。类型和数字之间有很强的数学相似性，如 Either扮演加法、元组的角色(,)扮演乘法、函数的角色(->)作为求幂( a -> b 表示 b^a)， () (发音为“单位”)为 1，且 Void为 0。

类型可以采用的值的数量是该类型的数字解释。所以

Either () (Either () ())

被解释为

1 + (1 + 1)

所以我们应该期望三个值。确实是三个。

Left ()
Right (Left ())
Right (Right ())

同样，

(Either () (), Either () ())

被解释为

(1 + 1) * (1 + 1)

所以我们应该期望四个值。你能列出它们吗？

返回Void ，你可以有，比如说，Either () Void ，这将被解释为 1 + 0。这种类型的构造函数是 Left () ，和Right v对于每个值 v类型 Void -- 但是没有 Void 类型的值，所以 Either () Void 的唯一构造函数是 Left () 。 1 + 0 = 1，所以我们得到了我们所期望的。

练习: Maybe a 的数学解释应该是什么？是？ Maybe Void 有多少个值有没有——这符合解释吗？

注释

• 我忽略了这种处理的偏袒，假装 Haskell 是完整的。技术上undefined可以输入 Void ，但我们喜欢使用 fast and loose忽略这些的推理。
• 路 void用于基于C的语言实际上更像Haskell的()比 Haskell 的 Void 。在 Haskell 中，函数返回 Void根本无法返回，而在 C 中语言返回 void 的函数可以返回，但返回值无趣——它只能是一件事，所以为什么要麻烦呢？