forall量化子とは？
runSTは，どのようにして型検査の段階で書き換え可能なデータ型の流出を防いでいるのでしょうか？
そのヒントはrunSTやSTRef，STArrayなどの型の定義にあります。ただ，正しい理解のためには，次期標準Haskell'で追加される予定のいくつかの拡張機能を理解しておく必要があります（参考リンク）。こうした拡張機能についてまず説明しましょう。
拡張機能の説明の起点は，runSTの型で使われているforallという識別子です。これは，数理論理学で使われる「全称量化子（universal quantifier）」である「∀」に相当します（参考リンク1，参考リンク2）。
と言ってもわけがわからない人がほとんどでしょう。第17回で，forAllという名前の関数を紹介したのを覚えているでしょうか。forallは文字通り「すべての（for all）」を意味します。「forall a. (a -> a)」と書けば「すべての型aの値を取って型aの値を返す関数」，「forall a b. (a -> b)」と書けば「すべての型aの値を取ってすべての型bの値を返す関数」になります。「.」は省略できませんが，内部の括弧を省いて「forall a. a -> a」「forall a b. a -> b」のように書くことができます。
forallを使用した型は，単に型変数を利用した多相型と何ら変わりありません。これまで多相型を持った関数を単に「a -> a」と書いてきましたが，実はこれは暗黙のforallによって「全称量化（universal quantification）」された「forall a. (a -> a)」を意味していたのです（参考リンク）。GHCiでは，-fglasgow-extsオプションを有効した状態で:typeコマンドを使うと，明示的に全称量化した型を返します。
Prelude> :t id id :: a -> a Prelude> :t (==) (==) :: (Eq a) => a -> a -> Bool Prelude> :t (>>=) (>>=) :: (Monad m) => m a -> (a -> m b) -> m b Prelude> :set -fglasgow-exts Prelude> :t id id :: forall a. a -> a Prelude> :t (==) (==) :: forall a. (Eq a) => a -> a -> Bool Prelude> :t (>>=) (>>=) :: forall (m :: * -> *) a b. (Monad m) => m a -> (a -> m b) -> m b
forallをあえて明示的に書く意義はどこにあるのでしょうか？
一般に，明示的な記述は制御を可能にします。forallを陽に書くことで，全称量化する範囲を操作できるのです。その結果，Haskellの型に付随する制約を緩和できます。runST関数のように逆に制約を与えることもできます。
forallを使って制約を緩和する例を見ましょう。
Haskellでプログラムを書いていて，静的型付けに起因する制限に悩まされた経験はないでしょうか？ 動的型付けを行うSchemeのような言語では動作するコードでも，Haskellの静的型付けによって実行できないといったことがあるはずです。forallの導入を起点とした様々な拡張は，そのようなコードをHaskellで実行するための道を開きます。
通常は，Haskellでは「applyTuple f = (f True, f "hidamari")」や「applyThenSum g = g [1..100] + g ['a'..'z']」といった関数定義はできません。なぜならHaskellにおける暗黙の量化は，あくまで型の一番外側にforallを置くことで行われるものであり，一番内側の型に対して行われるのではないからです（参考リンク）。applyTupleのfとapplyThenSumのgにおける多相性は，applyTupleやapplyThenSum自身に対して成り立たない場合には無視されます。結果として，これらの式が型エラーになるのです。
Prelude> let applyTuple f = (f True, f "hidamari")
<interactive>:1:28:
Couldn't match expected type `[Char]' against inferred type `Bool'
Expected type: [Char] -> t
Inferred type: Bool -> t1
In the expression: f "hidamari"
In the expression: (f True, f "hidamari")
Prelude> let applyThenSum g = g [1..100] + g ['a'..'z']
<interactive>:1:24:
No instance for (Num Char)
arising from the literal `1' at <interactive>:1:24
Possible fix: add an instance declaration for (Num Char)
In the expression: 1
In the first argument of `g', namely `[1 .. 100]'
In the first argument of `(+)', namely `g ([1 .. 100])'しかし，fやgとして使用できる多相型関数は存在するため，このような式を定義できないのは不便です。そこで，いくつかのHaskell処理系では，任意の場所での全称量化を許す「ランク2多相性（rank-2 polymorphism，2階多相性）」や「ランクN多相性（N階多相性）」といった拡張機能を提供しています（参考リンク）。
GHCでは，-X*オプションやLANGUAGE指示文を使ってRank2Types（またはRankNTypes）を指定することで，こうした拡張機能を使えます（参考リンク）。Hugsでは-98オプションを使用した非互換モードで処理系を起動させることで同様の機能を利用できます（参考リンク）。
$ ghci Rank2.hs GHCi, version 6.8.2: http://www.haskell.org/ghc/ :? for help Loading package base ... linking ... done. [1 of 1] Compiling Rank2 ( Rank2.hs, interpreted ) Ok, modules loaded: Rank2. *Rank2> applyTuple id (True,"hidamari") *Rank2> applyThenSum length 126
{-# LANGUAGE Rank2Types #-}
module Rank2 where
applyTuple :: (forall a. a -> a) -> (Bool, String)
applyTuple f = (f True, f "hidamari")
applyThenSum :: (forall a. [a] -> Int) -> Int
applyThenSum g = g [1..100] + g ['a'..'z']こうした拡張を使えば，idやlengthなどの多相型関数を取る関数としてapplyTupleやapplyThenSumを定義できます。
ランク2多相性やランクN多相性の「ランク」は，forall量化子が表れるまでの関数適用の矢印（arrow）の深さで決まります。idやlengthといった普通のHaskellの多相型はランク1です。
Prelude> :t id id :: forall a. a -> a Prelude> :t length length :: forall a. [a] -> Int
applyTupleやapplyThenSumは，forall量化子が一つ内側（関数矢印の左側）にくるのでランク2になります。
*Rank2> :t applyTuple applyTuple :: (forall a. a -> a) -> (Bool, String) *Rank2> :t applyThenSum applyThenSum :: (forall a. [a] -> Int) -> Int
同様に，「applyThenSumなどのランク2多相性を持つ型」を引数に取るような型は，forall量化子が二つ内側にくるのでランク3になります。
polyFunc :: (forall a. [a] -> Int) -> ((forall a. [a] -> Int) -> Int) -> Int polyFunc f g = g f + 1
こうした型は，ランク2多相性までしか対応していない処理系や拡張機能では扱えないので気を付けてください。
$ ghci Rank2.hs
GHCi, version 6.8.2: http://www.haskell.org/ghc/ :? for help
Loading package base ... linking ... done.
[1 of 1] Compiling Rank2 ( Rank2.hs, interpreted )
Rank2.hs:13:0:
Illegal polymorphic or qualified type: forall a. [a] -> Int
In the type signature for `polyFunc':
polyFunc :: (forall a. [a] -> Int)
-> ((forall a. [a] -> Int) -> Int) -> Int
Failed, modules loaded: none.
Prelude> ランク3以上の多相性を持つ型を使うにはランクN多相性が必要です。
{-# LANGUAGE RankNTypes #-}
module RankN where
applyThenSum :: (forall a. [a] -> Int) -> Int
applyThenSum g = g [1..100] + g ['a'..'z']
polyFunc :: (forall a. [a] -> Int) -> ((forall a. [a] -> Int) -> Int) -> Int
polyFunc f g = g f + 1*RankN> polyFunc length applyThenSum 127
ただし，実際には理論的な制約があります。
ここまでの説明では，型変数を具体化する際に与えられるのは，forall量化子を伴わない「単相型（monotype，monomorphic type）」に限られていました。しかし，forall量化子を導入すると，好きな場所にforallを置けるようになります。型変数を多相型（polytype）で具体化する可能性が出てくるのです。このような多相性を「非叙述的多相性（impredicative polymorphism，非可述的多相性）」と呼び，従来の多相性を「叙述的多相性（predicative polymorphism，可述的多相性）」と呼んで，両者を区別します。
多くの言語や処理系は，非叙述的多相性を認めていません。したがって，以下のような関数は定義できません。
maybeApply :: Maybe (forall a. [a] -> [a]) -> ([Int], [Char]) -> ([Int], [Char]) maybeApply (Just f) (nums, strs) = (f nums, f strs) maybeApply Nothing v = v
このような関数を定義するには，Maybe aの型変数aに(forall a. [a] -> [a])を与える必要があるからです。
なぜ，多くの言語や処理系が非叙述的多相性を採用しないのでしょうか？ その理由は，非叙述的多相性やランクN多相性を加えることにより，型推論が極めて難しくなってしまうことにあります。型が決定不能にならないように，「どのように推論すべきか」「推論のどこに制限を設けるべきか」といった点を明確にしなければなりません。しかし，このための理論は十分には確立されていません。
GHCはこうした研究のためのプラットフォームになっているため，6.6以降では非叙述的多相性を利用できます（参考リンク1，参考リンク2）。GHCでは今のところ（2008年5月20日現在），デフォルトで非叙述的多相性を利用できます。
*RankN> maybeApply (Just (take 6 . cycle)) ([2..3], "fine") ([2,3,2,3,2,3],"finefi") *RankN> maybeApply Nothing ([2..3], "fine") ([2,3],"fine")
仕様の細かい部分は，理論の発展とともに改良されていく見込みです（参考リンク）。もっとも，非叙述的多相性はHaskell'に採用されない可能性があります。非叙述的多相性を使うのであれば，今後の動向に注意してください。
