haskell - 库里-霍华德同构

Question

我在互联网上搜索过，但我找不到任何对 CHI 的解释，这些解释不会迅速退化为逻辑理论讲座，这完全超出了我的理解范围。 (这些人说话就好像“直觉命题演算”是一个对普通人来说实际上意味着什么的短语!)

粗略地说，CHI 说类型就是定理，程序就是这些定理的证明。但这到底是什么意思？？

到目前为止，我已经弄清楚了:

• 考虑id::x -> x。它的类型表示“鉴于 X 为真，我们可以得出结论 X 为真”。对我来说这似乎是一个合理的定理。

• 现在考虑foo::x -> y。正如任何 Haskell 程序员都会告诉你的那样，这是不可能的。你不能写这个函数。 (好吧，无论如何，不​​要作弊。)作为一个定理，它说“鉴于任何 X 都是真的，我们可以得出结论，任何 Y 都是真的”。这显然是无稽之谈。而且，果然，你无法编写这个函数。

• 更一般地，函数的参数可以被认为是“假设为真的这个”，而结果类型可以被认为是“假设所有其他事情都是真的的事情”。如果有一个函数参数，例如 x -> y，我们可以将其视为假设 X 为真意味着 Y 必须为真。

• 例如，(.)::(y -> z) -> (x -> y) -> x -> z 可以被视为“假设 Y 暗示Z，X 暗示 Y，并且 X 为真，我们可以得出结论 Z 为真”。这对我来说在逻辑上似乎是合理的。

现在，Int -> Int 到底是什么意思？ o_O

我能想到的唯一明智的答案是:如果你有一个函数 X -> Y -> Z，那么类型签名表示“假设可以构造一个 X 类型的值，以及另一个类型的值” Y，则可以构造 Z 类型的值”。函数体准确地描述了您将如何执行此操作。

这似乎有道理，但并不是很有趣。很明显，肯定还有更多的事情......

Answer 1

Curry-Howard 同构简单地指出类型对应于命题，值对应于证明。

Int -> Int 作为一个逻辑命题，并没有多大意义。当将某事物解释为逻辑命题时，您只关心该类型是否存在(有任何值)。所以，Int -> Int 只是意味着“给定一个 Int，我可以给你一个 Int”，当然，这是真的。它有很多不同的证明(对应于该类型的各种不同函数)，但是当将其作为逻辑命题时，你并不真正关心。

这并不意味着有趣的命题不能涉及这样的功能；只是作为一个命题，那种特定类型非常无聊。

对于不完全多态且具有逻辑含义的函数类型实例，请考虑 p -> Void(对于某些 p)，其中 Void 是无人居住的类型:没有值的类型(Haskell 中的 ⊥ 除外，但我稍后会介绍)。获得 Void 类型值的唯一方法是您可以证明一个矛盾(当然，这是不可能的)，并且由于 Void 意味着您已经证明了一个矛盾矛盾，你可以从中得到任何值(即存在一个函数absurd::Void -> a)。因此，p -> Void 对应于 Øp:它的意思是“p意味着虚假”。

Intuitionistic logic只是常见函数式语言所对应的某种逻辑。重要的是，它是建设性的:基本上，a -> b 的证明为您提供了一个算法来计算b a，这在常规经典逻辑中是不正确的(因为 law of excluded middle ，它会告诉您某件事是对还是错，但不告诉您为什么)。

尽管像 Int -> Int 这样的函数作为命题意义不大，但我们可以用其他命题来对它们进行陈述。例如，我们可以声明两种类型的相等类型(使用 GADT ):

data Equal a b where
    Refl :: Equal a a

如果我们有一个 Equal a b 类型的值，则 a 与 b 类型相同:Equal a b code> 对应命题 a = b。问题是我们只能通过这种方式谈论类型的平等。但如果我们有 dependent types ，我们可以轻松地将这个定义推广到任何值，因此等于 a b 将对应于以下命题:值 a 和 b 相同。因此，例如，我们可以这样写:

type IsBijection (f :: a -> b) (g :: b -> a) =
    forall x. Equal (f (g x)) (g (f x))

这里，f 和 g 是常规函数，因此 f 可以轻松拥有类型 Int -> Int 。同样，Haskell 无法做到这一点；你需要依赖类型来完成这样的事情。

典型的函数式语言并不真正适合编写证明，不仅因为它们缺乏依赖类型，还因为 ⊥，其中所有 a 都有类型 a code>，充当任何命题的证明。但是total像Coq这样的语言和 Agda利用对应关系充当证明系统以及依赖类型的编程语言。