标签: curry-howard

我在编程生涯中相对较晚地遇到了Curry-Howard Isomorphism,也许这有助于我对它完全着迷.这意味着对于每个编程概念,在形式逻辑中存在精确的模拟,反之亦然.这是一个关于这种类比的"基本"列表,在我的头脑中:

program/definition        | proof
type/declaration          | proposition
inhabited type            | theorem/lemma
function                  | implication
function argument         | hypothesis/antecedent
function result           | conclusion/consequent
function application      | modus ponens
recursion                 | induction
identity function         | tautology
non-terminating function  | absurdity/contradiction
tuple                     | conjunction (and)
disjoint union            | disjunction (or)          -- corrected by Antal S-Z
parametric polymorphism   | universal quantification

那么,对于我的问题:这种同构的一些更有趣/模糊的含义是什么？我不是逻辑学家,所以我确信我只是在这个清单上划过界限.

例如,这里有一些编程概念,我不知道逻辑中精辟的名字:

currying                  | "((a & b) => c) iff (a => (b => c))"
scope                     | "known …

该absurd函数Data.Void具有以下签名,其中,Void是在逻辑上无人居住类型由包导出的:

-- | Since 'Void' values logically don't exist, this witnesses the logical
-- reasoning tool of \"ex falso quodlibet\".
absurd :: Void -> a

我知道足够的逻辑来获得文档的评论,这与命题与类型的对应关系对应于有效的公式? ? a.

令我困惑和好奇的是:这个函数在什么样的实际编程问题上有用？我想也许在某些情况下它可能是一种类型安全的方式来彻底处理"不可能发生"的情况,但我对Curry-Howard的实际用法不太了解,以确定这个想法是否在正确的轨道.

编辑:最好在Haskell中的例子,但如果有人想使用依赖类型的语言我不会抱怨...

我在互联网上搜索过,我找不到任何关于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"类型的值.函数体将准确描述您将如何执行此操作.

这似乎有道理,但它不是很有趣.显然,它必须比这更多......

我一直在研究依赖类型,我理解以下内容:

1. 为什么通用量化表示为依赖函数类型.?(x:A).B(x)表示"对于所有x类型,A都有类型的值B(x)".因此它表示为其中,当给定一个功能的任何值x类型的A返回类型的值B(x).
2. 为什么存在量化表示为依赖对类型.?(x:A).B(x)表示"存在有x类型A值的类型B(x)".因此,它表示为一对,其第一个元素是类型的特定值x,A其第二个元素是类型的值B(x).

旁白:值得注意的是,通用量化总是与物质含义一起使用,而存在量化始终与逻辑联合使用.

无论如何,关于依赖类型的维基百科文章指出:

与从属类型相反的是从属对类型,从属和类型或西格玛类型.它类似于副产品或不相交的联合.

对类型(通常是产品类型)是如何类似于不相交的联合(这是一种和型)？这一直困扰着我.

此外,依赖函数类型如何与产品类型类似？

Set,类似于[]具有完美定义的monadic操作.问题是它们要求值满足Ord约束,因此不可能定义return并且>>=没有任何约束.同样的问题适用于需要对可能值进行某种约束的许多其他数据结构.

标准技巧(在haskell-cafe帖子中向我建议)是包含Set在延续monad中.ContT并不关心底层类型仿函数是否有任何约束.只有在将Sets 包装/展开到continuation中时才需要约束:

import Control.Monad.Cont
import Data.Foldable (foldrM)
import Data.Set

setReturn :: a -> Set a
setReturn = singleton

setBind :: (Ord b) => Set a -> (a -> Set b) -> Set b
setBind set f = foldl' (\s -> union s . f) empty set

type SetM r a = ContT r Set a

fromSet :: (Ord r) => Set a …

因此,在我不断尝试通过小型Haskell练习半理解Curry-Howard时,我已经陷入了困境:

{-# LANGUAGE GADTs #-}

import Data.Void

type Not a = a -> Void

-- | The type of type equality proofs, which can only be instantiated if a = b.
data Equal a b where
    Refl :: Equal a a

-- | Derive a contradiction from a putative proof of @Equal Int Char@.
intIsNotChar :: Not (Equal Int Char)
intIsNotChar intIsChar = ???

很明显,这种类型Equal Int Char没有(非底层)居民,因此在语义上应该有一个absurdEquality :: Equal Int Char -> a功能......但对于我的生活,我无法想出任何方式来编写除了使用之外的其他方法undefined.

所以要么: …

这是库里 - 霍华德的双重否定的记者a; (a -> r) -> r或者(a -> ?) -> ?,或两者兼而有之？

两种类型都可以在Haskell中编码如下,其中?编码为forall b. b.

p1 :: forall r. ((a -> r) -> r)
p2 :: (a -> (forall b. b)) -> (forall b. b)

Wadler 2003的论文以及 Haskell中的实现似乎采用了前者,而其他一些文献(例如本文)似乎支持后者.

我目前的理解是后者是正确的.我理解前者的风格,因为你可以创建类型的值的困难a,从forall r. ((a -> r) -> r)使用纯计算:

> let p1 = ($42) :: forall r. (Int -> r) -> r
> p1 id
42

这似乎与你不能获得直觉逻辑相矛盾 …

我试图理解"Löb和möb:Haskell中的奇怪循环",但是现在意义正在逐渐消失,我只是不明白它为什么会有用.只是召回功能loeb定义为

loeb :: Functor f => f (f a -> a) -> f a
loeb x = go where go = fmap ($ go) x

或等效地:

loeb x = go 
  where go = fmap (\z -> z go) x

在文章中有一个带有[]仿函数和电子表格实现的例子,但对于我来说,就像电子表格本身一样(从未使用它们).

虽然我理解电子表格的东西,但我认为尽管有列表,但对于我和其他人来说,有更多的例子会有所帮助.是否有任何应用程序loeb的Maybe或其他函子？

在范畴论 8.2的最后，Bartosz Milewski 展示了一些逻辑、范畴论和类型系统之间对应关系的例子。

我在徘徊与逻辑异或运算符对应的内容。我知道

a xor b == (a ? b) ? ¬(a ? b) == (a ? b) ? (¬a ? ¬b)

所以我只解决了部分问题：a xor b对应于(Either a b, Either ? ?). 但是这两种缺失的类型是什么？

看来怎么写xor其实归结为怎么写not。

那么什么是¬a？我的理解是，a如果存在类型为 的元素（至少一个），这是合乎逻辑的a。所以要not a为真，a应该是假的，即它应该是Void。因此，在我看来，有两种可能：

(Either a Void, Either Void b) -- here I renamed "not b" to "b"
(Either Void b, Either a Void) -- …

编辑:Void我的意思是Haskell的Void类型,即不能有值的空类型undefined.

有关Swift Evolution的讨论是否noreturn要用实际Void类型替换函数属性.要做到这一点,我们必须确保这将为平台带来真正的好处.使用Void返回类型是不够的.

所以我请你提供非常实用的例子,其中使用Void增加了代码的清晰度,简洁性和通用性.也许它会使用类(在Haskell意义上),也许是泛型,也许它将包含Void在ADT中.

但是,请不要太过深入HKT,Monads,所有那些高级别的东西.标准库中的实用程序功能也是一个不好的例子.一个完美的例子将是街机游戏的一部分或类似的东西.