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

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类语言的原始类型系统不支持更高级别的多态性,更不用说我们在这里使用的impredicative polymorphism.

问题是,为了键入检查,我们需要forall在类型的任何位置支持s.不仅在类型的前面一直聚集(允许类型推断的正常限制).一旦你离开这个区域,类型推断一般就变得不可判定了(对于秩n多态和其他).在我们的例子中,类型[test1, test2]将需要[forall a. Num a => a -> a]这是考虑到它不适合上面讨论的方案有问题.它需要我们使用impredicative多态,所谓的因为a范围超过foralls中的类型,因此a可以用它所使用的类型替换.

所以,因为问题不能完全解决,所以会出现一些行为不端的情况.GHC确实对rank n多态性有一些支持,并且对impredicative polymorphism有一些支持,但通常使用newtype包装器来获得可靠的行为通常会更好.据我所知,GHC也不鼓励使用这个功能,因为很难弄清楚类型推断算法将要处理的确切内容.

总而言之,数学表明会有片状的情况,newtype包装是最好的,如果有点不满意,应对它.