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

Question

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

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

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

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

unit + unit = 2*unit

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

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

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

所以，这里的一个悖论是:空元组的长度是多少？正如你所看到的，它的长度同时为零和一......

Answer 1

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

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

Then, lets go deeper. Unit type defines only one value, okay. But, why in ADT theory

unit + unit = 2*unit

when we should get unit? "+" works like "or" defining type that we know as variant types. "unit or unit" definitely doesn't give us "bits", or anything more complex to continue.

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

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 ()
Loading package stm-2.4.2 ... linking ... done.
Loading package acme-missiles-0.3 ... linking ... done.
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()!所以要么 Void () ≅ ()，因为那是该类型的单个值。
• 1*1 = 1。元组两边只能取值()。
• 1+1 = 2。这就是我上面讨论的情况，它具有不同的值 Left () 和 Right ()。
• 2+3 = ... 该死的，I've chosen the wrong programming language for explaining this! 顺便说一句，⟂ 就出来了......