在Agda中对ST monad建模 [英] Modeling the ST monad in Agda

问题描述

这最近 SO问题促使我在Haskell中编写了一个不安全和纯粹的ST monad仿真，稍微修改后的版本可以在下面看到：

  { - ＃LANGUAGE DeriveFunctor，GeneralizedNewtypeDiving，RankNTypes＃ - } 
 
 import Control.Monad.Trans.State 
 import GHC.Prim（Any）
 import不安全。 Coerce（unsafeCoerce）
 import Data.List 
 
 newtype ST sa = ST（State（[Any]，Int）a）派生（Functor，Applicative，Monad）
 newtype STRef sa = STRef Int派生Show 
 
 newSTRef :: a  - > ST s（STRef sa）
 newSTRef a = ST $ do 
（env，i）<  -  get 
 put（unsafeCoerce a：env，i + 1）
 pure STRef i）
 
 update :: [a]  - > （a  - > a） - > Int  - > [a] 
更新为f i = case splitAt i as of 
（as，b：bs） - > as ++ f b：bs 
 _  - > as 
 
 readSTRef :: STRef s a  - > ST sa 
 readSTRef（STRef i）= ST $ do 
（m，i'）< -  get 
 pure（unsafeCoerce（m !!（i' -  i  -  1））） 
 
 modifySTRef :: STRef sa  - > （a  - > a） - > ST s（）
 modifySTRef（STRef i）f = ST $ 
修改$ \（env，i'） - > （更新env（unsafeCoerce f）（i' -  i-1），i'）
 
 runST ::（全部.ST s a） - > a 
 runST（ST s）= evalState s（[]，0）
  

如果我们可以提供通常的ST monad API，而不需要 unsafeCoerce ，那就太好了。具体来说，我想正式说明为什么常见的GHC ST monad和上述仿真工作的原因。在我看来，他们的工作原因是：

• 任何 STRef sa s tag 必须在当前ST计算中创建，因为 runST 确保不同各州不能混为一谈。 前一点与ST计算只能扩展引用环境的事实意味着任何 STRef sa s 标记引用环境中有效的 a 类型的位置（在运行时可能削弱引用之后）。 上述几点可以为您提供一种无需证明义务的编程体验。在我能想到的安全和纯正的Haskell中，没有任何东西能够接近真实;我们可以用索引状态monads和异构列表做一个相当差的模仿，但是这并不表示上述任何一点，因此需要在 STRef 的每个使用站点上进行证明。 s。
  
  

  我很茫然，我们可以在Agda中正确定义这一点。对于初学者来说，在这个计算中分配是非常棘手的。我想过代表 STRef -s作为特定分配包含在特定 ST 计算中的证据，但似乎导致类型索引的无限递归。

  解决方案

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

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

  
  
  

  darcs get http://code.haskell.org/~Saizan/ST/ 对于完整的源代码
  
  

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

  
  

  This recent SO question prompted me to write an unsafe and pure emulation of the ST monad in Haskell, a slightly modified version of which you can see below:

  {-# 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)
  

  It would be good if we could present the usual ST monad API without unsafeCoerce. Specifically, I'd like to formalize the reasons why the usual GHC ST monad and the above emulation works. It seems to me that they work because:

  • Any STRef s a with the right s tag must have been created in the current ST computation, since runST ensures that different states can't be mixed up.
  • The previous point together with the fact that ST computations can only ever extend the environment of references implies that any STRef s a with the right s tag refers to a valid a-typed location in the environment (after possibly weakening the reference at runtime).

  The above points enable a remarkably proof-obligation-free programming experience. Nothing really comes close in safe and pure Haskell that I can think of; we can do a rather poor imitation with indexed state monads and heterogeneous lists, but that doesn't express any of the above points and thus requires proofs at each use site of STRef-s.

  I'm at a loss how we could formalize this properly in Agda. For starters, "allocated in this computation" is tricky enough. I thought about representing STRef-s as proofs that a particular allocation is contained in a particular ST computation, but that seems to result in an endless recursion of type indexing.

  解决方案

  Here's some form of a solution done by postulating a parametricity theorem. It also ensures that the postulate does not get in the way of computation.

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

  "darcs get http://code.haskell.org/~Saizan/ST/" for the full source

  I'm not happy about the closed universe of types but it's the easy way to tailor the parametricity theorem to what we actually need.

  这篇关于在Agda中对ST monad建模的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！