haskell - 在变压器堆栈中展开 STT 单子(monad)？

Question

这个问题显然与讨论的问题here相关。和 here 。不幸的是，我的要求与这些问题略有不同，并且给出的答案不适用于我。我也不太明白为什么 runST 在这些情况下无法进行类型检查，这没有帮助。

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

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

另一段代码需要与此集成，将其包装在 STT monad 中:

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

在这些部分之间的接口(interface)处，我显然需要包裹和展开外层。我有以下函数可以在 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 层，但我似乎无法做到这一点，因为 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 类型相同？

Answer 1

(下面讨论的是 ST s a，但应用与 STT s m a 相同；我只是避免了下面讨论变压器版本带来的不必要的复杂性)

您看到的问题是 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 是同一类型”的原因是，如果我向您传递一个ST s a 对于 s 和 a 的给定选择，这与给您一些允许您选择自己的 不同>s。 GHC 选择 s1(Skolemized 变量)作为 s，因此尝试将 ST s a 与 ST s1 a 统一>