Haskell类型检查和确定性

Question

根据Haskell 2010 language report，它的类型检查器是基于Hindley-Milner的。因此考虑这种类型的函数f，

f :: forall a. [a] -> Int

例如，它可以是长度函数。根据Hindley-Milner的说法，f []会检查Int的类型。我们可以通过将f的类型实例化为[Int] -> Int，将[]的类型实例化为[Int]来证明这一点，然后得出结论，应用程序([Int] -> Int) [Int]的类型为Int。

在这个证明中，我选择通过将Int替换为a来实例化forall a. [a] -> Int和forall a. [a]类型。我可以用Bool代替，证明也是有效的。在Hindley-Milner中，我们可以将一个多态类型应用到另一个类型，而不指定我们使用的实例，这不是很奇怪吗？

更具体地说，是什么阻止了我在f的实现中使用a类型？我可以想象f是一个在任何列表上等于18的函数，并且在所有其他类型的列表上等于通常的长度函数。在本例中，f []是18还是0？Haskell的报告说“内核没有正式指定”，所以很难说。

Answer 1

在类型推断期间，这样的类型变量确实可以实例化为任何类型。这可能被视为一个高度不确定的步骤。

在这种情况下，GHC使用内部Any类型。例如，编译

{-# NOINLINE myLength #-}
myLength :: [a] -> Int
myLength = length

test :: Int
test = myLength []

结果如下：

-- RHS size: {terms: 3, types: 4, coercions: 0}
myLength [InlPrag=NOINLINE] :: forall a_aw2. [a_aw2] -> Int
[GblId, Str=DmdType]
myLength =
  \ (@ a_aP5) -> length @ [] Data.Foldable.$fFoldable[] @ a_aP5

-- RHS size: {terms: 2, types: 6, coercions: 0}
test :: Int
[GblId, Str=DmdType]
test = myLength @ GHC.Prim.Any (GHC.Types.[] @ GHC.Prim.Any)

其中GHC.Prim.Any出现在最后一行。

现在，这真的不是确定性的吗？好吧，它确实涉及到算法“中间”的一种非确定性步骤，但最终得到的(最通用的)类型是Int，而且是确定性的。我们为a选择什么类型并不重要，我们总是在最后得到Int类型。

当然，获得相同的类型是不够的:我们还希望获得相同的Int值。我猜想，可以证明，给定

f :: forall a. T a
g :: forall a. T a -> U

然后

g @ V (f @ V) :: U

无论V是什么类型，都是相同的值。这应该是parametricity应用于这些多态类型的结果。

Answer 2

为了跟进迟浩田的回答，下面是f []不能依赖于f和[]的类型实例的证明。根据免费定理(上一篇文章here)，对于任何类型的a,a'和任何函数g :: a -> a'，那么

f_a = f_a' . map g

其中f_a是f在类型a上的实例化，例如在Haskell中

f_Bool :: [Bool] -> Int
f_Bool = f

然后，如果您在[]_a上计算前面的等式，它将生成f_a []_a = f_a' []_a'。在原始问题的情况下，f_Int []_Int = f_Bool []_Bool。

Haskell中的一些参数化参考也会很有用，因为Haskell看起来比Walder的论文中描述的多态λ演算更强大。特别地，这个wiki page指出可以通过使用seq函数来打破Haskell中的参数化。

维基页面还说我的类型依赖函数存在(除了Haskell之外的其他语言)，它被称为ad-hoc polymorphism。