7

根据Haskell 2010 语言报告，它的类型检查器是基于Hindley-Milner 的。所以考虑f这种类型的函数，

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

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

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

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

4

2 回答 2

3

为了跟进 Chi 的回答，这里是f []不能依赖于fand类型实例的证明[]。根据免费定理（这里的最后一篇文章），对于任何类型a,a'和任何函数g :: a -> a'，然后

f_a = f_a' . map g

on typef_a的实例化在哪里，例如在 Haskell 中fa

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 页面说在 Haskell 中可以通过使用该seq函数来打破参数化。

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

于 2018-08-10T14:58:23.607 回答
3

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

无论如何，GHCAny在这种情况下使用内部类型。例如，编译

{-# 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)

whereGHC.Prim.Any出现在最后一行。

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

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

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

然后

g @ V (f @ V) :: U

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

于 2018-08-10T12:21:07.677 回答