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

发布于 2024-12-07 19:18:00 字数 567 浏览 1 评论 0原文

本文建立了类型推断（称为“可打字性”）论文中）在系统 F 中是不可判定的。我在其他地方从未听过提到的是论文的第二个结果，即 F 中的“类型检查”也是不可判定的。这里的“类型检查”问题的意思是：给定一个术语t，类型T和类型环境A，则判断A ⊢ t : T 可导出吗？这个问题是不可判定的（并且它相当于可打字性问题），这令我感到惊讶，因为从直觉上看，它应该是一个更容易回答的问题。

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

想必理解这篇论文会带来建设性的答案，但我有点超出了我的深度:)

原文

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

腹黑女流氓 2024-12-14 19:18:00

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

所以问题是：我们可以从 Haskell 转向充分注释的 System F 术语吗？答案是肯定的，这要归功于 Haskell 类型系统设置的一些关键限制。最关键的是所有类型都是第一级*。无需过多讨论，“排名”与您必须转到 -> 构造函数左侧才能找到 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 等多态类型。）这在一定程度上确保了类型替换保留了排名一性。

事实证明，如果您做出这两个限制，那么类型推断不仅是可判定的，而且您还可以获得最小类型。

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

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

* 实际上，限制为二级就足以使其可判定，但是一级类型的算法可以更有效率。排名三的类型已经为程序员提供了足够的绳索来使推理问题变得不可判定。我不确定委员会选择将 Haskell 限制为一级类型时是否知道这些事实。

Type checking can be made decidable by enriching the syntax appropriately. For example, in the paper, we have lambdas written as \x -> e; to type-check this, you must guess the type of x. However, with a suitably enriched syntax, this can be written as \x :: t -> e instead, which takes the guess-work out of the process. Similarly, in the paper, they allow type-level lambdas to be implicit; that is, if e :: t, then also e :: forall a. t. To do typechecking, you have to guess when and how many forall's to add, and when to eliminate them. As before, you can make this more deterministic by adding syntax: we add two new expression forms /\a. e and e [t] and two new typing rule that says if e :: t, then /\a. e :: forall a. t, and if e :: forall a. t, then e [t'] :: t [t' / a] (where the brackets in t [t' / a] are substitution brackets). Then the syntax tells us when and how many foralls to add, and when to eliminate them as well.

So the question is: can we go from Haskell to sufficiently-annotated System F terms? And the answer is yes, thanks to a few critical restrictions placed by the Haskell type system. The most critical is that all types are rank one*. Without going into too much detail, "rank" is related to how many times you have to go to the left of an -> constructor to find a forall.

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

In particular, this restricts polymorphism a bit. We can't type something like this with rank one types:

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

The next most critical restriction is that type variables can only be replaced by monomorphic types. (This includes other type variables, like a, but not polymorphic types like forall a. a.) This ensures in part that type substitution preserves rank-one-ness.

It turns out that if you make these two restrictions, then not only is type-inference decidable, but you also get minimal types.

If we turn from Haskell to GHC, then we can talk not only about what is typable, but how the inference algorithm looks. In particular, in GHC, there are extensions that relax the above two restrictions; how does GHC do inference in that setting? Well, the answer is that it simply doesn't even try. If you want to write terms using those features, then you must add the typing annotations we talked about all the way back in paragraph one: you must explicitly annotate where foralls get introduced and eliminated. So, can we write a term that GHC's type-checker rejects? Yes, it's easy: simply use un-annotated rank-two (or higher) types or impredicativity. For example, the following doesn't type-check, even though it has an explicit type annotation and is typable with rank-two types:

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

* Actually, restricting to rank two is enough to make it decidable, but the algorithm for rank one types can be more efficient. Rank three types already give the programmer enough rope to make the inference problem undecidable. I'm not sure whether these facts were known at the time that the committee chose to restrict Haskell to rank-one types.

回复收藏 0 原文