可以纯粹执行类似“ST”的 monad（没有“ST”库）吗？

Question

这篇文章是识字的 Haskell。只需放入“pad.lhs”之类的文件，ghci 就可以运行它。

> {-# LANGUAGE GADTs, Rank2Types #-}
> import Control.Monad
> import Control.Monad.ST
> import Data.STRef

好的，所以我能够弄清楚如何用纯代码表示 ST monad。首先，我们从引用类型开始。它的具体值并不重要。最重要的是PT s a 不应该与任何其他类型forall s 同构。 （特别是，它应该与() 和Void 都不同构。）

> newtype PTRef s a = Ref {unref :: s a} -- This is defined liked this to make `toST'` work. It may be given a different definition.

s 的类型是 *->*，但现在这并不重要。可能是polykind，我们只关心。

> data PT s a where
>     MkRef   :: a -> PT s (PTRef s a)
>     GetRef  :: PTRef s a -> PT s a
>     PutRef  :: a -> PTRef s a -> PT s ()
>     AndThen :: PT s a -> (a -> PT s b) -> PT s b

非常直接。 AndThen 允许我们将其用作Monad。您可能想知道return 是如何实现的。这是它的 monad 实例（它只遵守关于 runPF 的 monad 法则，稍后将定义）：

> instance Monad (PT s) where
>     (>>=)    = AndThen
>     return a = AndThen (MkRef a) GetRef --Sorry. I like minimalism.
> instance Functor (PT s) where
>     fmap = liftM
> instance Applicative (PT s) where
>     pure  = return
>     (<*>) = ap

现在我们可以将fib 定义为测试用例。

> fib :: Int -> PT s Integer
> fib n = do
>     rold <- MkRef 0
>     rnew <- MkRef 1
>     replicateM_ n $ do
>         old <- GetRef rold
>         new <- GetRef rnew
>         PutRef      new  rold
>         PutRef (old+new) rnew
>     GetRef rold

它会键入检查。欢呼！现在，我能够将其转换为 ST（我们现在明白为什么 s 必须是 * -> *）

> toST :: PT (STRef s) a -> ST s a
> toST (MkRef  a        ) = fmap Ref $ newSTRef a
> toST (GetRef   (Ref r)) = readSTRef r
> toST (PutRef a (Ref r)) = writeSTRef r a
> toST (pa `AndThen` apb) = (toST pa) >>= (toST . apb)

现在我们可以定义一个函数来运行PT，而不需要引用ST：

> runPF :: (forall s. PT s a) -> a
> runPF p = runST $ toST p

runPF $ fib 7 给出13，这是正确的。

---

我的问题是我们可以在没有引用的情况下使用 ST 定义 runPF 吗？

有没有一种纯粹的方式来定义runPF？ PTRef 的定义完全不重要；无论如何，它只是一个占位符类型。它可以被重新定义为使它工作的任何东西。

如果你不能纯粹定义runPF，请证明它不能。

性能不是问题（如果是，我不会让每个return 都有自己的参考）。

我认为存在类型可能有用。

注意：如果我们假设 a 是可动态的，这很简单。我正在寻找适用于所有a 的答案。

注意：事实上，答案甚至不一定与PT 有很大关系。它只需要像ST 一样强大而不使用魔法。 （从(forall s. PT s) 转换是一种测试答案是否有效。）

Answer 1

tl;dr：不调整PT 的定义是不可能的。这是核心问题：您将在某种存储介质的上下文中运行有状态计算，但所述存储介质必须知道如何存储 任意 类型。如果不将某种证据打包到 MkRef 构造函数中，这是不可能的 - 或者像其他人建议的那样存在包装的 Typeable 字典，或者证明该值属于已知的有限类型集之一。

作为第一次尝试，让我们尝试使用列表作为存储介质并使用整数来引用列表中的元素。

newtype Ix a = MkIx Int  -- the index of an element in a list

interp :: PT Ix a -> State [b] a
interp (MkRef x) = modify (++ [x]) >> gets (Ref . MkIx . length)
-- ...

在环境中存储新项目时，我们确保将其添加到列表的末尾，以便我们之前给出的 Refs 始终指向正确的元素。

这是不对的。我可以参考any 类型a，但interp 的类型表示存储介质是bs 的同构列表。当 GHC 拒绝此类型签名时，我们要求我们争取权利，抱怨它无法将 b 与 MkRef 中的事物类型匹配。

---

不要害怕，让我们尝试使用一个异构列表作为State monad的环境，我们将在其中解释PT。

infixr 4 :>
data Tuple as where
    E :: Tuple '[]
    (:>) :: a -> Tuple as -> Tuple (a ': as)

这是我个人最喜欢的 Haskell 数据类型之一。它是一个可扩展元组，由其中的事物类型列表索引。元组是异构链表，其中包含有关其中事物类型的类型级信息。 （通常在Kiselyov's paper 之后称为HList，但我更喜欢Tuple。）当您在元组的前面添加一些内容时，您将其类型添加到类型列表的前面。诗意的I once put it this way：“元组和它的类型一起成长，就像藤蔓爬上竹子一样。”

Tuples 的示例：

ghci> :t 'x' :> E
'x' :> E :: Tuple '[Char]
ghci> :t "hello" :> True :> E
"hello" :> True :> E :: Tuple '[[Char], Bool]

对元组中值的引用是什么样的？我们必须向 GHC 证明我们从元组中得到的东西的类型确实是我们期望的类型。

data Elem as a where  -- order of indices arranged for convenient partial application
    Here :: Elem (a ': as) a
    There :: Elem as a -> Elem (b ': as) a

Elem 的定义在结构上是自然数的定义（Elem 值，如 There (There Here) 看起来类似于自然数，如 S (S Z)）但有额外的类型 - 在这种情况下，证明类型 @987654347 @ 在类型级别列表 as 中。我提到这一点是因为它具有暗示性：Nats 是很好的列表索引，同样Elem 对于索引到元组很有用。在这方面，它可以替代我们引用类型中的Int。

(!) :: Tuple as -> Elem as a -> a
(x :> xs) ! Here = x
(x :> xs) ! (There ix) = xs ! ix

我们需要几个函数来处理元组和索引。

type family as :++: bs where
    '[] :++: bs = bs
    (a ': as) :++: bs = a ': (as :++: bs)

appendT :: a -> Tuple as -> (Tuple (as :++: '[a]), Elem (as :++: '[a]) a)
appendT x E = (x :> E, Here)
appendT x (y :> ys) = let (t, ix) = appendT x ys
                      in (y :> t, There ix)

让我们尝试在Tuple 环境中为PT 编写解释器。

interp :: PT (Elem as) a -> State (Tuple as) a
interp (MkRef x) = do
    t <- get
    let (newT, el) = appendT x t
    put newT
    return el
-- ...

没办法，克星。问题是当我们获得新的引用时，环境中Tuple的类型发生了变化。正如我之前提到的，向元组添加一些内容会将其类型添加到元组的类型中，State (Tuple as) a 类型掩盖了这一事实。 GHC 不会被这种企图的诡计所迷惑：Could not deduce (as ~ (as :++: '[a1]))。

---

据我所知，这就是车轮脱落的地方。您真正想要做的是在整个PT 计算中保持元组的大小不变。这将要求您通过可以获取引用的类型列表来索引PT 本身，证明每次这样做都允许（通过提供Elem 值）。然后环境看起来像一个列表元组，引用将包含一个Elem（用于选择正确的列表）和一个Int（用于查找列表中的特定项目）。

这个方案当然是违反规则的（你需要改变PT的定义），但它也有工程问题。当我打电话给MkRef 时，我有责任为我引用的值提供Elem，这非常乏味。 （也就是说，您通常可以说服 GHC 通过使用 hacky 类型类进行证明搜索来找到 Elem 值。）

另一件事：编写PTs 变得很困难。您计算的所有部分都必须由 same 类型列表索引。您可以尝试引入允许您扩展PT 环境的组合器或类，但您还必须在执行此操作时更新所有引用。使用 monad 会很困难。

一个可能更简洁的实现将允许PT 中的类型列表随着您在数据类型周围的移动而变化：每次遇到MkRef 时，类型都会变长。因为计算的类型会随着它的进行而改变，所以你不能使用常规的 monad - 你必须求助于IxMonad 。如果你想知道那个程序是什么样子的，请看我的other answer。

最终，症结在于元组的类型由PT 请求的值决定。环境是给定请求决定在其中存储的内容。 interp 不能选择元组中的内容，它必须来自 PT 上的索引。任何试图欺骗该要求的尝试都会崩溃和燃烧。现在，在一个真正的依赖类型系统中，我们可以检查给定的PT 值并找出as 应该是什么。唉，Haskell 不是一个依赖类型的系统。

Answer 2

一个简单的解决方案是包装一个State monad 并提供与ST 相同的API。在这种情况下，不需要存储运行时类型信息，因为它可以从STRef-s 的类型中确定，并且通常的ST s 量化技巧可以防止用户弄乱存储引用的容器。

我们将 ref-s 保存在 IntMap 中，并在每次分配新 ref 时增加一个计数器。读写只是修改了IntMap，并在上面撒了一些unsafeCoerce。

{-# LANGUAGE DeriveFunctor, GeneralizedNewtypeDeriving, RankNTypes, RoleAnnotations #-}

module PureST (ST, STRef, newSTRef, readSTRef, modifySTRef, runST) where

import Data.IntMap (IntMap, (!))
import qualified Data.IntMap as M

import Control.Monad
import Control.Applicative
import Control.Monad.Trans.State
import GHC.Prim (Any)
import Unsafe.Coerce (unsafeCoerce)

type role ST nominal representational
type role STRef nominal representational
newtype ST s a = ST (State (IntMap 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
  (m, i) <- get
  put (M.insert i (unsafeCoerce a) m, i + 1)
  pure (STRef i)

readSTRef :: STRef s a -> ST s a
readSTRef (STRef i) = ST $ do
  (m, _) <- get
  pure (unsafeCoerce (m ! i))

writeSTRef :: STRef s a -> a -> ST s ()
writeSTRef (STRef i) a = ST $ 
  modify $ \(m, i') -> (M.insert i (unsafeCoerce a) m, i')

modifySTRef :: STRef s a -> (a -> a) -> ST s ()
modifySTRef (STRef i) f = ST $
  modify $ \(m, i') -> (M.adjust (unsafeCoerce f) i m, i')                      

runST :: (forall s. ST s a) -> a
runST (ST s) = evalState s (M.empty, 0)

foo :: Num a => ST s (a, Bool)
foo = do
  a <- newSTRef 0 
  modifySTRef a (+100)
  b <- newSTRef False
  modifySTRef b not
  (,) <$> readSTRef a <*> readSTRef b

现在我们可以这样做了：

> runST foo
(100, True)

但以下失败并出现通常的ST 类型错误：

> runST (newSTRef True)

当然，上述方案从不垃圾收集引用，而是在每次runST 调用时释放所有内容。我认为一个更复杂的系统可以实现多个不同的区域，每个区域都由一个类型参数标记，并以更细粒度的方式分配/释放资源。

另外，使用unsafeCoerce 意味着在这里直接使用内部与直接使用GHC.ST 内部和State# 一样危险，所以我们应该确保提供一个安全的API，并测试我们的内部彻底（否则我们可能会在 Haskell 中遇到段错误，这是一个大罪）。

Answer 3

自从我发布了我的earlier answer 以来，您已经表示您不介意更改您对PT 的定义。我很高兴地报告：放宽限制会将您问题的答案从 no 更改为 yes！我已经说过你需要通过存储介质中的类型集来索引你的 monad，所以这里有一些工作代码展示了如何做到这一点。 （我最初将此作为对我之前答案的编辑，但它太长了，所以我们在这里。）

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE TypeOperators #-}

import Prelude

我们将需要一个比 Prelude 中的更智能的 Monad 类：indexed monad-like things 描述通过有向图的路径的类。出于显而易见的原因，我还将定义索引函子。

class FunctorIx f where
    imap :: (a -> b) -> f i j a -> f i j b

class FunctorIx m => MonadIx m where
    ireturn :: a -> m i i a
    (>>>=) :: m i j a -> (a -> m j k b) -> m i k b

(>>>) :: MonadIx m => m i j a -> m j k b -> m i k b
ma >>> mb = ma >>>= \_ -> mb

replicateM_ :: MonadIx m => Int -> m i i a -> m i i ()
replicateM_ 0 _ = ireturn ()
replicateM_ n m = m >>> replicateM_ (n - 1) m

索引 monad 使用类型系统来跟踪有状态计算的进度。 m i j a 是一个单子计算，它需要i 的输入状态，将状态更改为j，并生成a 类型的值。使用>>>= 对索引单子进行排序就像玩多米诺骨牌。您可以将状态从i 到j 的计算输入到从j 到k 的计算中，并从i 到k 获得更大的计算。 （Kleisli Arrows of Outrageous Fortune (and elsewhere) 中描述了这个索引 monad 的更丰富的版本，但这对于我们的目的来说已经足够了。）

MonadIx 的一种可能性是File monad，它跟踪文件句柄的状态，确保您不会忘记释放资源。 fOpen :: File Closed Open () 以一个关闭的文件开始并打开它，fRead :: File Open Open String 返回打开的文件的内容，fClose :: File Open Closed () 将文件从打开状态变为关闭状态。 run 操作采用 File Closed Closed a 类型的计算，确保您的文件句柄始终得到清理。

但我跑题了：这里我们关心的不是文件句柄，而是一组键入的“内存位置”；虚拟机内存库中事物的类型是我们将用于 monad 索引的内容。我喜欢得到我的“程序/解释器”monads for free，因为它表达了结果存在于计算的叶子中的事实，并促进了可组合性和代码重用，所以这是当我们插入它时将产生 PT 的函子进入下面的FreeIx：

data PTF ref as bs r where
    MkRef_ :: a -> (ref (a ': as) a -> r) -> PTF ref as (a ': as) r
    GetRef_ :: ref as a -> (a -> r) -> PTF ref as as r
    PutRef_ :: a -> ref as a -> r -> PTF ref as as r

instance FunctorIx (PTF ref) where
    imap f (MkRef_ x next) = MkRef_ x (f . next)
    imap f (GetRef_ ref next) = GetRef_ ref (f . next)
    imap f (PutRef_ x ref next) = PutRef_ x ref (f next)

PTF 由引用类型ref :: [*] -> * -> * 参数化 - 允许引用知道系统中有哪些类型 - 并由存储在解释器“内存”中的类型列表索引。有趣的案例是MkRef_：创建一个新的引用会将a 类型的值添加到内存中，将as 变为a ': as；延续在扩展环境中期望ref。其他操作不会改变系统中的类型列表。

当我按顺序创建引用 (x <- mkRef 1; y <- mkRef 2) 时，它们将具有不同的类型：第一个是 ref (a ': as) a，第二个是 ref (b ': a ': as) b。为了使类型对齐，我需要一种在比创建它的环境更大的环境中使用引用的方法。一般来说，这个操作取决于引用的类型，所以我会把它放在一个类中。

class Expand ref where
    expand :: ref as a -> ref (b ': as) a

这个类的一个可能的概括是用inflate :: ref as a -> ref (bs :++: as) a这样的类型来总结expand的重复应用模式。

这是另一个可重用的基础架构，我之前提到的 indexed free monad。 FreeIx 通过提供类型对齐的连接操作 Free 将索引函子转换为索引 monad，该操作在函子参数中绑定递归结，以及无操作操作 Pure。

data FreeIx f i j a where
    Pure :: a -> FreeIx f i i a
    Free :: f i j (FreeIx f j k a) -> FreeIx f i k a

lift :: FunctorIx f => f i j a -> FreeIx f i j a
lift f = Free (imap Pure f)

instance FunctorIx f => MonadIx (FreeIx f) where
    ireturn = Pure
    Pure x >>>= f = f x
    Free love {- , man -} >>>= f = Free $ imap (>>>= f) love

instance FunctorIx f => FunctorIx (FreeIx f) where
    imap f x = x >>>= (ireturn . f)

免费 monad 的一个缺点是您必须编写样板文件以使 Free 和 Pure 更易于使用。这里有一些单动作 PTs，它们构成了 monad API 的基础，还有一些 pattern synonyms 在我们解压 PT 值时隐藏了 Free 构造函数。

type PT ref = FreeIx (PTF ref)

mkRef :: a -> PT ref as (a ': as) (ref (a ': as) a)
mkRef x = lift $ MkRef_ x id

getRef :: ref as a -> PT ref as as a
getRef ref = lift $ GetRef_ ref id

putRef :: a -> ref as a -> PT ref as as ()
putRef x ref = lift $ PutRef_ x ref ()

pattern MkRef x next = Free (MkRef_ x next)
pattern GetRef ref next = Free (GetRef_ ref next)
pattern PutRef x ref next = Free (PutRef_ x ref next)

这就是我们编写PT 计算所需的一切。这是您的fib 示例。我正在使用 RebindableSyntax 并在本地重新定义 monad 运算符（为其索引等效项），因此我可以在索引 monad 上使用 do 表示法。

-- fib adds two Ints to an arbitrary environment
fib :: Expand ref => Int -> PT ref as (Int ': Int ': as) Int
fib n = do
    rold' <- mkRef 0
    rnew <- mkRef 1
    let rold = expand rold'
    replicateM_ n $ do
        old <- getRef rold
        new <- getRef rnew
        putRef new rold
        putRef (old+new) rnew
    getRef rold
        where (>>=) = (>>>=)
              (>>) = (>>>)
              return :: MonadIx m => a -> m i i a
              return = ireturn
              fail :: MonadIx m => String -> m i j a
              fail = error

这个版本的fib 看起来就像你想在原始问题中写的那个。唯一的区别（除了>>= 等的本地绑定）是对expand 的调用。每次新建引用都要expand所有旧引用，有点繁琐。

最后我们可以完成我们开始做的工作并构建一个PT-machine，它使用Tuple作为存储介质，Elem作为引用类型。

infixr 5 :>
data Tuple as where
    E :: Tuple '[]
    (:>) :: a -> Tuple as -> Tuple (a ': as)

data Elem as a where
    Here :: Elem (a ': as) a
    There :: Elem as a -> Elem (b ': as) a

(!) :: Tuple as -> Elem as a -> a
(x :> xs) ! Here = x
(x :> xs) ! There ix = xs ! ix

updateT :: Elem as a -> a -> Tuple as -> Tuple as
updateT Here x (y :> ys) = x :> ys
updateT (There ix) x (y :> ys) = y :> updateT ix x ys

要在比您构建它的元组更大的元组中使用Elem，您只需使其看起来更靠后。

instance Expand Elem where
    expand = There

请注意，Elem 的这种部署很像 de Bruijn 索引：最近绑定的变量具有较小的索引。

interp :: PT Elem as bs a -> Tuple as -> a
interp (MkRef x next) tup = let newTup = x :> tup
                            in interp (next $ Here) newTup
interp (GetRef ix next) tup = let x = tup ! ix
                              in interp (next x) tup
interp (PutRef x ix next) tup = let newTup = updateT ix x tup
                                in interp next newTup
interp (Pure x) tup = x

当解释器遇到MkRef 请求时，它会通过在前面添加x 来增加其内存大小。类型检查器会提醒您，MkRef 之前的任何 refs 必须是正确的 expanded，因此当元组更改大小时，现有引用不会失控。我们为没有不安全类型转换的解释器付费，但我们获得了引用完整性。

从静止开始运行要求PT 计算期望从一个空的内存库开始，但我们允许它以任何状态结束。

run :: (forall ref. Expand ref => PT ref '[] bs a) -> a
run x = interp x E

它会进行类型检查，但它有效吗？

ghci> run (fib 5)
5
ghci> run (fib 3)
2