咖喱霍华德同构

我已经在互联网上search了一遍，我也找不到任何关于“气”的解释，这些解释并没有迅速退化成一个逻辑理论的演讲，而这个逻辑理论在我的脑海中已经大打折扣了。 （这些人认为“直觉主义演算”是一个实际上对于正常人来说意味着什么的短语！）

粗略地说，CHI说types是定理，程序是这些定理的certificate。 但是这到底意味着什么呢？

到目前为止，我已经明白了这一点：

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

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

• 更一般地说，函数的论点可以被认为是“被假定为真的”，结果types可以被认为是“假设所有其他事物都是真的”。 如果有一个函数论证，比如说x -> y ，那么我们可以把这个假设看作X是真的，这意味着Y必须是真的。

• 例如， (.) :: (y -> z) -> (x -> y) -> x -> z可以被认为是“假设Y意味着Z，X意味着Y，并且X是真实的，我们可以得出结论Z是真的“。 这对我来说似乎是合情合理的。

现在，究竟是什么Int -> Int意思是？ O_O

我可以想到的唯一明智的答案是：如果你有一个函数X – > Y – > Z，那么types签名表示“假设可以构造一个Xtypes的值，另一个types为Y，那么有可能构造一个Z型的值“。 而function正文描述了你将如何做到这一点。

这似乎是有道理的，但它不是很有趣 。 所以显然必须有比这更多的…

Answer 1

咖喱霍华德同构只是说types对应于命题，而数值对应于certificate。

Int -> Int作为一个逻辑命题并不意味着太有趣。 当把某些东西解释为一个逻辑命题时，你只关心types是否有人居住 （有任何价值）。 所以， Int -> Int只是意味着“给一个Int ，我可以给你一个Int ”，这当然是真的。 它有很多不同的certificate（对应于这种types的各种不同的function），但是当它作为一个逻辑命题时，你并不在乎。

这并不意味着有趣的命题不能涉及这样的function; 只是那个特别的types是相当无聊的，作为一个命题。

对于不是完全多态的函数types的实例，它具有逻辑意义，请考虑p -> Void （对于某些p ），其中Void是无人居住的types：没有值的types（除了Haskell中的⊥外我会在以后）。 获得Voidtypes值的唯一方法就是如果你能certificate一个矛盾（这当然是不可能的），并且由于Void意味着你已经certificate了一个矛盾，你可以从中获得任何价值（即存在一个函数absurd :: Void -> a ）。 因此， p -> Void对应于¬p：这意味着“ p暗示虚假”。

直觉逻辑就是普通的function语言所对应的某种逻辑。 重要的是，它是build设性的 ：基本上，一个certificatea -> b给你一个algorithm来计算b ，这在正则经典逻辑中是不正确的（因为排除中间的规律 ，它会告诉你某事是是真是假，但不是为什么 ）。

尽pipe像Int -> Int这样的函数并不像命题那么重要，但我们可以用其他命题来陈述它们。 例如，我们可以声明两种types的平等（使用GADT ）：

 data Equal ab where Refl :: Equal aa 

如果我们有一个types为Equal ab的值，那么a是相同types的b ： Equal ab对应于命题a = b 。 问题是我们只能用这种方式来谈论types的平等。 但是，如果我们有依赖types ，我们可以很容易地推广这个定义来处理任何值，所以Equal ab将对应于a和b 值相同的命题。 所以，举个例子，我们可以这样写：

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

在这里， f和g是正则函数，所以f可以很容易地具有typesInt -> Int 。 Haskell再一次不能这样做; 你需要依赖types来做这样的事情。

典型的函数式语言并不适合于写作certificate，不仅仅是因为它们缺less依赖types，而且还因为⊥，其中所有的a都是atypes，这就是任何命题的certificate。 但是像Coq和Agda这样的总体语言利用通信来充当certificate系统和依赖型编程语言。

Answer 2

也许理解它的意思的最好方法是开始（或尝试） 使用types作为命题和程序作为certificate。 学习一种依赖types的语言比较好，比如Agda （它是用Haskell编写的，与Haskell类似）。 该语言有各种文章和课程 。 了解你Agda是不完整的，但它是试图简化的东西，就像LYAHFGG书。

这是一个简单的certificate的例子：

 {-# OPTIONS --without-K #-} -- we are consistent module Equality where -- Peano arithmetic. -- -- ℕ-formation: ℕ is set. -- -- ℕ-introduction: o ∈ ℕ, -- a ∈ ℕ | (1 + a) ∈ ℕ. -- data ℕ : Set where o : ℕ 1+ : ℕ → ℕ -- Axiom for _+_. -- -- Form of ℕ-elimination. -- infixl 6 _+_ _+_ : ℕ → ℕ → ℕ o + m = m 1+ n + m = 1+ (n + m) -- The identity type for ℕ. -- infix 4 _≡_ data _≡_ (m : ℕ) : ℕ → Set where refl : m ≡ m -- Usefull property. -- cong : {mn : ℕ} → m ≡ n → 1+ m ≡ 1+ n cong refl = refl -- Proof _of_ mathematical induction: -- -- P 0, ∀ x. P x → P (1 + x) | ∀ x. P x. -- ind : (P : ℕ → Set) → P o → (∀ n → P n → P (1+ n)) → ∀ n → P n ind P P₀ _ o = P₀ ind P P₀ next (1+ n) = next n (ind P P₀ next n) -- Associativity of addition using mathematical induction. -- +-associative : (mnp : ℕ) → (m + n) + p ≡ m + (n + p) +-associative mnp = ind P P₀ is m where P : ℕ → Set P i = (i + n) + p ≡ i + (n + p) P₀ : P o P₀ = refl is : ∀ i → P i → P (1+ i) is i Pi = cong Pi -- Associativity of addition using (dependent) pattern matching. -- +-associative′ : (mnp : ℕ) → (m + n) + p ≡ m + (n + p) +-associative′ o _ _ = refl +-associative′ (1+ m) np = cong (+-associative′ mnp) 

在那里你可以看到(m + n) + p ≡ m + (n + p)命题为types及其作为函数的certificate。 这种certificate有更先进的技巧（例如，先序推理 ，Agda中的组合器就像Coq中的策略）。

还有什么可以certificate的：

• head ∘ init ≡ head向量， 在这里 。

• 你的编译器生成一个程序，执行的结果与解释同一个（主机）程序时得到的值相同， 这里是Coq。 这本书也是关于语言build模和程序validation的一个很好的阅读。

• 除此之外，在build构性math中还可以certificate什么，因为Martin-Löf的performance力types理论相当于ZFC。 实际上，Curry-Howard同构可以扩展到物理和拓扑以及代数拓扑 。

Answer 3

我可以想到的唯一明智的答案是：如果你有一个函数X – > Y – > Z，那么types签名表示“假设可以构造一个Xtypes的值，另一个types为Y，那么有可能构build一个typesZ的值“。 而function正文描述了你将如何做到这一点。 这似乎是有道理的，但它不是很有趣。 所以显然必须有比这更多的…

那么，是的，还有很多，因为它有很多的含义，并带来了很多问题。

首先，你们对CHI的讨论仅限于暗示/functiontypes（ -> ）。 你不谈这个，但是你可能也已经看到了连接和分离如何分别对应产品和总和types。 但是其他逻辑运算符如否定，普遍量化和存在量化呢？ 我们如何将涉及这些的逻辑certificate翻译成程序？ 事实certificate，这大致是这样的：

• 否定相当于一stream的延续 。 不要问我解释这一个。
• 对命题（而不是个体）variables的通用量化对应于参数多态性 。 所以例如，多态函数id确实具有typesforall a. a -> a forall a. a -> a
• 命题variables的存在量化对应于与数据或实现隐藏有关的一些事情： 抽象数据types ， 模块系统和dynamic调度 。 GHC的存在types与此有关。
• 对个体variables的普遍和存在性量化导致依赖型系统 。

除此之外，这也意味着有关逻辑的各种certificate立即转化为编程语言的certificate。 例如，直觉主义命题逻辑的可判定性意味着在简单types的lambda演算中终止所有的程序。

现在，究竟是什么Int – > Int的意思是？ O_O

这是一种types，或者一个命题。 在f :: Int -> Int ， (+1)命名一个“程序”（具体来说，函数和常量都可以作为“程序”，或者也可以是certificate）。语言的语义必须提供f一个推论的原始规则，或者certificatef是如何从这样的规则和前提构build的certificate。

这些规则通常是用等式公理来定义的，这些公理定义了一个types的基本成员和规则，这些规则允许你certificate哪些types的其他程序。 例如，从Int转换到Nat （自然数从0开始），我们可以有这些规则：

• 公理： 0 :: Nat （ 0是0 :: Nat的原始certificate）
• 规则： x :: Nat ==> Succ x :: Nat
• 规则： x :: Nat, y :: Nat ==> x + y :: Nat
• 规则： x + Zero :: Nat ==> x :: Nat
• 规则： Succ x + y ==> Succ (x + y)

这些规则足以certificate关于自然数的加法的许多定理。 这些certificate也将是程序。