2

我正在尝试使用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
   |            ^^^^

怎么了？

4

1 回答 1

1

问题似乎是run1（顺便说一句，它已经可用runReaderEff）接受最外层为"reader-float"的效果，但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"在effsfor前面加上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使用general 的原因eff1是为了让它们在具有所需层的任何效果堆栈中使用；一般类型签名是为了调用者的利益。在这种情况下，eff0正在调用，除了它需要的层、它在本地构造的新层以及它投射到它自己的一般环境中的“io”层之外，它eff1没有理由提供任何东西。没有其他对or感兴趣的东西，所以不需要从to向下传播。eff1"reader-float"effseffseff0eff1effseff0eff1

于 2020-12-23T19:13:13.607 回答