1

我对 GHC 用户指南的“隐式参数和多态递归”一章有疑问。

代码是

len1 :: [a] -> Int
len1 xs = let ?acc = 0 in len_acc1 xs

len_acc1 [] = ?acc
len_acc1 (_:xs) = let ?acc = ?acc + (1::Int) in len_acc1 xs

------------

len2 :: [a] -> Int
len2 xs = let ?acc = 0 in len_acc2 xs

len_acc2 :: (?acc :: Int) => [a] -> Int
len_acc2 [] = ?acc
len_acc2 (_:xs) = let ?acc = ?acc + (1::Int) in len_acc2 xs

章节说

在前一种情况下，len_acc1 在它自己的右手边是单态的，所以隐式参数 ?acc 不会传递给递归调用。在后一种情况下，由于 len_acc2 具有类型签名，因此对多态版本进行递归调用，该版本将 ?acc 作为隐式参数。

问题是

  • 在这种情况下，“单态在它自己的右手边”是否意味着类型 len_acc1 :: (?acc :: Int) => [a] -> p？为什么ghci说len_acc1 :: (?acc::Int) => [a] -> Int？

  • 为什么第一个函数是单态的，而第二个不是？如果我的理解是正确的，反之亦然。

  • 或者可能意味着类型是len_acc1 :: [a] -> Int，但每种情况都指的是?acc隐式值，所以我认为类型应该提到(?acc :: Int)约束。

  • 这种单态性如何暗示隐式参数没有传递给函数？

4

2 回答 2

2

在 Haskell 中，我们经常将带有类型变量的类型签名称为多态，比如id这里的类型签名包含类型变量的多态函数a：

id :: a -> a

然而，这个签名是多态的，不是因为它包含类型变量a，而是因为该变量是quantified。在 Haskell 中，类型签名是隐式地普遍量化的，所以上面等价于：

id :: forall a. a -> a

如果您打开ExplicitForAll扩展程序，这实际上是可接受的语法。正是这种量化使类型具有多态性。

当 Haskell 键入没有类型签名的绑定时，它使用 Hindley-Milner 类型算法来分配类型。该算法通过将单态类型签名分配给相互依赖的绑定集，然后通过确定它们之间的关系来细化它们。这些签名允许包含类型变量（！），但它们仍然被认为是单态的，因为变量没有被量化。也就是说，变量被想象为代表特定类型，我们只是还没有弄清楚它们，因为我们正处于类型检查的中间。

一旦类型检查完成，并且分配了“最终”单态类型，就会有一个单独的泛化步骤。保留在单态类型中的所有类型变量，尚未确定为 和 等固定类型Int，Bool都通过全称量化进行泛化。该步骤确定绑定的最终多态类型。约束是量化过程的一部分，因此当我们从单态类型转移到多态类型时，仅在泛化步骤中应用于类型签名。

该文档指的是这样一个事实，即在推断len_acc1的类型时，算法为其分配单态类型，最终是len_acc1 :: [a] -> Int具有自由（即未量化）类型变量的最终单态类型a。虽然类型检查器会注意到需要一个(?acc :: Int)约束，但它不会使这部分成为推断类型的len_acc1. 特别是，分配给递归调用的类型是没有约束len_acc1的单态类型[a] -> Int。只有在len_acc1确定了最终的单态类型 for 之后，才通过量化a和添加约束对其进行概括，以产生最终的顶级签名。

相反，当提供顶级多态签名时：

len_acc2 :: forall a. (?acc :: Int) => [a] -> Int

绑定len_acc2在任何使用它的地方都是多态的（连同其相关的约束），特别是在递归调用中。

结果是len_acc1递归调用单态，没有提供（新）?acc参数值的约束字典，而len_acc2多态调用，具有新?acc值的约束字典。我相信，这种情况是隐式参数所独有的。否则，您不会遇到递归调用可以单态和多态键入的情况，这样代码在两种类型下的行为会有所不同。

您更有可能遇到如下情况，其中需要“明显”的类型签名，因为无法推断出单态类型：

data Binary a = Leaf a | Pair (Binary (a,a)) deriving (Show)

-- following type signature is required... 
-- toList :: Binary a -> [a]
toList (Leaf x) = [x]
toList (Pair b) = concatMap (\(x,y) -> [x,y]) (toList b)

main = print $ toList (Pair (Pair (Leaf ((1,2),(3,4)))))
于 2020-12-27T03:16:05.223 回答
0

我只能部分回答这个问题。

为什么ghci说len_acc1 :: (?acc::Int) => [a] -> Int？

这是Int因为第一个子句返回?acc并且可以推断它Int来自?acc + (1::Int)第二个子句。

“在……右手边”

表示 之后的部分=，其类型Int同上，是单态的。len_acc1 :: (?acc :: Int) => [a] -> p将是多态的。

或者可能意味着类型是 len_acc1 :: [a] -> Int，但每种情况都引用 ?acc 隐式值，所以我认为类型应该提到 (?acc :: Int) 约束。

这似乎是对我说的；至少暂时将其视为具有该类型。但是我不明白为什么它会编译。

我试图阅读定义隐式参数的论文，但没有找到答案。

于 2020-12-26T16:53:21.620 回答