自从我发布了我之前的答案以来，您已经表示您不介意更改PT. 我很高兴地报告：放宽限制会将您问题的答案从“否”变为“是”！我已经说过你需要通过存储介质中的类型集来索引你的 monad，所以这里有一些工作代码展示了如何做到这一点。（我最初将此作为对我之前答案的编辑，但它太长了，所以我们在这里。）
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE TypeOperators #-}
import Prelude
我们将需要一个Monad比 Prelude 中的更智能的类：通过有向图描述路径的索引单子类事物。出于显而易见的原因，我还将定义索引函子。
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。对索引单子进行排序>>>=就像玩多米诺骨牌一样。您可以将一个将状态 from的计算输入到一个从 to 的计算中，并从ito获得更大的计算。（在Kleisli Arrows of Outrageous Fortune（和其他地方）中描述了这个索引 monad 的更丰富的版本，但这对于我们的目的来说已经足够了。）jjkik
一种可能性MonadIx是File跟踪文件句柄状态的 monad，确保您不会忘记释放资源。fOpen :: File Closed Open ()从一个关闭的文件开始并打开它，fRead :: File Open Open String返回打开的文件的内容，并将fClose :: File Open Closed ()文件从打开状态变为关闭状态。该run操作需要计算 type 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通过提供一个类型对齐的连接操作，将一个索引函子变成一个索引单子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易于使用。下面是一些构成 monad API 基础的单动作PT，以及一些模式同义词，用于在我们解包值时隐藏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使用 aTuple作为存储介质和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任何s ，因此当元组更改大小时，现有引用不会失控。我们为没有不安全类型转换的解释器付费，但我们获得了引用完整性。refMkRefexpand
从一个固定的开始运行需要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