Using Universally Quantified Type Arguments to express stateful types

Learn
1

I was inspired by the ST Monad, which is indexed by a type variable to disallow using ST data structure in unsafe ways.

I tried to create a MappingSnapshot which captures a mapping and has a type variable, it also has a smart constructor.

newtype MappingSnapshot state container key value = MappingSnapshot { get :: container key value }

mkMappingSnapshot :: container key value -> forall s. MappingSnapshot s container key value
mkMappingSnapshot = MappingSnapshot

also there is type-indexed newtype ValidKey which should represent a key that was valid for a snapshot indexed with the same type variable, it also has a smart constructor.

newtype ValidKey s k = ValidKey 
  { get :: k
  }

mkValidKey :: Mapping c k v => MappingSnapshot s c k v -> k -> Maybe (ValidKey s k)
mkValidKey container key = fmap (const $ ValidKey key) $ Mapping.lookup container key

The Mapping class looks like this with a trivially defined instance for Data.Map

class Mapping container key value where
  lookup :: container key value -> key -> Maybe value
  unsafeLookup :: container key value -> key -> value

since ValidKeys are valid into the mapping they index into, I defined this function

safeLookup :: Mapping container key value => MappingSnapshot s container key value -> ValidKey s key -> value
safeLookup m k = unsafeLookup m (get k)

but I was able to cheat through the type indexing with this script:

mapping :: MappingSnapshot s Map Int Int
mapping = mkMappingSnapshot $ Map.singleton 1 1

key :: ValidKey s Int
key = let Just k = mkValidKey mapping 1
  in k

cheat :: ValidKey s Int -> MappingSnapshot s Map Int Int
cheat _ = mkMappingSnapshot $ Map.empty

bad :: Int
bad = let k = key in safeLookup (cheat k) k

-- >>> bad
-- *** Exception: Mapping.unsafeLookup: given key is not an element in the set

How can I design the type variable quantification to disallow this unsafe usage?

3

Maybe you want this?

4

I deleted my solution, since I misunderstood your mkValidKey.

Another quick attempt is that: learn from how ST monad works, and have an abstract ā€œsā€ that you cannot fake, but you will have to wrap everything under a runXYZ.

1 Like
5

Thank you for your answers, unfortunately I cannot accept both your answers as a solution.

I now understand that it is impossible to do this without a library-supplied s-type, like Data.Map.Justified and Control.Monad.ST do it using their withXYZ or runST types.