可以纯粹执行`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是*->*,但现在不是真的很重要.对于我们所关心的一切,它可能是多面手的.

> 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实例(它仅尊重monad法则,runPF稍后定义):

> 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我们之前发出的s指向正确的元素.

这不对.我可以引用任何类型a,但是类型interp说存储介质是bs 的同类列表.当GHC拒绝这种类型的签名时,GHC让我们对权利抱怨,抱怨它b与内部的东西的类型不匹配MkRef.

没有被吓倒,让我们继续使用异构列表作为State我们将解释的monad 的环境PT.

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

这是我个人最喜欢的Haskell数据类型之一.它是一个可扩展的元组,由其中的事物类型列表索引.元组是异构链表,其中包含有关其中内容类型的类型级信息.(它通常被称为HList跟Kiselyov的论文,但我更喜欢Tuple.)当你在元组的前面添加一些东西时,你将它的类型添加到类型列表的前面.在一种诗意的情绪中,我曾经这样说过:"元组和它的类型一起生长,就像藤蔓爬上竹子一样."

例子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.我之所以提到这一点是因为它具有提示性: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)

让我们尝试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 Elem通过使用hacky类型的证明搜索来查找值.)

另一件事:构成PT变得困难.计算的所有部分都必须由相同的类型列表编制索引.您可以尝试引入组合器或类,它们允许您扩展a的环境PT,但是当您这样做时,您还必须更新所有引用.使用monad会非常困难.

一个可能更清晰的实现将允许a中的类型列表PT随着您在数据类型中的变化而变化:每次遇到MkRef类型时都会变长一个.因为计算的类型随着它的进展而改变,所以你不能使用常规的monad - 你必须求助于IxMonad .如果您想知道该程序的外观,请参阅我的其他答案.

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

Answer 2

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

IntMap每次分配新的ref时,我们都会将ref-s保持在一个并增加一个计数器.阅读和写作只是修改了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

自从我发布了我之前的回答以来,您已表明您不介意更改您的定义PT.我很高兴地报告:放宽这个限制会改变你的问题的答案从否到是!我已经争辩说你需要通过存储介质中的一组类型索引你的monad,所以这里有一些工作代码显示如何做到这一点.(我最初把它作为我之前答案的编辑,但它太长了,所以我们在这里.)

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

import Prelude

我们需要一个Monad比Prelude中的类更聪明的类:索引monad式的东西,描述通过有向图的路径.由于显而易见的原因,我还将定义索引函子.

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是一个monadic计算,它需要输入状态i,改变状态j,并产生类型的值a.对索引的monad进行排序>>>=就像玩多米诺骨牌一样.您可以养活一个计算这需要从国家i到j成从去计算j到k,并从获得更大的计算i来k.(这个索引monad的更丰富版本在Kleisli Arrows of Outrageous Fortune(以及其他地方)中有所描述,但这个版本足以满足我们的目的.)

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

但是我离题了:这里我们不关心文件句柄,而是关注一组键入的"内存位置"; 虚拟机内存库中的东西类型是我们将用于monad索引的内容.我喜欢免费获得我的"程序/解释器"monad ,因为它表示结果存在于计算的叶子中,并促进可组合性和代码重用,所以这里是将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)时,它们将具有不同的类型:第一个将是a ref (a ': as) a,第二个将是a ref (b ': a ': as) b.为了使类型排成一行,我需要一种方法来在比它创建的环境更大的环境中使用引用.通常,这个操作取决于引用的类型,所以我将它放在一个类中.

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

这个类的一个可能的概括将expand包括类似的类型的重复应用的模式inflate :: ref as a -> ref (bs :++: as) a.

这是另一个可重复使用的基础设施,我之前提到的索引免费monad.FreeIx通过提供类型对齐的连接操作将索引的仿函数转换为索引的monad Free,该操作将仿函数参数中的递归结与无操作操作联系起来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更易于使用.下面是一些PT构成monad API基础的单动作,以及一些模式同义词,用于Free在解包PT值时隐藏构造函数.

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运算符(对于它们的索引等价物),所以我可以do在我的索引monad上使用表示法.

-- 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使用a 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到前面来增加其内存的大小.类型检查器将提醒您必须正确编辑ref之前的任何s ,因此当元组更改大小时,现有引用不会出现问题.我们支付了一个没有不安全演员的翻译,但是我们得到了引用的参照完整性.MkRefexpand

从一开始运行需要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