为什么需要“包装”函数类型才能满足类型检查器的要求？答案

【问题标题】：Why is a function type required to be "wrapped" for the type checker to be satisfied?为什么需要“包装”函数类型才能满足类型检查器的要求？
【发布时间】：2017-08-08 08:29:21
【问题描述】：

以下程序类型检查：

{-# LANGUAGE RankNTypes #-}

import Numeric.AD (grad)

newtype Fun = Fun (forall a. Num a => [a] -> a)

test1 [u, v] = (v - (u * u * u))
test2 [u, v] = ((u * u) + (v * v) - 1)

main = print $ fmap (\(Fun f) -> grad f [1,1]) [Fun test1, Fun test2]

但是这个程序失败了：

main = print $ fmap (\f -> grad f [1,1]) [test1, test2]

类型错误：

Grad.hs:13:33: error:
    • Couldn't match type ‘Integer’
                     with ‘Numeric.AD.Internal.Reverse.Reverse s Integer’
      Expected type: [Numeric.AD.Internal.Reverse.Reverse s Integer]
                     -> Numeric.AD.Internal.Reverse.Reverse s Integer
        Actual type: [Integer] -> Integer
    • In the first argument of ‘grad’, namely ‘f’
      In the expression: grad f [1, 1]
      In the first argument of ‘fmap’, namely ‘(\ f -> grad f [1, 1])’

直观地说，后一个程序看起来是正确的。毕竟，以下看似等效的程序确实有效：

main = print $ [grad test1 [1,1], grad test2 [1,1]]

这看起来像是 GHC 类型系统的限制。我想知道是什么导致了失败，为什么存在这种限制，以及任何可能的除了包装函数之外的解决方法（根据上面的Fun）。

(注意：这不是由单态限制引起的；编译 NoMonomorphismRestriction 没有帮助。）

【问题讨论】：

这可能是可怕的单态限制吗？
不是单态限制。
这确实是类型系统的限制。失败的程序将需要正确地检查不可预测的类型（[test1,test2]::[forall a . ...] 是不可预测的），正如 docs 声称的那样，GHC 只有“非常不稳定的支持”。最好的解决方法是 newtype 包装器。或者，打开ImpredicativeTypes 并为程序的每个子项添加类型注释，直到它进行类型检查。
我还记得ad 有几个模块可以精确解决 GHC 中的这个限制，例如对于diff。

标签： haskell type-mismatch type-systems automatic-differentiation

【解决方案1】：

这是 GHC 类型系统的问题。顺便说一句，它确实是 GHC 的类型系统；类似 Haskell/ML 的语言的原始类型系统不支持更高等级的多态性，更不用说我们在这里使用的暗示性多态性了。

问题在于，为了进行类型检查，我们需要在类型中的任何位置支持foralls。不仅在类型的前面一直聚在一起（允许类型推断的正常限制）。一旦你离开这个区域，类型推断通常会变得无法确定（对于 rank n 多态性及以上）。在我们的例子中，[test1, test2] 的类型需要是[forall a. Num a => a -> a]，考虑到它不适合上面讨论的方案，这是一个问题。这将要求我们使用暗示性多态性，之所以这么称呼是因为a 涵盖了其中包含foralls 的类型，因此a 可以替换为正在使用的类型。

因此，会出现一些行为不端的情况，只是因为问题无法完全解决。 GHC 确实对 rank n 多态性提供了一些支持，并且对隐含多态性提供了一些支持，但通常最好只使用 newtype 包装器来获得可靠的行为。据我所知，GHC 也不鼓励使用此功能，因为很难弄清楚类型推断算法将处理什么。

总而言之，math 表示会出现片状情况，而newtype 包装器是最好的处理方式，如果有点不满意的话。

【讨论】：

ImpredicativeTypes 实际上并没有以任何有意义的方式得到支持。

【解决方案2】：

类型推断算法不会推断出更高等级的类型（-> 左侧带有forall 的类型）。如果我没记错的话，它变得无法确定。无论如何，考虑这段代码

foo f = (f True, f 'a')

它的类型应该是什么？我们本来可以

foo :: (forall a. a -> a) -> (Bool, Char)

但我们也可以有

foo :: (forall a. a -> Int) -> (Int, Int)

或者，对于任何类型的构造函数F :: * -> *

foo :: (forall a. a -> F a) -> (F Bool, F Char)

在这里，据我所知，我们找不到主体类型——这是我们可以分配给foo 的最通用类型。

如果主体类型不存在，则类型推断机制只能为 foo 选择次优类型，这可能会导致稍后出现类型错误。这是不好的。相反，GHC 依赖于 Hindley-Milner 风格的类型推理引擎，该引擎得到了极大的扩展，以涵盖更高级的 Haskell 类型。这种机制与普通的 Hindley-Milner 不同，它将为 f 分配一个多态类型提供用户明确要求，例如给foo签名。

使用像Fun 这样的包装新类型也以类似的方式指示GHC，为f 提供多态类型。

【讨论】：