为什么需要"wrapped"函数类型才能满足类型检查器?



以下程序类型检查:

{-# 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无济于事。

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

问题是,为了类型检查,我们需要在类型中的任何位置支持foralls。不仅一直聚集在类型的前面(允许类型推断的正常限制(。一旦你离开这个区域,类型推断通常变得不可判定(对于秩n多态性及更高(。在我们的例子中,需要[forall a. Num a => a -> a][test1, test2]的类型,考虑到它不适合上面讨论的方案,这是一个问题。它要求我们使用非谓词多态性,之所以这样称呼,是因为a范围超过包含foralls 的类型,因此a可以替换为

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

总之,数学说会有片状的情况,newtype包装器是最好的,如果有点不满意,来应对它。

类型推断算法不会推断更高等级的类型(->左侧有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提供多态类型。

相关内容

  • 没有找到相关文章

最新更新