库里在 Haskell 中的悖论？答案

【问题标题】：Curry's paradox in Haskell?库里在 Haskell 中的悖论？
【发布时间】：2020-02-09 15:05:50
【问题描述】：

Curry's paradox （以与当前编程语言相同的人命名）是一种可能在错误逻辑中的构造，它允许人们证明任何事情。

我对逻辑一无所知，但它有多难？

module Main where

import Data.Void
import Data.Function

data X = X (X -> Void)

x :: X
x = fix \(X f) -> X f

u :: Void
u = let (X f) = x in f x

main :: IO ()
main = u `seq` print "Done!"

它确实会循环。 （GHC 是怎么知道的？！）

% ghc -XBlockArguments Z.hs && ./Z
[1 of 1] Compiling Main             ( Z.hs, Z.o )
Linking Z ...
Z: <<loop>>

这是忠实的翻译吗？为什么？
我可以在没有fix 或递归的情况下做同样的事情吗？为什么？

【问题讨论】：

如果不使用修复或某种递归（在术语级别或类型级别），您无法构造Void 类型的术语。如果您删除所有永久递归的方法或导致运行时错误（例如undefined），那么语言就会变得规范化，因此每个t :: T 都会减少到一些t' :: T，这是一种正常形式，“开始”具有构造函数T（如果是函数类型，则为 lambda）。 Void 没有构造函数，所以这是不可能的。
@chi 如果您可以重复此作为对question nearby 的回答。

标签： haskell recursion logic curry-howard

【解决方案1】：

库里悖论的编码看起来更像这样：

x :: X
x = X (\x'@(X f) -> f x')

X 确实可以读作“如果X 为真，则存在矛盾”，或者等效地，“X 为假”。

但是用fix来证明X其实并没有什么意义，因为fix作为推理原则是公然不正确的。库里悖论更微妙。

你如何实际证明X？

x :: X
x = _

X 是一个条件命题，所以你可以先假设它的前提来显示它的结论。这个逻辑步骤对应于插入一个 lambda。（建设性地，蕴涵证明是从前提证明到结论证明的映射。）

x :: X
x = X (\x' -> _)

但是现在我们有一个假设x' :: X，我们可以再次展开X的定义得到f :: X -> Void。在对 Curry 悖论的非正式描述中，没有明确的“展开步骤”，但在 Haskell 中，当X 是假设时，它对应于新类型构造函数上的模式匹配，或者当X 是目标时应用构造函数（在事实上，正如我们上面所做的那样）：

x :: X
x = X (\x'@(X f) -> _)

最后，我们现在有了f :: X -> Void和x' :: X，所以我们可以通过函数应用推导出Void：

x :: X
x = X (\x'@(X f) -> f x')

【讨论】：