欣德利 - 米尔纳的概括变坏了？

Question

考虑以下程序(在Haskell中,但可以是任何HM推断语言):

x = []
y = x!!0

使用HM(或运行编译器),我们推断:

x :: forall t. [t]
y :: forall a. a

我理解这是如何发生的,通过通常的泛化/实例化规则,但我不确定是否有可能有这样的东西forall a. a.

一个问题是:由于我们在这里有一个越界访问,人们可以排除该程序作为一个有效的例子.相反,我们可以说我们推断的通用类型是程序中出错的标志吗？如果是的话,我们是否可以使用这个"事实"故意在其他情况下无效检查无效程序？

下一个程序甚至可以获得更奇怪的类型:

c = []
d = (c!!0) + (1 :: Int)

推断类型:

c :: forall t. [t]
d :: Int

......虽然d是从中抽出来的c!

我们可以在没有排除有效程序的情况下增强HM在这里做得更好吗？

编辑:我怀疑ed这是使用部分函数的工件(!!0在这种情况下).但请看:

c = []
d = case c of [] -> 0; (x:_) -> x + (1 :: Int)

现在没有使用部分功能.然而,c :: forall t. [t]和d :: Int.

Answer 1

Hindley-Milner类型的术语不依赖于其子项的值,仅取决于它们的类型.HM类型检查器永远不会评估表达式,只会对它们进行类型检查,因此它将您x视为"列表a",而不是"空列表a",就像人们非正式地对您的程序进行类型检查一样.

有一些类型系统可以将你的程序标记为类型不正确,例如依赖类型,但那些没有显式类型声明的类型推断,这是Haskell/ML程序员喜欢的奢侈品之一,这要归功于HM.

使用HM(GADT)的扩展Haskell可以为"安全列表"定义类型

data Empty
data NonEmpty

data SafeList a b where
  Nil :: SafeList a Empty
  Cons:: a -> SafeList a b -> SafeList a NonEmpty

(!!) :: SafeList a NonEmpty -> Int -> a
-- etc

这会产生Nil!!0类型错误.