Vector creation safety

Pushing this idea to the limit has actually helped me understand it better, and I'm now fairly well convinced that all of these functions are safe. Consider

createTOf  :: (forall s1 s2.       (MVector s1 a -> ST s2 (Vector a))       -> t (MVector s1 a) -> ST s2 (u (Vector a)))  -> (forall s. ST s (t (MVector s a)))  -> u (Vector a)createTOf trav m = runST $ m >>= trav unsafeFreeze

It's certainly quite a mouthful of a type signature! Let's focus in closely on the safety property we care about: that no MVector is mutated after it is frozen. The first thing we do is run m to produce something of type t (MVector s a).

t is very mysterious right now. Is it a container? Is it some sort of action that produces vectors? We can't really say terribly much about what it is, but we can say some things about what trav unsafeFreeze cannot do with it. Let's start by breaking out the type signature of trav:

trav :: forall s1 s2.        (MVector s1 a -> ST s2 (Vector a))     -> t (MVector s1 a) -> ST s2 (u (Vector a)))

trav turns t (MVector s1 a) into ST s2 (u (Vector a)). If t has vectors in it, then those vectors live in state thread s1. The result, however, is an action in state thread s2. So trav cannot modify an MVectors it's given using the usual operations. It can only apply the function it takes (which will be unsafeFreeze), and use whatever machinery may ride in on t. What sort of machinery could ride in on t? Well, here's a silly example:

data T :: Type -> Type where  T :: [ST s (MVector s a)] -> t (MVector s a)

Could trav interleave these ST actions with the freezes? No! Those ST actions match the MVectors, but they don't match the state thread trav operates in. So trav can't do anything with them whatsoever.