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 类型.

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

更具体地说，Haskell 中的内容阻止我使用类型 a在执行 f ?我可以想象 f是一个等于 18 的函数在任何 [Bool] , 并且等于所有其他类型列表的通常长度函数。在这种情况下， 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值(value)。我猜想可以证明，给定

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

然后

g @ V (f @ V) :: U

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