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

Question

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

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

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

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

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计算与外部纯净世界的任何潜在(改变)效果的类型.s所有ST计算,STRefs等被标记的幻像类型的整个点是跟踪ST它们属于哪个" 域"; 以及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