在Agda建模ST monad

这个最近的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)

如果我们能够提供通常的ST monad API,那将会很好unsafeCoerce.具体来说,我想说明为什么通常的GHC ST monad和上面的仿真工作的原因.在我看来,他们的工作原因是:

任何STRef s a具有正确s标签的必须在当前ST计算中创建,因为runST确保不能混合不同的状态.

前一点以及ST计算只能扩展引用环境这一事实意味着任何STRef s a具有正确s标记的事件都指向环境中的有效a类型位置(在运行时可能弱化引用之后).

以上几点可以实现显着的免费证明编程体验.在我能想到的安全和纯粹的Haskell中,没有什么能真正接近; 我们可以使用索引状态monad和异构列表进行相当差的模仿,但这并不表示上述任何一点,因此需要在STRef-s的每个使用站点进行校对.

我不知道如何在Agda中正确地形式化这一点.对于初学者来说,"在这个计算中分配"是非常棘手的.我想将STRef-s 表示为特定分配包含在特定ST计算中的证据,但这似乎导致类型索引的无限递归.