问Haskell隐式参数与多态递归

EN

在Haskell中，我们经常将类型变量的类型签名称为多态类型，就像多态函数id，其类型签名在这里包括类型变量a。

id :: a -> a

但是，这个签名是多态的，不是因为它包含类型变量a，而是因为该变量是量化的。在Haskell中，类型签名是隐含的、普遍量化的，因此上面的内容相当于：

id :: forall a. a -> a

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

当Haskell在没有类型签名的情况下键入绑定时，它使用辛德雷-米尔纳键入算法来分配类型。该算法通过向相互依赖的绑定集分配单纯类型签名，然后通过确定它们之间的关系来细化它们。允许这些签名包含类型变量(!)，但它们仍然被认为是单形的，因为这些变量没有量化。也就是说，变量被认为是特定类型的代表，我们只是还没有弄清楚它们，因为我们正在进行类型检查。

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

文档所指的事实是，当推断len_acc1's类型时，算法给它指定了一个单纯类型，最终是具有自由(即未量化)类型变量a的最终单纯类型a。虽然类型检查器会注意到需要一个(?acc :: Int)约束，但它并不是推断的len_acc1类型的这一部分。特别是，分配给len_acc1递归调用的类型是没有约束的单纯类型[a] -> Int。只有在确定了len_acc1的这个最终的单纯类型之后，它才是通过对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)))))

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

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

它是Int，因为第一个子句返回?acc，可以在第二个子句中从?acc + (1::Int)推断为Int。

“在.右边”

表示=之后的部分，其类型为Int，如上面所示，它是单形的。len_acc1 :: (?acc :: Int) => [a] -> p是多态的.

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

这就是它似乎在对我说的话，至少暂时它被视为有这种类型。但我不明白它为什么会编译。

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