为什么函数类型需要被“包装”才能满足类型检查器？

下面的程序类型检查：为什么函数类型需要被“包装”才能满足类型检查器？

{-# 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没有帮助）

来源

2017-08-08 frasertweedale

难道这是可怕的单态吗？ –

这不是单态限制。 – frasertweedale

这实际上是类型系统中的一个限制。失败的程序需要对意想不到的类型进行正确的类型检查（'[test1，test2] :: [forall a。...]'是不可预测的），这是[docs]（https：//downloads.haskell。 org /〜ghc/latest/docs/html/users_guide/glasgow_exts.html＃impredicative-polymorphism）声称，GHC只有“非常片状的支持”。最好的解决方法是'newtype'包装。或者，打开ImpredicativeTypes并为程序的每个子项添加类型注释，直到它被敲入。 – user2407038

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

问题是，为了打字检查，我们需要在类型的任何位置支持forall。不仅在类型前面一直束缚（允许类型推断的正常限制）。一旦你离开这个区域，类型推断通常会变得不可判定（对于n级多态性和超越）。在我们的例子中，[test1, test2]的类型需要是[forall a. Num a => a -> a]，考虑到它不适合上面讨论的方案，这是一个问题。这将需要我们使用impredicative多态性，所谓的，因为a范围内的类型与forall s在其中，因此a可以被它所使用的类型所取代。

因此，会出现一些不正当的情况，因为问题不能完全解决。 GHC确实对rank n多态性有一定的支持，并且对implicitic polymorphism有点支持，但通常使用newtype包装来获得可靠的行为通常会更好。据我所知，GHC也不赞成使用这个特性，因为很难弄清楚类型推理算法会处理什么。

综上所述，math表示会有片状的情况，newtype包装纸是最好的，如果有些不满意的方式，以应付它。

来源

2017-08-08 08:57:33 jozefg

“ImpredicativeTypes”实际上并未得到任何有意义的支持。 – dfeuer

类型推理算法（在->左边那些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这样的包装类型也会以类似的方式指示GHC，为f提供多态类型。

来源

2017-08-08 08:56:27 chi

为什么函数类型需要被“包装”才能满足类型检查器？

回答

相关问题