3

以下程序类型检查:

{-# 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如上所述)之外的任何可能的解决方法。

(注意:这不是由单态限制引起的;编译 withNoMonomorphismRestriction没有帮助。)

4

2 回答 2

8

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

问题是,为了进行类型检查,我们需要forall在类型中的任何位置支持 s。不仅在类型的前面一直聚在一起(允许类型推断的正常限制)。一旦你离开这个区域,类型推断通常变得无法确定(对于 rank n 多态性及以上)。在我们的例子中,考虑到它不适合上面讨论的方案,类型[test1, test2]需要是一个问题。[forall a. Num a => a -> a]这将要求我们使用暗示性多态性,之所以这么称呼是因为a范围覆盖了其中包含foralls 的类型,因此a可以用它所使用的类型替换。

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

总而言之,数学表明会有一些不稳定的情况,并且newtype包装是最好的,如果有点不满意的话,可以应付它。

于 2017-08-08T08:57:33.517 回答
3

类型推断算法不会推断出更高等级的类型(带有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签名。

使用包装器 newtype likeFun也以类似的方式指示 GHC,为f.

于 2017-08-08T08:56:27.437 回答