haskell - 为什么需要函数类型为 "wrapped"才能满足类型检查器的要求？

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没有帮助。)

Answer 1

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

问题是为了进行类型检查，我们需要支持 forall s 在类型中的任何位置。不仅在类型的前面一直聚在一起(允许类型推断的正常限制)。一旦离开这个区域，类型推断通常就变得不可判定(对于 n 级多态性及更高级别)。在我们的例子中，类型是 [test1, test2]需要是 [forall a. Num a => a -> a]考虑到它不适合上面讨论的方案，这是一个问题。这将要求我们使用不可预测的多态性，之所以这样称呼是因为 a使用 forall 覆盖类型s 在他们等等 a可以替换为正在使用的类型。

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

总之，math说会有片状的情况和newtype包装器是处理它的最佳方式，即使有些不满意。