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.