首页 文章

在变压器堆栈中展开STT monad？

提问于
浏览 次
2

这个问题显然与讨论的问题here和here有关 . 不幸的是，我的要求与这些问题略有不同，并且给出的答案真的很难理解为什么 runST 在这些情况下无法输入检查，这无济于事 .

我的问题是，我有一段代码使用一个monad堆栈，或者更确切地说是一个monad：

import Control.Monad.Except
type KErr a = Except KindError a

另一部分代码需要与此集成，将其包装在_1123063中：

type RunM s a = STT s (Except KindError) a

在这些部分之间的界面上，我显然需要包裹和展开外层 . 我有以下功能在 KErr - > RunM 方向工作：

kerrToRun :: KErr a -> RunM s a
kerrToRun e = either throwError return $ runExcept e

但由于某种原因，我只是不能反过来键入检查：

runToKErr :: RunM s a -> KErr a
runToKErr r = runST r

我正在假设由于 RunM 的内部monad具有与 KErr 相同的结构，所以我可以在我打开 STT 层后返回它，但我似乎无法达到那么远， as runST 抱怨其类型参数：

src/KindLang/Runtime/Eval.hs:18:21:
    Couldn't match type ‘s’ with ‘s1’
      ‘s’ is a rigid type variable bound by
          the type signature for runToKErr :: RunM s a -> KErr a
          at src/KindLang/Runtime/Eval.hs:17:14
      ‘s1’ is a rigid type variable bound by
           a type expected by the context:
             STT s1 (ExceptT KindError Data.Functor.Identity.Identity) a
           at src/KindLang/Runtime/Eval.hs:18:15
    Expected type: STT
                     s1 (ExceptT KindError Data.Functor.Identity.Identity) a
      Actual type: RunM s a

我也尝试过：

runToKErr r = either throwError return $ runExcept $ runST r

为了更好地隔离 runST 与其预期的返回类型，如果是问题的原因，但结果是相同的 .

这个 s1 类型来自哪里，我如何说服ghc它与 s 的类型相同？

haskell polymorphism higher-rank-types

1 回答

  • 5

    （下面谈到 ST s a 但是和_1123079一样适用;我刚刚避免了下面谈论变压器版本的不必要的复杂性）

    您看到的问题是 runST 具有类型 (forall s. ST s a) -> a ，以隔离来自外部纯净世界的任何潜在（ STRef -交换）计算效果 . 所有 ST 计算， STRef 等被标记的 s 幻像类型的整个点是跟踪它们属于哪个“ ST -domain”;并且 runST 的类型确保域之间不能传递任何内容 .

    您可以通过强制执行相同的不变量来编写 runToKErr ：

    {-# language Rank2Types #-}

runToKErr :: (forall s. RunM s a) -> KErr a
runToKErr = runST

    （当然，你可能会意识到这个限制对于你希望编写的程序来说太强了;在那一点上你需要失去希望，对不起，我的意思是你需要重新设计你的程序 . ）

    至于错误信息，你不能“说服类型检查器 s1 和 s 是同一类型”的原因是因为如果我为 s 和 a 的给定选择传递 ST s a ，这与给出的不同你可以选择自己的 s . GHC选择 s1 （Skolemized变量）为 s ，因此尝试将 ST s a 与 ST s1 a 统一

    回复于

相关问题