小编Tom*_*ett的帖子

我在编程生涯中相对较晚地遇到了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 …

两者都是类型是所有类型(无人居住)的交集的术语.两者都可以在代码中传递而不会失败,直到有人试图评估它们.我能看到的唯一区别是,在Java中,存在一个漏洞,它允许仅对null一个操作进行评估,这是一个引用相等比较(==) - 而在Haskell undefined中根本不能在不抛出异常的情况下进行评估.这是唯一的区别吗？

编辑

我真正想要解决的问题是,为什么null在Java 中包含这样一个显然很糟糕的决定,以及Haskell如何逃脱它？在我看来,真正的问题是,你可以做一些有用的带null,即你可以检查它的NULL的含量.因为您可以这样做,所以在代码中传递空值并使它们表示"无结果"而不是"此程序中存在逻辑错误"已成为标准惯例.而在Haskell中,没有办法检查一个术语是否在没有评估它且程序爆炸的情况下评估到底部,因此它永远不会用这种方式来表示"没有结果".相反,一个人被迫使用类似的东西Maybe.

对不起,如果看起来我用"评价"这个词快速而宽松地玩......我试图在这里进行类比,并且难以准确地说出它.我想这表明这个比喻是不精确的.

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

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

在Haskell中采用简单的身份功能,

id :: forall a. a -> a

鉴于Haskell据称支持impregicative多态性,我应该能够通过类型归属"限制" id到类型似乎是合理的(forall a. a -> a) -> (forall b. b -> b).但这不起作用:

Prelude> id :: (forall a. a -> a) -> (forall b. b -> b)

<interactive>:1:1:
    Couldn't match expected type `b -> b'
                with actual type `forall a. a -> a'
    Expected type: (forall a. a -> a) -> b -> b
      Actual type: (forall a. a -> a) -> forall a. a -> a
    In the expression: …

我已经看到了一些用于rank-2多态性的用例(最突出的例子是ST monad),但是没有比这更高级别的用例.有谁知道这样的用例？

数字文字具有多态类型:

*Main> :t 3
3 :: (Num t) => t

但是,如果我将变量绑定到这样的文字,则多态性将丢失:

x = 3
...
*Main> :t x
x :: Integer

另一方面,如果我定义一个函数,它当然是多态的:

f x = 3
...
*Main> :t f
f :: (Num t1) => t -> t1

我可以提供一个类型签名,以确保x遗骸多态:

x :: Num a => a
x = 3
...
*Main> :t x
x :: (Num a) => a

但为什么这有必要呢？为什么不推断出多态类型？

Typeclassopedia说:

"类似的论点也表明,满足第一定律的任何Functor实例(fmap id = id)也会自动满足第二定律.实际上,这意味着只需要检查第一定律(通常通过非常简单的归纳法)确保Functor实例有效."

如果是这种情况,为什么我们甚至提到第二个仿函法？

Law 1: fmap id = id
Law 2: fmap (g . h) = (fmap g) . (fmap h)

我怎样才能让(a, a)一个Functor不诉诸newtype？

基本上我希望它像这样工作:

instance Functor (a, a) where
  fmap f (x, y) = (f x, f y)

但当然,这不是表达它的合法方式:

Kind mis-match
The first argument of `Functor' should have kind `* -> *',
but `(a, a)' has kind `*'
In the instance declaration for `Functor (a, a)'

我真正想要的是这样的类型级函数:( \a -> (a, a)语法无效).也许这是一个类型别名？

type V2 a = (a, a)
instance Functor V2 where
    fmap f (x, y) = (f x, f y)

我认为这会奏效,但事实并非如此.首先我得到这个投诉:

Illegal instance declaration …

本文确定系统F中的类型推断(在本文中称为"可打字性")是不可判定的.我在其他地方从未听过的是该论文的第二个结果,即F中的"类型检查"也是不可判定的.这里的"类型检查"问题意味着:给定一个术语t,类型T和打字环境A,判断是否A ? t : T可推导？这个问题是不可判定的(并且它相当于可打字性的问题)对我来说是令人惊讶的,因为它似乎直觉上应该是一个更容易回答的问题.

但无论如何,鉴于Haskell基于System F(或F-omega,偶数),关于类型检查的结果似乎表明存在Haskell术语t和类型T,使得编译器无法确定是否t :: T是有效.如果是这样的话,我很好奇这样的术语和类型是什么......如果不是这样的话,我有什么误解？

据推测,理解这篇论文会得到一个建设性的答案,但我有点超出我的深度:)

这是类型检查器中的错误吗？

Prelude> let (x :: forall a. a -> a) = id in x 3

<interactive>:0:31:
    Couldn't match expected type `forall a. a -> a'
                with actual type `a0 -> a0'
    In the expression: id
    In a pattern binding: (x :: forall a. a -> a) = id

以上事实无法进行类型检查,但这种扭曲成功:

Prelude> let (x :: (forall a. a -> a) -> Int) = (\f -> f 3) in x id
3

使我认为"弱prenex转换"(见23页文章)可能以某种方式有关.嵌入一​​个forall不能"浮出"的逆变位置似乎可以避免这种奇怪的错误.