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

Question

以下程序通过了类型检查：

{-# 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 编译也没有帮助。）

- frasertweedale

---

这可能是可怕的单态限制吗？ - Rein Henrichs

这不是单态限制。 - frasertweedale

这确实是类型系统中的限制。这个失败的程序需要正确检查类型的不定类型 ([test1,test2]::[forall a . ...]是不定类型)，根据文档， GHC只支持 "极其脆弱" 的不定式多态性，最好的解决方法是使用 newtype 包装器。或者打开 ImpredicativeTypes 并为程序的每个子项添加类型注释，直到它通过类型检查。 - user2407038

我也刚想起来ad有几个模块可以精确地解决GHC中的这个限制，例如diff。 - user2407038

Answer 1

这是 GHC 类型系统的一个问题。顺便提一下，这确实是 GHC 的类型系统；像 Haskell/ML 这样的语言的原始类型系统不支持更高阶的多态性，更不用说我们在这里使用的非确定性多态性了。

问题在于为了对此进行类型检查，我们需要支持在类型的任何位置上使用 forall。不仅仅是在类型的前面（允许类型推断的正常限制）。一旦你离开了这个区域，一般情况下类型推断就变得无法解决了（对于 n 阶多态性及以上）。在我们的情况下，[test1，test2] 的类型需要是 [forall a. Num a => a -> a]，这是一个问题，因为它不符合上述方案。它需要我们使用非确定性多态性，所谓的非确定性多态性是因为 a 取值范围包括其中带有 forall 的类型，因此 a 可以被替换为它所使用的类型。

因此，有些情况可能会出现问题，因为问题并不能完全解决。 GHC 对于等级 n 多态有一定的支持，并且对于不确定多态也有一些支持，但通常最好只使用新类型包装器来获得可靠的行为。据我所知，GHC 也反对使用这个特性，正是因为很难弄清楚类型推导算法将如何处理。

总之，math 表示会出现不稳定的情况，而使用 newtype 包装器是最好的方式，尽管有些令人不满意。

- Daniel Gratzer

---

“ImpredicativeTypes”在任何有意义的方式上都没有得到支持。 - dfeuer

Answer 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 这样使用包装器 newtype 也会以类似的方式指示 GHC，为 f 提供多态类型。

- chi