ADT 理论或它在编程语言中的处理方式真的有问题吗？

Question

我不是数学家，但我觉得存在一些逻辑问题。

让我们从 ADT 原语开始，例如“unit”类型。它应该在类型集的上下文中扮演“1”的角色。但实际上，我们在 C、C++ 等中看到“unit”类型通常被称为“void”等价物。同时我们在 ADT 中有自己的“void”类型，它扮演“0”的角色，实际上定义自身的 NO 值。

对此的一些观点听起来像“单元类型不带来任何信息，因此它是无用的，我们可以将其视为 void-like”。但是 C void 等价物在哪里？或者，void = unit，“0=1”？引入一些悖论是个坏主意。

然后，让我们更深入。单位类型只定义一个值，好吧。但是，为什么在 ADT 理论中

unit + unit = 2*unit

我们什么时候应该得到单位？ “+”的工作方式类似于“或”定义我们称为变体类型的类型。 “单位或单位”绝对不会给我们“位”，或者任何更复杂的东西来继续。

提到 haskell 元组，它甚至没有单个元素的元组，但可以为空。 所以它也来自ADT理论。元组是项类型的乘法，因此一个元素元组与那个裸元素相同，空元组是单位值（）。

a == (a) == ((a)) == ...
() == (()) == ...

所以，这里有一个悖论：空元组的长度是多少？可以看到，它的长度同时是零和一……

Answer 1

首先，我们需要忽略类 C 语言等：它们甚至不尝试匹配数学基础。

Haskell 和其他函数式语言确实尝试过这一点，虽然它们的同构如何工作通常并不明显。

然后，让我们更深入。单位类型只定义一个值，好吧。但是，为什么在 ADT 理论中

unit + unit = 2*unit

我们什么时候应该得到单位？ “+”的工作方式类似于“或”定义我们称为变体类型的类型。 “单位或单位”绝对不会给我们“位”或任何更复杂的东西来继续。

嗯，是的，它确实给了我们一些东西。

type Bit = Either () ()

(||), (&&) :: Bit -> Bit -> Bit

(Left()) || (Left()) = Left()
_ || _ = Right()

(Right()) && (Right()) = Right()
_ && _ = Left()

如果你不相信它有效：

Prelude Acme.Missiles> type Bit = Either () ()
Prelude Acme.Missiles> let [true, false] = [Left (), Right ()] :: [Bit]
Prelude Acme.Missiles> if true==false then launchMissiles else return ()
正在加载包 stm-2.4.2 ... 正在链接 ... 完成。
正在加载包 acme-missiles-0.3 ... 正在链接 ... 完成。
Prelude Acme.Missiles>

啊，谢天谢地，我们还活着……

---

至于“嵌套单元元组”：那些只是代表1ⁿ ≡ 1.

---

当我们真正考虑零类型时，也许事情会变得更清楚。

{-# LANGUAGE EmptyDataDecls #-}

data Void

现在，让我们来看看最简单的情况：

• 0*0 = 0。由于我们无法为元组的任一侧提供值，因此我们无法定义 (Void, Void) ≅ Void 类型的值。
• 0+0 = 0。虽然Either 提供了两个构造函数，但都需要一个我们无法提供的Void 参数，所以我们仍然有Either Void Void ≅ Void。
• 0*1 = 0。我们无法构造(Void, ())，因为我们无法为fst 提供值。
• 0+1 = 1。啊哈！我们不能构造Left，但我们可以构造Right ()！所以Either Void () ≅ ()，因为那是这种类型的单一值。
• 1*1 = 1。元组的两边只能取值()。
• 1+1 = 2。这就是我上面讨论的情况，它具有不同的值 Left () 和 Right ()。
• 2+3 = ... 该死，I've chosen the wrong programming language for explaining this! 顺便说一句，⟂ 就出来了...