gpt4 book ai didi

haskell - ImpredicativeTypes 的简单示例

转载 作者:行者123 更新时间:2023-12-04 00:44:52 26 4
gpt4 key购买 nike

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 dMachDouble d ( dRational )。如果我们找到一条规则,我们想将该规则的函数应用于 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 总部表示他们想放弃对扩展的支持,但也许他们已经重新考虑过了。它有时非常有用。

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

    26 4 0
    Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
    广告合作:1813099741@qq.com 6ren.com