4

我一直在玩“freer monads”和可扩展效果，在freer-effects包中实现，我遇到了一个似乎可行但我无法解决的问题。

我编写了一个表示与文件系统的简单交互的类型：

data FileSystem v where
  ReadFile :: FilePath -> FileSystem String
  WriteFile :: FilePath -> String -> FileSystem ()

为此编写解释器IO很容易，但很无聊。我真正感兴趣的是编写一个State内部使用的纯解释器。我可以有效地将 的实现内联runState到我的解释器中FileSystem，但这似乎有点违背了目的。我真正想做的是编写这两种类型之间的转换，然后重用State解释器。

编写这样的转换很简单：

fsAsState :: forall v r. FileSystem v -> Eff (State [(FilePath, String)] ': r) v
fsAsState (ReadFile a) = (lookup a <$> get) >>=
  maybe (fail "readFile: file does not exist") return
fsAsState (WriteFile a b) = modify $ \fs ->
  (a, b) : filter ((/= a) . fst) fs

现在我想要一个可以接受我的转换并通过重用解释器来解释我的通用reencode函数。有了这样的功能，我就可以编写以下解释器：fsAsStateFileSystemState

runInMemoryFS :: forall r w. [(FilePath, String)] -> Eff (FileSystem ': r) w -> Eff r (w, [(FilePath, String)])
runInMemoryFS fs m = runState (reencode fsAsState m) fs

棘手的事情实际上是实施reencode。我得到了几乎可以进行类型检查的东西：

reencode :: forall r w f g. (forall v. f v -> Eff (g ': r) v) -> Eff (f ': r) w -> Eff (g ': r) w
reencode f m = loop m
  where
    loop :: Eff (f ': r) w -> Eff (g ': r) w
    loop (Val x) = return x
    loop (E u q) = case decomp u of
      Right x -> qComp q loop =<< f x
      Left u' -> E (weaken u') undefined

不幸的是，我不知道如何E在loop. 我认为我不了解优化FTCQueue类型如何工作的实现细节，以便了解我是否需要在这里做一些简单的事情，或者我正在做的事情是不可能的。

这可能吗？如果答案是否定的，并且事实证明我正在做的事情实际上是不可能的，那么我会对帮助我理解原因的解释感兴趣。

4

1 回答 1

2

免责声明：以下类型检查但我没有尝试运行它。

您需要步行q（从E u q模式匹配）并将其所有步骤从 转移Eff (f ': r)到Eff (g ': r)。我们可以多态地编写这个遍历：

shiftQ :: forall m n a b. (forall a. m a -> n a) -> FTCQueue m a b -> FTCQueue n a b
shiftQ shift q = case tviewl q of
    TOne act -> tsingleton (shift . act)
    act :| q -> go (tsingleton (shift . act)) q
  where
    go :: forall a b c. FTCQueue n a b -> FTCQueue m b c -> FTCQueue n a c
    go q' q = case tviewl q of
        TOne act -> q' |> (shift . act)
        act :| q -> go (q' |> (shift . act)) q

（这有点尴尬，因为我们只能 snoc 并且只能 uncons FTCQueues）。

然后我们可以reencode通过将reencode f自身作为shifter 来使用它：

reencode :: forall r w f g. (forall v. f v -> Eff (g ': r) v) -> Eff (f ': r) w -> Eff (g ': r) w
reencode f m = loop m
  where
    loop :: Eff (f ': r) w -> Eff (g ': r) w
    loop (Val x) = return x
    loop (E u q) = case decomp u of
      Right x -> qComp q loop =<< f x
      Left u' -> E (weaken u') (shiftQ (reencode f) q)
于 2017-07-03T02:02:54.787 回答