Haskell 类型检查和确定性答案

【问题标题】：Haskell type checking and determinismHaskell 类型检查和确定性
【发布时间】：2018-08-10 11:15:41
【问题描述】：

根据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 中我们可以将多态类型应用于另一个，而不指定我们使用哪些实例，这不是很奇怪吗？

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

【问题讨论】：

这是个好问题。请注意，由于 参数化，您的函数 f 在 [Bool] 上的行为与在其他列表类型 [a] 上的行为不同，因此不能存在（即不能用 Haskell 编写）。在 Haskell 中，无法编写 if a==Bool then ... 并拥有未更改的签名 forall a. [a] -> Int。
在下面查看我的答案。参数化一开始可能有点难以理解，但您可以从 Wadler 的经典“免费定理”论文开始，其中展示了很好的示例。
我没有完美的参考。参数化有时会受到底部的影响（seq，无限递归），但我记得假设函数严格，仍然可以具有较弱的参数化形式。（同样，我无法提供参考）。要完全“打破”参数性，可以使用forall a. Typeable a => [a] -> Int，它允许if a==Bool then ...——但这里类型发生了变化，所以它并没有真正被打破：我们有一种用于参数多态性的类型，另一种用于临时（非参数）多态性。
不，在 Haskell 中根本不需要额外的 a 参数。即使在 Coq 中，您也无法消除 (a : Type)，因此没有“如果”。在 Coq 中，您需要一些参数来消除，例如 forall (a : Type), typeable a -> list a -> int 其中 typeable a 被适当定义，例如带有归纳定义。
@chi 没有额外的a，我发现最好的是f l = if typeOf l == typeOf ([True]) then 18 else length l。但随后f [] 因类型错误而崩溃。你有别的看法吗？

标签： haskell hindley-milner

【解决方案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 应用于这些多态类型的结果。

【讨论】：

【解决方案2】：

为了跟进 Chi 的回答，这里证明了 f [] 不能依赖于 f 和 [] 的类型实例。免费根据Theorems（上一篇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 中打破参数化。

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

【讨论】：

您可以使用类型类在 Haskell 中进行临时多态（并因此编写您的类型相关函数）。如果您这样做，类型检查器将强制您明确指定您使用的 a 的类型。
@DarthFennec 哼...这似乎与上面的参数方程相矛盾。或者函数的类型不是forall a. [a] -> Int。你能举出你想到的确切例子吗？
你说得对，抱歉我没说清楚；如果你使用一个类型类（我们称之为Foo）来创建一个类型相关的函数，那么函数的类型必须是forall a. Foo a => [a] -> Int。如果我们不将类约束添加到a，那么是的，参数化表明函数不能依赖于类型。