haskell - Hindley-Milner概论变得糟糕了吗？

考虑以下程序(在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以便在这里做得更好吗？

编辑:我怀疑和这是使用部分函数(在这种情况下为!!0)的产物。但请参阅:

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

现在没有正在使用的部分功能。但是，c :: forall t. [t]和d :: Int。

最佳答案

项的Hindley-Milner类型不取决于其子项的值，而仅取决于其类型。 HM类型检查器永远不会对表达式进行求值，仅对它们进行类型检查，因此它会像人工进行非正式类型检查时一样，将x视为“a列表”，而不是人类的“a空列表”程序。

有些类型系统会将您的程序标记为类型不正确，例如dependent types，但是那些没有显式类型声明就没有类型推断，这是HM带来的Haskell / ML程序员喜欢的奢侈品之一。

使用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成为类型错误。

关于haskell - Hindley-Milner概论变得糟糕了吗？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/27587759/