Using Haskell Rank 2 types to contain values

or "How to implement the semantics of the ST monad"

ST lets you create a type of mutable variable, an STRef. This STRef is only valid in the context that it was created. Rank2Types (or RankNTypes) is used to ensure that you can't get an STRef out and access it elsewhere, thus making the function semantically pure and free of side effects

What happens in the ST monad, stays in the ST monad.

How can one write such functions or monads?

Here is an example of using rank 2 types to prevent a type Cat from escaping its context Bag:

{-# LANGUAGE Rank2Types #-}
import Control.Monad

-- Type trickery to keep the cat in the bag
data Bag s a = Bag a -- like ST
data Cat s a = Cat a -- like STRef

instance Monad (Bag s) where
    (>>=) = bindBag
    return = returnBag

runBag :: forall a. (forall s. Bag s a) -> a
runBag k = case k of Bag a -> a

newCat :: a -> (forall s. Bag s (Cat s a))
newCat x = Bag (Cat x)

readCat :: forall s. forall a. (Cat s a -> Bag s a)
readCat x = case x of (Cat v) -> Bag v

bindBag :: Bag s a -> (a -> Bag s b) -> Bag s b
bindBag s f = case s of Bag x -> f x

returnBag :: a -> forall s. Bag s a
returnBag x = Bag x

-- Works, cat stays in the bag
test = runBag $ do
    cat <- newCat "meow"
    value <- readCat cat
    return value

-- --Doesn't compile - attempts to let the cat out
-- fail = runBag $ do
--     cat <- newCat "meow"
--     return cat

VidarHolen.net