微信公众号搜"智元新知"关注
微信扫一扫可直接关注哦!

Haskell 可扩展效果:另一种效果中的效果

如何解决Haskell 可扩展效果:另一种效果中的效果

我正在尝试使用 extensible-skeleton 包。 在另一个效果中堆叠一个效果会导致编译错误。 我尝试了一些其他语言扩展和类型注释,但无法消除这些错误。 如何解决这些错误

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Main where

import Data.Extensible
import Data.Extensible.Effect
import Data.Type.Equality

type In0 effs = Lookup effs "io" IO
type In1 effs = Lookup effs "reader-float" (ReaderEff Double)

run0 :: forall a. Eff '["io" >: IO] a -> IO a
run0 = retractEff

run1 :: forall effs a. Double -> Eff (("reader-float" >: ReaderEff Double) ': effs) a -> Eff effs a
run1 x = peelEff0 pure $ \Refl k -> k x

lift0 :: forall effs a. In0 effs => IO a -> Eff effs a
lift0 = liftEff (Proxy :: Proxy "io")

ask1 :: forall effs. In1 effs => Eff effs Double
ask1 = askEff (Proxy :: Proxy "reader-float")

eff0 :: forall effs. In0 effs => Eff effs ()
eff0 = do
  lift0 $ print "eff0"
  run1 2.5 eff1

eff1 :: forall effs. (In0 effs,In1 effs) => Eff effs ()
eff1 = do
  x <- ask1
  lift0 $ print "eff1"
  lift0 $ print (floor x)

main :: IO ()
main = do
  run0 eff0

编译时的错误

[1 of 2] Compiling Main
app/Main.hs:32:12: error:
    • Couldn't match type ‘membership-0:Type.Membership.Internal.Elaborate
                             "io" (membership-0:Type.Membership.Internal.FindAssoc 1 "io" effs)’
                     with ‘'membership-0:Type.Membership.Internal.Expecting (n0 ':> IO)’
        arising from a use of ‘eff1’
      The type variable ‘n0’ is ambiguous
    • In the second argument of ‘run1’,namely ‘eff1’
      In a stmt of a 'do' block: run1 2.5 eff1
      In the expression:
        do lift0 $ print "eff0"
           run1 2.5 eff1
    • Relevant bindings include
        eff0 :: Eff effs () (bound at app/Main.hs:30:1)
   |
32 |   run1 2.5 eff1
   |            ^^^^

怎么了?

解决方法

问题似乎是 run1(顺便说一下,它已经作为 runReaderEff 可用)接受最外层为 "reader-float" 的效果,但效果 {{1} } 您试图 eff1 只满足 run1,这保证 In1 effs 在某处,但不一定在最外层。

这反映了一个事实,即您无法运行埋在堆栈中的任意层。您需要从外到内运行这些层。

有效的是为 "reader-float" 构建显式效果堆栈,然后向上转换:

eff1

您似乎想在 eff0 :: forall effs. In0 effs => Eff effs () eff0 = do lift0 $ print "eff0" castEff $ run1 2.5 (eff1 :: Eff '["reader-float" :> ReaderEff Double,"io" :> IO] ()) "reader-float" 前面加上 effs,所以这样写:

eff0

但这不起作用。但是,如果您仔细考虑一下,除了特定的 {-# LANGUAGE ScopedTypeVariables #-} eff0 :: forall effs. In0 effs => Eff effs () eff0 = do lift0 $ print "eff0" castEff $ run1 2.5 (eff1 :: Eff (("reader-float" :> ReaderEff Double) ': effs) ()) 堆栈之外,没有理由在此处运行 eff1

请记住,在 ["reader-float","io"]effs 的类型签名中使用通用 eff0 的原因是让它们与所需的层一起用于任何效果堆栈;一般类型签名是为了调用者的利益。在这种情况下,eff1 正在调用 eff0,它没有理由为 eff1 提供它需要的层以外的任何东西,即它在本地构造的新 eff1 层,以及它投射到自己的通用 "reader-float" 环境中的“io”层。 effseffs 没有对 eff0 感兴趣,因此无需将 eff1effs 向下传播到 eff0。>

版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。