ImpredicativeTypes的简单示例

Question

GHC用户指南引用以下示例描述了impredicative polymorphism extension：

f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
f (Just g) = Just (g [3], g "hello")
f Nothing  = Nothing

但是，当我在文件中定义这个示例并试图调用它时，我会得到一个类型错误：

ghci> f (Just reverse)

<interactive>:8:9:
    Couldn't match expected type `forall a. [a] -> [a]'
                with actual type `[a0] -> [a0]'
    In the first argument of `Just', namely `reverse'
    In the first argument of `f', namely `(Just reverse)'
    In the expression: f (Just reverse)
ghci> f (Just id)

<interactive>:9:9:
    Couldn't match expected type `forall a. [a] -> [a]'
                with actual type `a0 -> a0'
    In the first argument of `Just', namely `id'
    In the first argument of `f', namely `(Just id)'
    In the expression: f (Just id)

似乎只有undefined、Nothing或Just undefined满足类型检查器。

因此，我有两个问题：

• 对于任何非底层的Just f，可以调用上述函数吗？
• 有人能提供一个值的例子，这个值只能用非谓词多态来定义，并且可以以一种非平凡的方式使用吗？

后者尤其考虑到了HaskellWiki page on Impredicative Polymorphism，它目前为扩展的存在提供了一个完全没有说服力的理由。

Answer 1

下面是一个项目const-math-ghc-plugin如何使用ImpredicativeTypes来指定匹配规则列表的示例。

这样做的想法是，当我们有一个表单App (PrimOp nameStr) (Lit litVal)的表达式时，我们希望根据primop名称查找适当的规则。litVal要么是MachFloat d，要么是MachDouble d (d是Rational)。如果我们找到一个规则，我们希望将该规则的函数应用到转换为正确类型的d。

函数mkUnaryCollapseIEEE为一元函数执行此操作。

mkUnaryCollapseIEEE :: (forall a. RealFloat a => (a -> a))
                    -> Opts
                    -> CoreExpr
                    -> CoreM CoreExpr
mkUnaryCollapseIEEE fnE opts expr@(App f1 (App f2 (Lit lit)))
    | isDHash f2, MachDouble d <- lit = e d mkDoubleLitDouble
    | isFHash f2, MachFloat d  <- lit = e d mkFloatLitFloat
    where
        e d = evalUnaryIEEE opts fnE f1 f2 d expr

第一个参数需要一个Rank-2类型，因为它将在Float或Double上实例化，这取决于文字构造函数。规则列表如下：

unarySubIEEE :: String -> (forall a. RealFloat a => a -> a) -> CMSub
unarySubIEEE nm fn = CMSub nm (mkUnaryCollapseIEEE fn)

subs =
    [ unarySubIEEE "GHC.Float.exp"    exp
    , unarySubIEEE "GHC.Float.log"    log
    , unarySubIEEE "GHC.Float.sqrt"   sqrt
    -- lines omitted
    , unarySubIEEE "GHC.Float.atanh"  atanh
    ]

这个没问题，如果我的口味有点麻烦的话。

然而，有一个类似的函数mkUnaryCollapsePrimIEEE。在这种情况下，对于不同的GHC版本，规则是不同的。如果我们想要支持多个GHC，它会变得有点棘手。如果我们采用同样的方法，subs定义将需要大量的CPP，这可能是不可维护的。相反，我们为每个GHC版本在一个单独的文件中定义了规则。但是，由于循环导入问题，这些模块中无法使用mkUnaryCollapsePrimIEEE。我们可能会重新构造模块以使其工作，但我们将规则集定义为：

unaryPrimRules :: [(String, (forall a. RealFloat a => a -> a))]
unaryPrimRules =
    [ ("GHC.Prim.expDouble#"    , exp)
    , ("GHC.Prim.logDouble#"    , log)
    -- lines omitted
    , ("GHC.Prim.expFloat#"     , exp)
    , ("GHC.Prim.logFloat#"     , log)
    ]

通过使用ImpredicativeTypes，我们可以保留一个秩-2函数的列表，可以用于mkUnaryCollapsePrimIEEE的第一个参数。替代方案将是更多的CPP/样板，更改模块结构(或循环导入)，或大量重复代码。这些我都不喜欢。

我似乎记得GHC总部表示，他们想放弃对扩展的支持，但也许他们已经重新考虑过了。它有时很有用。

Answer 2

难道不是因为ImpredicativeTypes已经被ghc-7+中的新打字机悄悄丢弃了吗？请注意，ideone.com仍然使用ghc-6.8，而且您的程序确实使用GHC6.8来运行：

{-# OPTIONS -fglasgow-exts  #-}

f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
f (Just g) = Just (g [3], g "hello")
f Nothing  = Nothing

main   = print $ f (Just reverse)

按预期打印Just ([3],"olleh")；请参见http://ideone.com/KMASZy

augustss给出了一个漂亮的用例--某种模仿Python -并在这里为扩展进行了辩护:在这里http://hackage.haskell.org/trac/ghc/ticket/4295中提到的http://augustss.blogspot.com/2011/07/impredicative-polymorphism-use-case-in.html。

Answer 3

注意这个解决办法：

justForF :: (forall a. [a] -> [a]) -> Maybe (forall a. [a] -> [a])
justForF = Just

ghci> f (justForF reverse)
Just ([3],"olleh")

或者这个(基本上是相同的内容)：

ghci> f $ (Just :: (forall a. [a] -> [a]) -> Maybe (forall a. [a] -> [a])) reverse
Just ([3],"olleh")

在您的情况下，类型推断似乎存在推断Just类型的问题，我们必须告诉它类型。

我不知道它是个虫子还是有一个很好的理由。:)