ImpredicativeTypes的简单示例

Question

GHC用户指南参考以下示例描述了impredicative polymorphism扩展:

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为任何非底部调用上述函数f吗？
• 有人可以提供一个只能用不可预测的多态性定义的值的例子,并且可以以非平凡的方式使用吗？

后者特别是关于Impredicative Polymorphism的HaskellWiki页面,它目前对扩展的存在做出了令人难以置信的案例.

Answer 1

是不是只是ImpredicativeTypes用ghc-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

Answer 2

这里有一个如何一个项目,一个例子常量,数学GHC-插件,使用ImpredicativeTypes指定的匹配规则列表.

我们的想法是,当我们有表单的表达式时App (PrimOp nameStr) (Lit litVal),我们希望根据primop名称查找适当的规则.A litVal将是a MachFloat 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 HQ表示他们希望放弃对扩展的支持,但也许他们已经重新考虑了.它有时非常有用.

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您的案例类型方面存在问题,我们必须告诉它类型.

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