在 Agda 中建模 ST monad

Question

最近的 SO question 促使我在 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 的情况下呈现通常的 ST monad API 就好了。具体来说，我想正式说明通常的 GHC ST monad 和上述仿真工作的原因。在我看来，它们起作用是因为：

具有正确s标签的任何STRef s a必须在当前ST计算中创建，因为runST确保不同的状态不能混淆。
前一点以及 ST 计算只能扩展引用环境这一事实意味着任何带有正确 s 标签的 STRef s a 都指代有效的 a-环境中的类型化位置（在运行时可能削弱引用之后）。

以上几点实现了非常无证明义务的编程体验。在我能想到的安全和纯粹 Haskell 中，没有什么比这更接近的了；我们可以用索引状态 monad 和异构列表做一个相当糟糕的模仿，但这并没有表达上述任何一点，因此需要在 STRef-s.

的每个使用站点进行证明

我不知道我们如何在 Agda 中正确地将其形式化。对于初学者来说，"allocated in this computation" 已经足够棘手了。我考虑过将 STRef-s 表示为特定分配包含在特定 ST 计算中的证明，但这似乎会导致类型索引的无休止递归。

Answer 1

这是通过假设参数定理完成的某种形式的解决方案。它还确保假设不会妨碍计算。

http://code.haskell.org/~Saizan/ST/ST.agda

"darcs get http://code.haskell.org/~Saizan/ST/" 完整来源

我对类型的封闭宇宙不满意，但这是根据我们实际需要调整参数定理的简单方法。

在 Agda 中建模 ST monad

Modeling the ST monad in Agda

haskell

agda

st-monad