12

GHC 用户指南参考以下示例描述了暗示性多态性扩展：

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, orJust undefined满足类型检查器。

因此，我有两个问题：

  • 可以Just f为任何非底部调用上述函数f吗？
  • 有人可以提供一个值的示例，该值只能用暗示性多态性来定义，并且可以以非平凡的方式使用吗？

后者尤其是考虑到有关 Impredicative Polymorphism 的 HaskellWiki 页面，这目前为扩展的存在提供了一个绝对没有说服力的案例。

4

3 回答 3

7

ImpredicativeTypesghc-7+ 中的新类型检查器不只是悄悄地放弃了这一点吗？请注意，ideone.com 仍然使用 ghc-6.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 dsl——并在这里为扩展辩护：http: //augustss.blogspot.com/2011/07/impredicative-polymorphism-use-case-in.html提到在这里的票http://hackage.haskell.org/trac/ghc/ticket/4295

于 2012-12-27T02:16:41.943 回答
7

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

这个想法是，当我们有 form 的表达式时App (PrimOp nameStr) (Lit litVal)，我们希望根据 primop 名称查找适当的规则。AlitVal将是 aMachFloat d或MachDouble d(d是 a 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，我们可以保留 Rank-2 函数的列表，准备用于 的第一个参数mkUnaryCollapsePrimIEEE。替代方案将是更多的 CPP/样板、更改模块结构（或循环导入）或大量代码重复。没有一个是我想要的。

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

于 2012-12-28T06:22:20.500 回答
5

请注意此解决方法：

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在您的情况下推断类型有问题，我们必须告诉它类型。

我不知道这是一个错误还是有充分的理由.. :)

于 2012-12-27T00:09:05.450 回答