Haskell 类型检查和确定性

Question

根据Haskell 2010 language report, its type checker is based on 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 中，我们可以将多态类型应用于另一个，而不指定我们使用哪些实例，这不是很奇怪吗？

更具体地说，Haskell 中的什么阻止我在 f 的实现中使用类型 a？我可以想象 f 是一个函数，它在任何 [Bool] 上等于 18，并且在所有其他类型的列表上等于通常的长度函数。在这种情况下， f [] 会是 18 还是 0 ？ Haskell 报告说 "the kernel is not formally specified"，所以很难说。

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 出现在最后一行。

现在，这真的不是确定性的吗？嗯，它确实涉及算法的一种非确定性步骤 "in the middle"，但最终结果（最一般的）类型是 Int，而且是确定性的。无论我们为 a 选择什么类型，我们总是在最后得到类型 Int。

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

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

然后

g @ V (f @ V) :: U

与 V 的类型相同。这应该是 parametricity 应用于那些多态类型的结果。

Answer 2

为了跟进 Chi 的回答，这里证明 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 论文中描述的多态 lambda 演算更强大。特别是，这个 wiki page 表示可以使用 seq 函数在 Haskell 中破坏参数性。

维基页面还说我的类型依赖函数存在（在 Haskell 以外的其他语言中），它被称为 ad-hoc polymorphism。

Haskell 类型检查和确定性

Haskell type checking and determinism

haskell

hindley-milner