咖喱霍华德同构

我已经在互联网上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正文描述了你将如何做到这一点。

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

咖喱霍华德同构只是说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的bEqual ab对应于命题a = b 。 问题是我们只能用这种方式来谈论types的平等。 但是,如果我们有依赖types ,我们可以很容易地推广这个定义来处理任何值,所以Equal ab将对应于ab 相同的命题。 所以,举个例子,我们可以这样写:

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

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

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

也许理解它的意思的最好方法是开始(或尝试) 使用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同构可以扩展到物理和拓扑以及代数拓扑 。

我可以想到的唯一明智的答案是:如果你有一个函数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 :: Nat00 :: 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也将是程序。