最近的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)
如果我们能够提供通常的 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
中的证明计算,但这似乎会导致类型索引的无限递归。
最佳答案
这是通过假设参数定理完成的某种形式的解决方案。 它还确保假设不会妨碍计算。
http://code.haskell.org/~Saizan/ST/ST.agda
“darcs get http://code.haskell.org/~Saizan/ST/”获取完整源代码
我对类型的封闭宇宙并不满意,但这是根据我们实际需要定制参数定理的简单方法。
关于haskell - 在 Agda 中对 ST monad 进行建模,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/34023712/