2

考虑以下程序（在 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。

4

2 回答 2

5

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

有一些类型系统会将你的程序标记为类型不正确，例如依赖类型，但那些没有明确类型声明的类型推断，这是 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类型错误。

于 2014-12-21T09:17:19.110 回答
3

我不确定是否需要类似forall a. a.

这是不可取的。通过参数化，当您评估这种类型的表达式时，它唯一能做的就是无法停止，无论是通过抛出异常还是通过无限循环。当我们谈论产生“底部”（⊥）的计算时，这就是 Haskellers 的意思。

如果您正在考虑 HM 的什么扩展会排除此类类型，您可以禁止任何类型，当解释为逻辑公式时，它不是重言式。这样的函数将保证对某些输入产生错误。

所以x :: forall a. [a]没关系，因为对于任何类型a，我们确实可以构造一个类型的值——一个[a]空列表！但是，例如，head :: forall a. [a] -> a这是不行的，因为我们总是不能a从一个类型的值中得到一个类型的值——[a]因为列表可能是空的。

但是，您的类型越具体，这就越没用。例如，您基本上无法保证 type 的功能Int -> Int。

于 2014-12-21T09:31:49.003 回答