haskell - Hindley-Milner 概括变坏了吗？

Question

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

x = []
y = x!!0

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

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

我理解这是如何发生的，按照通常的泛化/实例化规则进行游戏，但我不确定是否需要像 forall a.一个。

一个问题是:因为我们在这里有越界访问，所以可以排除该程序作为有效示例。相反，我们可以说我们推断出的通用类型是程序错误的标志吗？如果是，我们是否也可以使用这个“事实”在其他情况下故意不检查无效程序？

下一个程序有更奇怪的类型:

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

推断类型:

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

...尽管 d 是从 c 中提取的!

我们能否在不排除有效程序的情况下增强 HM 以在此处做得更好？

编辑:我怀疑编辑这是使用部分函数的产物(在本例中为!!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”，就像人类在对您的程序进行非正式类型检查时所做的那样。

有些类型系统会将您的程序标记为类型不正确，例如dependent types ，但是如果没有显式类型声明，它们就没有类型推断，这是 Haskell/ML 程序员享受的奢侈品之一，感谢 HM。

使用 HM 的扩展(GADTs)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 成为类型错误。