Since I posted my earlier answer, you've indicated that you don't mind making changes to your definition of PT. I am happy to report: relaxing that restriction changes the answer to your question from no to yes! I've already argued that you need to index your monad by the set of types in your storage medium, so here's some working code showing how to do that. (I originally had this as an edit to my previous answer but it got too long, so here we are.)
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE TypeOperators #-}
import Prelude
We're going to need a smarter Monad class than the one in the Prelude: that of indexed monad-like things describing paths through a directed graph. For reasons that should become apparent, I'm going to define indexed functors as well.
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
An indexed monad uses the type system to track the progress of a stateful computation. m i j a is a monadic computation which requires an input state of i, changes the state to j, and produces a value of type a. Sequencing indexed monads with >>>= is like playing dominoes. You can feed a computation which takes the state from i to j into a computation which goes from j to k, and get a bigger computation from i to k. (There's a richer version of this indexed monad described in Kleisli Arrows of Outrageous Fortune (and elsewhere) but this one is quite enough for our purposes.)
One possibility with MonadIx is a File monad which tracks the state of a file handle, ensuring you don't forget to free resources. fOpen :: File Closed Open () starts with a closed file and opens it, fRead :: File Open Open String returns the contents of an opened file, and fClose :: File Open Closed () takes a file from open to closed. The run operation takes a computation of type File Closed Closed a, which ensures that your file handles always get cleaned up.
But I digress: here we are concerned not with a file handle but with a set of typed "memory locations"; the types of the things in the virtual machine's memory bank are what we'll use for the monad's indices. I like to get my "program/interpreter" monads for free because it expresses the fact that results live at the leaves of a computation, and promotes composability and code reuse, so here's the functor which will produce PT when we plug it into FreeIx below:
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 is parameterised by the type of reference ref :: [*] -> * -> * - references are allowed to know which types are in the system - and indexed by the list of types being stored in the interpreter's "memory". The interesting case is MkRef_: making a new reference adds a value of type a to the memory, taking as to a ': as; the continuation expects a ref in the extended environment. The other operations don't change the list of types in the system.
When I create references sequentially (x <- mkRef 1; y <- mkRef 2), they'll have different types: the first will be a ref (a ': as) a and the second will be a ref (b ': a ': as) b. To make the types line up, I need a way to use a reference in a bigger environment than the one it was created in. In general, this operation depends on the type of reference, so I'll put it in a class.
class Expand ref where
expand :: ref as a -> ref (b ': as) a
One possible generalisation of this class would wrap up the pattern of repeated applications of expand, with a type like inflate :: ref as a -> ref (bs :++: as) a.
Here's another reusable bit of infrastructure, the indexed free monad I mentioned earlier. FreeIx turns an indexed functor into an indexed monad by providing a type-aligned joining operation Free, which ties the recursive knot in the functor's parameter, and a do-nothing operation 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)
One disadvantage of free monads is the boilerplate you have to write to make Free and Pure easier to work with. Here are some single-action PTs which form the basis of the monad's API, and some pattern synonyms to hide the Free constructors when we unpack PT values.
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)
That's everything we need to be able to write PT computations. Here's your fib example. I'm using RebindableSyntax and locally redefining the monad operators (to their indexed equivalents) so I can use do notation on my indexed 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
This version of fib looks just like the one you wanted to write in the original question. The only difference (apart from the local bindings of >>= and so on) is the call to expand. Every time you create a new reference, you have to expand all the old ones, which is a bit tedious.
Finally we can finish the job we set out to do and build a PT-machine which uses a Tuple as the storage medium and Elem as the reference type.
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
To use an Elem in a larger tuple than the one you built it for, you just need to make it look further down the list.
instance Expand Elem where
expand = There
Note that this deployment of Elem is rather like a de Bruijn index: more-recently-bound variables have smaller indices.
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
When the interpreter encounters a MkRef request, it increases the size of its memory by adding x to the front. The type checker will remind you that any refs from before the MkRef must be correctly expanded, so existing references don't get out of whack when the tuple changes size. We paid for an interpreter without unsafe casts, but we got referential integrity to boot.
Running from a standing start requires that the PT computation expects to begin with an empty memory bank, but we allow it to end in any state.
run :: (forall ref. Expand ref => PT ref '[] bs a) -> a
run x = interp x E
It typechecks, but does it work?
ghci> run (fib 5)
5
ghci> run (fib 3)
2
s ~ Const IntinrunPFand keep aMapwithIntkeys andavalues. – David Young Nov 28 '15 at 19:28Typeable ain eachPT s a? If so, it's a matter of adapting IOSpec, I guess. – chi Nov 28 '15 at 19:30Typeable, aMap Int Dynamicshould suffice to represent theSTRefs backstore. Reads/writes will need to be implemented through partial (but pure) functions, in that case. – chi Nov 28 '15 at 19:34