这个最近的SO 问题促使我在 Haskell 中编写了一个不安全且纯粹的 ST monad 仿真，您可以在下面看到一个稍微修改过的版本：
{-# LANGUAGE DeriveFunctor, GeneralizedNewtypeDeriving, RankNTypes #-}
import Control.Monad.Trans.State
import GHC.Prim (Any)
import Unsafe.Coerce (unsafeCoerce)
import Data.List
newtype ST s a = ST (State ([Any], Int) a) deriving (Functor, Applicative, Monad)
newtype STRef s a = STRef Int deriving Show
newSTRef :: a -> ST s (STRef s a)
newSTRef a = ST $ do
(env, i) <- get
put (unsafeCoerce a : env, i + 1)
pure (STRef i)
update :: [a] -> (a -> a) -> Int -> [a]
update as f i = case splitAt i as of
(as, b:bs) -> as ++ f b : bs
_ -> as
readSTRef :: STRef s a -> ST s a
readSTRef (STRef i) = ST $ do
(m, i') <- get
pure (unsafeCoerce (m !! (i' - i - 1)))
modifySTRef :: STRef s a -> (a -> a) -> ST s ()
modifySTRef (STRef i) f = ST $
modify $ \(env, i') -> (update env (unsafeCoerce f) (i' - i - 1), i')
runST :: (forall s. ST s a) -> a
runST (ST s) = evalState s ([], 0)
如果我们可以在没有unsafeCoerce. 具体来说，我想正式说明通常的 GHC ST monad 和上述仿真起作用的原因。在我看来，它们之所以起作用，是因为：
- 任何
STRef s a带有正确s标签的都必须在当前 ST 计算中创建，因为runST确保不会混淆不同的状态。 - 前一点加上 ST 计算只能扩展引用环境这一事实意味着任何
STRef s a具有正确s标记的对象都引用了环境中的有效a类型位置（在运行时可能会削弱引用之后）。
以上几点可实现显着的无证明义务的编程体验。在我能想到的安全和纯粹的 Haskell 中，没有什么能比得上真正的；我们可以用索引状态单子和异构列表做一个相当糟糕的模仿，但这并没有表达上述任何一点，因此需要在STRef-s 的每个使用站点进行证明。
我不知道我们如何在 Agda 中正确地将其正式化。对于初学者来说，“在这个计算中分配”已经够棘手了。我曾考虑将STRef-s 表示为特定分配包含在特定ST计算中的证明，但这似乎导致类型索引的无休止递归。