是否存在 Haskell 无法验证的类型签名？答案

【问题标题】：Are there type signatures which Haskell can't verify?是否存在 Haskell 无法验证的类型签名？
【发布时间】：2011-10-05 22:51:41
【问题描述】：

This paper 确定 System F 中的类型推断（在论文中称为“可类型性”）是不可判定的。我从未听说过在其他地方提到的是该论文的第二个结果，即 F 中的“类型检查”也是不可判定的。这里“类型检查”问题的意思是：给定一个术语t，类型T 和类型环境A，判断A ⊢ t : T 是否可导出？这个问题是不可判定的（并且它等同于可打字性的问题）令我惊讶，因为直觉上它似乎应该是一个更容易回答的问题。

但无论如何，鉴于 Haskell 基于 System F（或 F-omega，甚至），关于类型检查的结果似乎表明有一个 Haskell 术语 t 和类型 T 这样编译器将无法确定t :: T 是否有效。如果是这样的话，我很好奇这样的术语和类型是什么......如果不是这样，我误解了什么？

大概理解这篇论文会导致一个建设性的答案，但我有点超出我的深度:)

【问题讨论】：

Haskell 使用名为 [Hindley Milner][en.wikipedia.org/wiki/Hindley–Milner] 的 System F resitricted 版本。 AFAIK 可以推断出任何具有类型的表达式的类型。让类型检查变得不可能是打开足够多奇怪的扩展的问题。
@FUZxxl：我相信通过仅启用RankNTypes 和ImpredicativeTypes 将拥有System F 的全部功能（还有一些，因为Haskell 还支持对类型运算符的抽象）。跨度>
这就是我试图说的“使类型检查成为不可能是打开足够多奇怪的扩展的问题。”

标签： haskell typechecking type-theory

【解决方案1】：

类型检查可以通过适当地丰富语法来确定。例如，在论文中，我们将 lambdas 写为\x -> e；要对此进行类型检查，您必须猜测x 的类型。但是，通过适当丰富的语法，可以将其写为\x :: t -> e，从而消除了猜测工作。同样，在论文中，它们允许隐式类型级别的 lambda。也就是说，如果是e :: t，那么也是e :: forall a. t。要进行类型检查，您必须猜测何时添加以及添加多少 forall，以及何时删除它们。和以前一样，您可以通过添加语法来使其更具确定性：我们添加两个新的表达式形式 /\a. e 和 e [t] 以及两个新的输入规则，即如果 e :: t，然后是 /\a. e :: forall a. t，如果是 e :: forall a. t，那么e [t'] :: t [t' / a]（t [t' / a] 中的括号是替换括号）。然后语法告诉我们何时添加多少个 forall，以及何时删除它们。

所以问题是：我们可以从 Haskell 转到充分注释的 System F 术语吗？答案是肯定的，这要归功于 Haskell 类型系统设置的一些关键限制。最关键的是所有类型都是rank one*。无需过多详细说明，“排名”与您必须到 -> 构造函数的左侧找到 forall 的次数有关。

Int -> Bool -- rank 0?
forall a. (a -> a) -- rank 1
(forall a. a -> a) -> (forall a. a -> a) -- rank 2

特别是，这会稍微限制多态性。我们不能用等级一的类型输入这样的东西：

foo :: (forall a. a -> a) -> (String, Bool) -- a rank-2 type
foo polymorphicId = (polymorphicId "hey", polymorphicId True)

下一个最关键的限制是类型变量只能被单态类型替换。（这包括其他类型变量，如 a，但不包括多态类型，如 forall a. a。）这在一定程度上确保了类型替换保留秩一。

事实证明，如果你做了这两个限制，那么不仅类型推断是可判定的，而且你还可以得到 minimal 类型。

如果我们从 Haskell 转向 GHC，那么我们不仅可以讨论什么是可类型化的，还可以讨论推理算法的外观。特别是在 GHC 中，有一些扩展放宽了上述两个限制； GHC 如何在这种情况下进行推理？好吧，答案是它根本不尝试。如果您想使用这些功能编写术语，那么您必须添加我们在第一段中一直讨论的打字注释：您必须明确注释foralls 的引入和消除位置。那么，我们可以写一个 GHC 的类型检查器拒绝的术语吗？是的，这很容易：只需使用未注释的二级（或更高）类型或不可预测性。例如，以下内容不进行类型检查，即使它具有显式类型注释并且可以使用 rank-two 类型进行类型化：

{-# LANGUAGE Rank2Types #-}
foo :: (String, Bool)
foo = (\f -> (f "hey", f True)) id

* 实际上，限制为 rank 2 就足以使其可判定，但 rank 1 类型的算法可能更有效。 Rank 3 类型已经为程序员提供了足够的绳索，使推理问题无法确定。我不确定在委员会选择将 Haskell 限制为一级类型时是否知道这些事实。

【讨论】：

回复。 “所以问题是：” ...不，这实际上是不是的问题。我没有问是否通过注释函数参数或限制为 rank-2 多态性，我们是否可以使类型检查成为可判定的；我知道答案是肯定的。我的问题是，您能否展示一个术语 t 并输入 T 以使 t :: T 混淆类型检查器。我应该明确指出，t 应该是无类型 lambda 演算中的一个术语（它不应该包含类型归属），而 T 可以包含任意数量的嵌入 foralls。
@pelotom 好的，很抱歉造成误解。您提出的问题是一个非常困难的问题：它涉及您感兴趣的特定编译器使用的确切类型检查算法的非常复杂的知识。不可能从证明在不检查用于逼近该问题解决方案的算法的情况下，该问题对于该问题的不可解决实例的不可判定性。
@pelotom 我添加了两个部分，一个关于另一个重要限制（预测性），另一个是试图回答您针对 GHC 类型检查器的具体情况的实际问题：给出一个GHC 目前无法验证的术语和类型。这样更好吗？
Rank 2 类型没有最小类型
@JTanner 正确。具有 rank-2 类型的类型推断必然是整个程序的操作。您是否认为这与书面答案中的任何内容相矛盾？如果有，具体是什么？

【解决方案2】：

以下是 Scala 中 SKI 演算的类型级实现示例：http://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/

最后一个例子展示了一个无限迭代。如果你在 Haskell 中做同样的事情（我很确定你可以），你就有了一个“不可输入的表达式”的例子。

【讨论】：

我希望看到 Haskell 中的等价物。