在变压器堆栈中展开STT单片？

Question

这个问题显然与这里和这里讨论的问题有关。不幸的是，我的要求与这些问题略有不同，所给出的答案不适用于我。我也不太明白为什么runST不能在这些情况下键入check，这是没有帮助的。

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

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

另一段代码需要与此集成，将其封装在STT单模中。

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层后返回它，但我似乎无法做到这一点，因为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-changing)效应从外部的纯世界中分离出来。所有s计算、STRef等被标记的ST幻影类型的全部要点是跟踪它们属于哪个"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 (一个去骨化变量)作为s，因此试图将ST s a与ST s1 a统一起来。