以下程序通过了类型检查:
{-# 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 . ...]
是不定类型),根据文档, GHC只支持 "极其脆弱" 的不定式多态性,最好的解决方法是使用newtype
包装器。或者打开ImpredicativeTypes
并为程序的每个子项添加类型注释,直到它通过类型检查。 - user2407038ad
有几个模块可以精确地解决GHC中的这个限制,例如diff
。 - user2407038