Let's say you want to write some stateful function in Haskell. You have to use a monadic style like this: (using whatever state monad)
f :: x -> k -> (ST s) r
So this means that essentially the function takes some input x and k, might use and/or modify the world to compute a return value r.
Assume x is a stateful structure, that might be modified by f. Assume k is just a simple key type used for example to access something in x. k itself will be assigned a simple number type later, but we don't want to have to decide now of its type.
So essentially I know that x is a mutable thing, and k is immutable.
The problem is just looking at f's signature, we cannot tell that, so if f occurs in the body of some more complex monadic code we can't reason very well about those variables.
Example:
g :: x -> k -> (ST s) r
g a i = do
...
f a i -- I don't know if i :: k depends on state
... --- I don't know if i was changed by f
What I mean is that if I was given a variable i of unknown type k, I don't know whether or not it depends on s and whether its value can be affected by a call of f.
This problem of course does not exist when writing pure functions, since everything is immutable.
Is there a way to conveniently annotate and, more importantly, statically enforce that k will remain unchanged in the ST monad when calling f?
Inside ST, you can definitely tell what is mutable: an Int is always an immutable integer, while a STRef s Int is an (immutable) reference to a mutable Int.
Hence,
f :: STRef s Int -> String -> (ST s) Bool
can (read and) modify the Int pointed to the first argument, but can only read the immutable string passed as second argument.
On top of that, f might create (and mutate) new STRef s references to newly allocated values. It can also modify other valued if f was defined using a reference to such values. E.g. in
bar :: forall s . ST s ()
bar = do
x_ref <- newSTRef "hello"
let f :: STRef s String -> String -> ST s ()
f y_ref str = do
y <- readSTRef y_ref
writeSTRef x_ref y
writeSTRef y_ref (y ++ " change " ++ str)
...
calling f will alter both the string which was originally set to "hello" and the string whose reference is passed to f.
In your own example:
g :: x -> k -> (ST s) r
g a i = do
...
f a i -- I don't know if i :: k depends on state
... --- I don't know if i was changed by f
If i :: k was not a reference, it still has the same value. If it was a reference, the referred value might have been changed by f a i.