haskell - ImpredicativeTypes 的简单示例

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 是否可以使用 f 调用上述函数？

有人能提供一个只能用不可预测的多态定义的值的例子吗？

后者特别是考虑到 HaskellWiki page on Impredicative Polymorphism，这对于扩展的存在来说目前是一个明显没有说服力的案例。

最佳答案

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

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

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

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 类型，因为它将在 mkUnaryCollapseIEEE 或 Float 处实例化，具体取决于文字构造函数。规则列表如下所示:

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
    ]

这没关系，如果我的口味有点太多样板。

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

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)
    ]

通过使用 mkUnaryCollapsePrimIEEE ，我们可以保留一个 Rank-2 函数的列表，准备用于 ImpredicativeTypes 的第一个参数。替代方案将是更多的 CPP/样板，改变模块结构(或循环导入)，或者大量的代码重复。没有我想要的。

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

关于haskell - ImpredicativeTypes 的简单示例，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/14047241/