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

Question

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

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

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

Answer 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]是替代括号中).然后语法告诉我们何时以及添加多少个foralls,以及何时消除它们.

所以问题是:我们可以从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的类型检查器拒绝的术语吗？是的,这很简单:只需使用未注释的二级(或更高级)类型或不可预测性.例如,以下内容不进行类型检查,即使它具有显式类型注释并且可以使用rank-two类型:

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

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

Answer 2

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

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