没想到还能这样玩…真是有一套啊

ST Ref 提供了和 IO Ref 类似的操作：

data ST s a
data STRef s a
newSTRef :: a -> ST s (STRef s a)
readSTRef :: STRef s a -> ST s a
writeSTRef :: STRef s a -> a -> ST s ()

runST :: (forall s. ST s a) -> a

看起来和 IO Ref 的一套几乎一模一样，除了 ST Ref 多了一个类型参数 s ，而且 ST Monad 有一个很劲爆的函数 runST ，通过它的类型签名，我们可以发现，它可以让我们从 ST Monad 回来！而 IO Monad 是不能这样做的，除非使用 unsafePerformIO :: IO a -> a。那么，ST Ref 为什么可以这样做呢？这样做会不会破坏 Haskell 的纯洁性呢？以及，runST 里的 forall 是什么意思呢？

RankNTypes

考虑一个普普通通的多态函数

head :: [a] -> a

当我们使用 head [1..] 的时候，我们可以认为，它的类型签名中的 a 被统一替换成了 Integer ，这就很像 $\lambda\textrm{-Calculus}$ 里的 $\alpha\textrm{-deduction}$。

这样做在大部分情况下都是没有太大问题的。但是假如我们脑洞大开，写出了这样一个函数，把列表操作 [a] -> a lift 到元组上：

liftF f (xs, ys) = (f xs, f ys)

我们可以试探性地先写一个它的类型签名出来：

liftF :: ([a] -> a) -> ([b], [c]) -> (b, c)

但是这样好像不太对劲！根据我们之前总结出来的「替换」规则，这样写 a 是没法被替换的。那写成这样呢？

liftF :: ([b] -> b) -> ([b], [c]) -> (b, c)

这就更不对劲了，这样一来，f ys 的类型就对不上了。

forall

首先我们打开语言拓展 RankNTypes

{-# LANGUAGE RankNTypes #-}

我们通常写的多态函数，实际上都是以下形式的简写：

head :: forall a   .  [a]             ->  a
map  :: forall a b .  (a -> b) -> [a] -> [b]
id   :: forall a   .   a              ->  a

我们可以注意到，格式大概是 forall <TypeNames> . <Signature> ，这样写相当于「$\lambda~a.([a]\to a)$ 」。为了解释方便，我们来写一点 Idris。

head :: Type -> List Type -> Type
head _ (x::xs) = x

在 Idris 里，类型也是一等公民，我们可以这样调用 head

head Nat 1::2::3

这里我们传入了一个类型名。得到类型名之后，编译器会把 Type 代入类型签名剩下的部分。

事实上这完全多此一举，我们完全可以按照 Haskell 的那一套思路来写。但是这部分工作总是要有人做的，实际上 forall 就起到了这样的作用，编译器会自动推断我们调用函数所用到的参数的值的类型，然后把类型名给替换掉。而 Haskell 为我们隐藏了起来这部分内容，即 Rank 1 Type 不必书写 forall 。

我们以此把之前的函数签名改写一下：

liftF :: (forall a . ([a] -> a)) -> ([b], [c]) -> (b, c)

这样一来，编译器会先把 b 代入 [a] -> a 里，得到 [b] -> b ，再把 c 代入 [a] -> a 里，得到 [c] -> c ，然后满意地点点头。

ST Monad

ST Monad 里的 s 和 forall 究竟是干什么的呢？我们不妨先把 forall 去掉，看看会发生什么：

newSTRef :: a -> ST s (STRef s a)
runST :: ST s a -> a

runST $ newSTRef (1::Int)

这可真是要命，newSTRef 会得到一个 ST s (STRef s Int)，再执行一下 runST ，我们惊奇地发现，函数内部的状态已经泄露到外面去了，这可不太行啊，得治治这些动不动上房揭瓦的 Programmer。

那么接下来就是感受前人智慧的时间，实际上类型 s 什么都没有做，它是一个 Phantom Type，它唯一用途，就是防止用户上房揭瓦，把函数内部的状态泄露到外面去。

runST :: (forall s. ST s a) -> a

加上 forall 限定后，事情发生了一些变化，注意到前文我们对 forall 和 $\lambda\textrm{-Calculus}$ 的相似性的讨论，我们不难发现，惨遭 forall 的类型名是只能在 forall 的括号内部使用的，这就很像 $\lambda~x.x+1$ ，我们不能在这个函数的外面使用这个函数里面的 $x$ 一样。这样来说，类型 s 就只能在这个括号的内部发挥余热了。如果某个人试图 runST $ newSTRef (1::Int)，从而把状态给泄露出去，他能不能成功呢？我们来看一下类型：

newSTRef 会得到一个 ST s (STRef s Int)，但是当他试图 runST 的时候会发现，函数签名会变成这样：runST :: (forall s. ST s (STRef s Int)) -> STRef s Int ，类型 s 被泄露到了括号外面！这就会编译错误，从而从根本上杜绝了上房揭瓦的可能性。

有了 ST Monad，我们就可以愉快地写一些看似很纯，实际上有内部状态的东西了。