Haskell 的类型系统是不是同构于一个不一致的逻辑系统？如果是这样，后果是啥？

Posted 2023-05-08

【中文标题】Haskell 的类型系统是不是同构于一个不一致的逻辑系统？如果是这样，后果是啥？

【英文标题】：Is Haskell's type system isomorphic to an inconsistent logic system? If so, what are the consequences?Haskell 的类型系统是否同构于一个不一致的逻辑系统？如果是这样，后果是什么？

【发布时间】：2017-10-17 11:47:02

【问题描述】：

在Haskell中有一个术语undefined :: a，据说是一个术语 表示错误的计算或无限循环。由于undefined 有 输入a，他们可以创建任何语法正确的类型 应用类型替换。所以undefined 有任何类型，反之亦然：任何类型都有undefined，这是存在于任何类型内部的底部值（包括Void 类型，对吧？）。

Curry-Howard 同构给出的不仅仅是作为类型的命题，它还给出了作为定理的惯用类型。

将所有命题作为定理的逻辑系统称为不一致。

那么，Haskell 的类型系统同构于一个不一致的逻辑系统？

如果是这样，后果是什么？

如果 Haskell 的类型系统是一个不一致的证明系统，我们就不能信任它吗？

如果没有undefined，是否可以表示无限循环？

【问题讨论】：

好吧 undefined 有时被定义为 undefined = undefined... 所以它一直在评估.. 所以如果你想表示一个无限循环，你可以用 f = f 做到这一点。

undefined 的评估是一个例外。我不认为无限循环和异常意味着相同。但是有人可以证明我错了！ :)

@RafaelCastro：Haskell 语义通常定义为“从上到下”（或“到 ⊥”，带有符号）——所有的“底部”，也就是说非终止，值被认为是相同的. （我们让IO 以通常的不纯方式区分它们。）

@AntalSpector-Zabusky 感谢您提供的信息！

出于务实的原因，Haskell 编译器可以检测 一些 无限循环/递归并将它们转化为异常。这不会以任何方式影响库里-霍华德或任何其他理论。

【参考方案1】：

是的，逻辑不一致。

但是，这并不意味着类型系统没有用。例如，类型系统确保我们永远不会尝试添加整数和字符串，或者将第一个组件投影到布尔值之外。这些通常是某些无类型语言中的运行时类型错误。

我们仍然存在一些运行时错误，例如非详尽的模式匹配（我个人会禁止使用该语言 :-P）、error、undefined、异常等等。但至少我们没有类型相关的。我们也有非终止（通过无限递归），这在图灵完备语言中是一个必要的弊端，并且无论如何都会导致不一致。

最后，我认为即使在这种不一致的环境中，库里-霍华德也是有用的。例如。如果我想写f :: Either a b -> a，我可以立即发现这不是一个直觉定理，因此f 只能使用上述运行时错误来实现，所以一开始可能不是一个好主意，如果我需要这样f，我应该重新考虑我的设计。

拥有一个定义良好的 Haskell 的“总”片段是否也有用，具有相同的类型，但没有上面提到的坏事？绝对地！例如，它将允许将() 类型的任何表达式优化为值()——毕竟它必须对此进行评估。此外，e :: a :~: b 将类似地优化为类似unsafeCoerce Refl 的内容，从而可以编写只需要 O(1) 运行时成本的“类型之间相等的证明”。现在，不幸的是这样的证明必须在运行时进行评估，导致愚蠢的开销只是为了确保证明是“真实的”，而不是例如。伪装的undefined。

【讨论】：

我喜欢你的回答，但我想知道是否有任何不良后果。比如说，如果a -> b 类型有一个术语，那么该术语不是 unsafeCoerce 有什么保证？在一个永远不会被问到的一致逻辑中！

@RafaelCastro 挥手：forall a b. a -> b 类型的术语要么是 unsafeCoerce（我们假装不存在），要么是一些 ⊥，例如 let x = x in x。

@RafaelCastro 我想这取决于“Haskell”的定义。如果从非常广泛的意义上解释，包括低级原语、FFI 和其他一些“危险”的东西，那么我们确实会失去类型安全。我的意思是，FFI 让我们将数据发送到 C，将它们转换为其他类型，然后将它们返回到 Haskell。如果您包含类似的内容，则无法保证。甚至unsafePerformIO 也可以用来违反类型安全。不过，通常我们会假装这些东西不是 Haskell 的一部分。

你对“是的，逻辑不一致”的引用是什么？

@j4nbur53 没有，但是，正如 OP 所述，undefined :: a 证明了每个公式，所以它立即遵循。

【参考方案2】：

如果 Haskell 的类型系统是一个不一致的证明系统，那么我们就不能相信它？

正如@chi 所暗示的，类型安全 是一个比逻辑一致性 弱得多的条件。引用Types and Programming Languages（如果您对这类事情感兴趣，请阅读！），

安全 = 进步 + 保护

[...] 那么，我们想知道的是，键入良好的术语不会被卡住。我们分两个步骤来展示这一点，通常称为 progress 和 preservation 定理。

Progress：一个良好类型的术语没有被卡住（它要么是一个值，要么它可以根据评估规则迈出一步）。 保留：如果一个类型良好的术语进行了评估步骤，那么生成的术语也是类型良好的。

这些属性共同告诉我们，类型良好的术语在评估期间永远不会达到卡住状态。

请注意，这种类型安全的定义并不排除类型良好的术语将永远循环或抛出异常的可能性。但是这两条规则确实保证了如果您成功获得了Int，那么它确实是Int，而不是Bool、Spoon 或Ennui。 （在 Haskell 中，懒惰使这有点复杂，但基本思想仍然正确。）这是一个非常有用的属性，程序员学会在他们的日常工作流程中至关重要地依赖它！

请允许我跑题。正如逻辑上不一致但仍然类型安全的系统在实践中有用且值得信赖一样，类型不安全但仍然静态检查的系统在实践中也很有用（尽管有些人可能不愿称它们为“值得信赖”） .看看 javascript 生态系统，其中“渐进式”系统（如 TypeScript 和 Flow）旨在为工作程序员提供额外的支持层——因为 VanillaJS 即使在中型代码库中也是一场噩梦——没有做出大胆的承诺喜欢进步和保存。 （我听说 Python 和 php 社区也在逐渐（哈哈）采用类型。）TypeScript 仍然成功地捕获了我在编程时犯的大部分人为错误，并且支持大小不一的代码更改，尽管不是“正式意义上的类型安全”。

我想我的观点是，PL 社区倾向于非常重视证明系统的属性（例如类型安全），但这通常不是软件工程师获得他们的完成工作！我认识的工程师关心的是一个工具是否能帮助他们编写更少的错误，而不是它是否被证明是安全的或一致的。我只是认为每个小组都可以从彼此身上学到很多东西！当超类型社区的聪明人与非类型社区的聪明人一起构建工程工具时，interesting things can happen。

可以表示没有undefined 的无限循环吗？

当然。方法很多。

loop = loop
fib = 1 : 1 : zipWith (+) fib (tail fib)
repeat x = unfoldr (const (Just x))
main = forever $ print "cheese"

从正式的角度来看，所有这些术语都是 ⊥，但实际上，您运行的是哪个 ⊥ 非常重要。

如果您的问题真的是编写循环术语的能力是否意味着不一致？那么简短的回答是肯定的，即let x = x in x :: forall a. a。这就是为什么像 Agda 这样的证明助手通常具有一个终止检查器，它检查程序的语法并拒绝一般递归的可疑用法。更长的答案是no, not exactly - 您可以将程序的通用递归部分嵌入到 monad 中，然后使用一些外部评估器实现该偏向性 monad 的语义。 （这正是 Haskell 对纯度采取的方法：将不纯净的部分放在 IO monad 中，并将执行委托给运行时系统。）

总而言之，是的，Haskell 作为一种逻辑是不一致的——每种类型都包含一个无限的⊥s 家族，具有各种运行时行为，因此您可以轻松“证明”任何命题。这（以及依赖类型的整体笨拙）是人们不使用 Haskell 作为定理证明器的原因。不过，对于工程而言，类型安全的较少保证通常就足够了，其中一些 ⊥s 很有趣！

【讨论】：

我想买这本书……还有一个原因。您关于类型安全是一个更弱的条件的澄清是有帮助的。你猜对了我真正想要的关于没有undefined的无限循环的问题。

fib 和 repeat 从正式的角度来看绝对不是⊥。我不太确定main，但我认为也不是。

@AlexeyRomanov 你能详细说明一下吗？我的印象是，对 NF 的评估未能终止的任何术语都被视为⊥。

@TheOrgazoid 对于严格的语言，是的；对于 Haskell，将 NF 更改为 WHNF。正如 Antal Spector-Zabusky 对该问题的评论所说，“所有“底部”，即非终止值，都被认为是相同的”，但您可以在纯 Haskell 中区分 fib 和 undefined（没有 IO，@ 987654348@等）例如通过使用head。