haskell - 是否可以纯粹执行 `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，这是正确的。

我的问题是我们可以完全不用 runPF来定义 ST吗？

是否有定义 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)
-- ...

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

这是不对的。我可以引用任何类型的 a，但是 interp的类型表示存储介质是 b的同类列表。当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:“元组及其类型一起生长，就像藤蔓爬上竹树一样。”
Tuple的示例:

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)这样的自然数)，但是具有额外的类型-在这种情况下，证明类型 a在类型级别列表 as中。我之所以提及它，是因为它具有启发性: Nat可以作为良好的列表索引，同样 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)

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

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值。)

另一件事:组成 PT变得很困难。计算的所有部分都必须由相同的类型列表索引。您可以尝试引入组合器或类，以使您可以扩展 PT的环境，但是在这样做时，您还必须更新所有引用。使用monad将非常困难。

可能更干净的实现将使 PT中的类型列表随数据类型的变化而变化:每次遇到 MkRef时，类型都会更长。由于计算的类型会随着计算的进行而变化，因此您不能使用常规的monad-必须使用 IxMonad 。如果您想知道该程序的外观，请参阅我的 other answer。

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