有Haskell无法验证的类型签名吗? [英] Are there type signatures which Haskell can't verify?

问题描述

本文建立了这种类型推断(称为系统F中的典型性"是不确定的.我在其他地方从未听说过的是本文的第二个结果，即F中的类型检查"也是不确定的.在这里，类型检查"问题的意思是:给定术语t，类型T和类型环境A，判断A ⊢ t : T是否可导出?对于我来说，这个问题无法确定(相当于可打字性问题)令我感到惊讶，因为从直觉上看，这应该是一个更容易回答的问题.

This paper establishes that type inference (called "typability" in the paper) in System F is undecidable. What I've never heard mentioned elsewhere is the second result of the paper, namely that "type checking" in F is also undecidable. Here the "type checking" question means: given a term t, type T and typing environment A, is the judgment A ⊢ t : T derivable? That this question is undecidable (and that it's equivalent to the question of typability) is surprising to me, because it seems intuitively like it should be an easier question to answer.

但是无论如何，鉴于Haskell基于系统F(甚至F-omega)，关于类型检查的结果似乎表明存在Haskell术语t和类型T使得编译器将无法确定t :: T是否有效.如果是这样，我很好奇这样的术语和类型是什么...如果不是，那我会误解什么?

But in any case, given that Haskell is based on System F (or F-omega, even), the result about type checking would seem to suggest that there is a Haskell term t and type T such that the compiler would be unable to decide whether t :: T is valid. If that's the case, I'm curious what such a term and type are... if it's not the case, what am I misunderstanding?

大概理解这篇论文会得出一个建设性的答案，但我的观点还不够深入:)

Presumably comprehending the paper would lead to a constructive answer, but I'm a little out of my depth :)

推荐答案

可以通过适当丰富语法来确定类型检查.例如，在本文中，我们将lambda编写为\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，以及何时消除它们.

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.

所以问题是:我们可以从Haskell转到带有足够注释的System F术语吗?答案是肯定的，这要归功于Haskell类型系统设置的一些关键限制.最关键的是所有类型都排名第一*.无需赘述，等级"与您必须在->构造函数的左侧查找forall的次数有关.

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)

下一个最关键的限制是类型变量只能由单态类型替换. (这包括其他类型变量，例如a，但不包括多态类型，例如forall a. a.)这样可以部分确保类型替换保留等级一.

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.

事实证明，如果您同时设定了这两个限制，则不仅类型推断是可决定的，而且还可以获得 minimum 类型.

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

如果我们从Haskell转向GHC，那么我们不仅可以讨论可打字的内容，还可以讨论推理算法的外观.特别是在GHC中，有一些扩展可以放宽上述两个限制； GHC如何在这种情况下进行推断?好吧，答案是它甚至根本不尝试.如果要使用这些功能来编写术语，则必须在第一段中添加我们曾经讨论过的键入注释:您必须显式注释forall的引入和消除之处.那么，我们可以写一个GHC类型检查器拒绝的术语吗?是的，这很容易:只需使用未注释的二级(或更高级别)类型或隐含性即可.例如，即使下面的代码具有显式的类型注释并且可以使用第二级类型进行键入，也不会对其进行类型检查:

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

*实际上，限制等级2足以使其可判定，但是等级1类型的算法可能更有效.等级三类型已经给程序员足够的动力来使推理问题变得不可预知.我不确定在委员会选择将Haskell限制为排名第一类型时是否知道这些事实.

* 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.

这篇关于有Haskell无法验证的类型签名吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！