【问题标题】:Haskell extensible effects: effect in another effectHaskell 可扩展效果:另一种效果中的效果
【发布时间】:2021-04-02 01:23:09
【问题描述】:

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

怎么了?

【问题讨论】:

    标签: haskell extensible


    【解决方案1】:

    问题似乎是run1(顺便说一下,它已经以runReaderEff 提供)接受最外层为"reader-float" 的效果,但您尝试@ 的效果eff1 987654325@只满足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] ())
    

    您似乎想在effs 前面添加"reader-float" 以表示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) ())
    

    但这不起作用。但是,如果您考虑一下,除了特定的 ["reader-float", "io"] 堆栈之外,没有理由在此处运行 eff1

    请记住,在eff0eff1 的类型签名中使用通用effs 的原因是为了让它们在具有所需层的任何效果堆栈中使用;一般类型签名是为了调用者的利益。在这种情况下,eff0 正在调用eff1,它没有理由向eff1 提供除了它需要的层、它在本地构造的新"reader-float" 层和它的“io”层之外的任何东西。它投射到自己的一般effs 环境中。在effs 中没有任何其他内容对eff0eff1 感兴趣,因此无需将effseff0 传播到eff1

    【讨论】:

    • 第二个代码 sn-p 是我想做的。在没有显式效果堆栈的情况下,是否不可能将effseff0 传播到eff1?例如,将In2ask2run2 定义为与"reader-int" 相同的方式。 eff2 = (ask1 &gt;&gt;= (lift0 . print)) &gt;&gt; (ask2 &gt;&gt;= (lift0 . print))eff1 = ask1 &gt;&gt;= (\x -&gt; run2 (floor x) eff2)。这种情况需要将effseff1向下传播到eff2
    • 然后eff1 应该使用显式堆栈["reader-int", "reader-float", "io"] 调用eff2,通过runReaderEff 提供reader-int 并将["reader-float", "io"] 转换为其effs。您永远不会处于调用效果中“需要”未指定 effs 的情况。
    猜你喜欢
    • 1970-01-01
    • 1970-01-01
    • 2012-01-28
    • 2018-01-27
    • 2021-05-28
    • 1970-01-01
    • 2016-08-04
    • 1970-01-01
    • 1970-01-01
    相关资源
    最近更新 更多