库里 - 霍华德同构

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

库里 - 霍华德同构简单地指出类型对应于命题,而值对应于证明.

Int -> Int作为一个逻辑命题并不是真的有意义.在将某些东西解释为逻辑命题时,您只关心该类型是否有人居住(有任何值).所以,Int -> Int只是意味着"给予一个Int,我可以给你一个Int",这当然是真的.它有许多不同的证明(对应于该类型的各种不同功能),但当把它作为一个逻辑命题时,你并不在乎.

这并不意味着有趣的命题不能涉及这些功能; 只是那种特殊的类型很无聊,作为一个命题.

对于一个不完全多态并且具有逻辑意义的函数类型的实例,考虑p -> Void(对于某些p),Void无人居住的类型:没有值的类型(除了⊥,在Haskell中,但我会到达以后).获得类型值的唯一方法Void是,如果你可以证明一个矛盾(当然,这是不可能的),并且因为Void你已经证明了一个矛盾,你可以从中获得任何价值(即存在一个函数absurd :: Void -> a) .因此,p -> Void对应于¬ p:它的意思是" p意味着谬误".

直觉逻辑只是普通函数语言所对应的某种逻辑.重要的是,它是建设性的:基本上,证明a -> b给你一个算法来计算b从a,这是不正确常规经典逻辑(因为的排中律,它会告诉你,什么是真或假,但不为什么).

即使函数不像Int -> Int命题那么重要,我们也可以用其他命题对它们进行陈述.例如,我们可以声明两种类型的相等类型(使用GADT):

data Equal a b where
    Refl :: Equal a a

如果我们有一个类型的值Equal a b,那么a它是相同的类型b:Equal a b对应于命题a = b.问题是我们只能用这种方式谈论类型的相等性.但是如果我们有依赖类型,我们可以很容易地将这个定义推广到任何值,因此Equal 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,可以作为任何命题的证明.但像Coq和Agda这样的总语言利用这些对应关系来充当证明系统以及依赖类型的编程语言.