Can a `ST`-like monad be executed purely (without the `ST` library)?

Question

This post is literate Haskell. Just put in a file like "pad.lhs" and ghci will be able to run it.

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

Okay, so I was able to figure how to represent the ST monad in pure code. First we start with our reference type. Its specific value is not really important. The most important thing is that PT s a should not be isomorphic to any other type forall s. (In particular, it should be isomorphic to neither () nor 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. 

The kind for s is *->*, but that is not really important right now. It could be polykind, for all we care.

> 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 

Pretty straight forward. AndThen allows us to use this as a Monad. You may be wondering how return is implemented. Here is its monad instance (it only respects monad laws with respect to runPF, to be defined later):

> 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 

Now we can define fib as a test case.

> 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 

And it type checks. Hurray! Now, I was able to convert this to ST (we now see why s had to be * -> *)

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

Now we can define a function to run PT without referencing ST at all:

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

runPF $ fib 7 gives 13, which is correct.

---

My question is can we define runPF without reference using ST at all?

Is there a pure way to define runPF? PTRef's definition is completely unimportant; it's only a placeholder type anyway. It can be redefined to whatever makes it work.

If you cannot define runPF purely, give a proof that it cannot.

Performance is not a concern (if it was, I would not have made every return have its own ref).

I'm thinking that existential types may be useful.

Note: It's trivial if we assume is a is dynamicable or something. I'm looking for an answer that works with all a.

Note: In fact, an answer does not even necessarily have much to do with PT. It just needs to be as powerful as ST without using magic. (Conversion from (forall s. PT s) is sort of a test of if an answer is valid or not.)

Answer 1

tl;dr: It's not possible without adjustments to the definition of PT. Here's the core problem: you'll be running your stateful computation in the context of some sort of storage medium, but said storage medium has to know how to store arbitrary types. This isn't possible without packaging up some sort of evidence into the MkRef constructor - either an existentially wrapped Typeable dictionary as others have suggested, or a proof that the value belongs to one of a known finite set of types.

For a first attempt, let's try using a list as the storage medium and integers to refer to elements of the list.

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) -- ... 

When storing a new item in the environment, we make sure to add it to the end of the list, so that Refs we've previously given out stay pointing at the correct element.

This ain't right. I can make a reference to any type a, but the type of interp says that the storage medium is a homogeneous list of bs. GHC has us bang to rights when it rejects this type signature, complaining that it can't match b with the type of the thing inside MkRef.

---

Undeterred, let us have a go at using a heterogeneous list as the environment for the State monad in which we'll interpret PT.

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

This is one of my personal favourite Haskell data types. It's an extensible tuple indexed by a list of the types of the things inside it. Tuples are heterogeneous linked lists with type-level information about the types of the things inside it. (It's often called HList following Kiselyov's paper but I prefer Tuple.) When you add something to the front of a tuple, you add its type to the front of the list of types. In a poetic mood, I once put it this way: "The tuple and its type grow together, like a vine creeping up a bamboo plant."

Examples of Tuples:

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

What do references to values inside tuples look like? We have to prove to GHC that the type of the thing we're getting out of the tuple is indeed the type we expect.

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 

The definition of Elem is structurally that of the natural numbers (Elem values like There (There Here) look similar to natural numbers like S (S Z)) but with extra types - in this case, proving that the type a is in the type-level list as. I mention this because it's suggestive: Nats make good list indices, and likewise Elem is useful for indexing into a tuple. In this respect it'll be useful as a replacement for the Int inside our reference type.

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

We need a couple of functions to work with tuples and indices.

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) 

Let's try and write an interpreter for a PT in a Tuple environment.

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 -- ... 

No can do, buster. The problem is that the type of the Tuple in the environment changes when we obtain a new reference. As I mentioned before, adding something to a tuple adds its type to the tuple's type, a fact belied by the type State (Tuple as) a. GHC's not fooled by this attempted subterfuge: Could not deduce (as ~ (as :++: '[a1])).

---

This is where the wheels come off, as far as I can tell. What you really want to do is keep the size of the tuple constant throughout a PT computation. This would require you to index PT itself by the list of types to which you can obtain references, proving every time you do so that you're allowed to (by giving an Elem value). The environment would then look like a tuple of lists, and a reference would consist an Elem (to select the right list) and an Int (to find the particular item in the list).

This plan breaks the rules, of course (you need to change the definition of PT), but it also has engineering problems. When I call MkRef, the onus is on me to give an Elem for the value I'm making a reference to, which is pretty tedious. (That said, you can usually convince GHC to find Elem values by proof search using a hacky type class.)

Another thing: composing PTs becomes difficult. All the parts of your computation have to be indexed by the same list of types. You could attempt to introduce combinators or classes which allow you to grow the environment of a PT, but you'd also have to update all the references when you do that. Using the monad would be quite difficult.

A possibly-cleaner implementation would allow the list of types in a PT to vary as you walk around the datatype: every time you encounter a MkRef the type gets one longer. Because the type of the computation changes as it progresses, you can't use a regular monad - you have to resort to IxMonad . If you want to know what that program looks like, see my other answer.

Ultimately, the sticking point is that the type of the tuple is determined by the value of the PT request. The environment is what a given request decides to store in it. interp doesn't get to choose what's in the tuple, it must come from an index on PT. Any attempt to cheat that requirement is going to crash and burn. Now, in a true dependently-typed system we could examine the PT value we were given and figure out what as should be. Alas, Haskell is not a dependently-typed system.