STモナドはなぜ変更可能な参照を外へ持ち出せないのか調べてみた

Haskell

この投稿は、Haskell Advent Calendar 2019 の4日目の記事です。STモナドの仕組みについて書きました。初中級者向けの内容となっています。

はじめに

STモナドは、変更可能な参照と破壊的代入操作を扱いつつも、そういった不純な状態を外へ持ち出せないことが型で保証されているモナドです。

最近この「型で状態を外へ持ち出せない仕組み」について調べていて、なるほどなと思ったので、今回はそのあたりのことを書きたいと思います。

流れとしては、最初にSTモナドの概要や使い方を紹介します。次にSTモナドを支える量化やランクN多相に触れ、それらがどのようにSTモナドの安全性を支えているのかを解説していきたいと思います。

なお、内容に誤りがありましたら優しくご指摘いただけると嬉しいです。

STモナドとは

STモナド (strict state-transformer monad) は、状態を扱うモナドです。ここで言う状態とは、命令型言語のように変更可能な参照を意味しています。この変更可能な参照に対して破壊的代入を繰り返しながら計算結果を求めていくのが、STモナドの特徴です。

ところで、同じ状態を扱うモナドにStateモナドがあります。比較すると、Stateモナドは更新の度に都度新しい状態を作成するのに対して、STモナドは状態の使い回しができるので、処理効率的にはSTモナドの方が有利です。例えば巨大なデータ構造を状態として扱う場合は、この差が開くんじゃないでしょうか。

このように効率的だけど不純な汚れ仕事を扱うSTモナドですが、汚れているのはモナドアクションの中だけです。モナドアクションから最終的に出力される計算結果は、ちゃんと純粋な値として取り出すことができます。

STモナドの面白いところは、この不純な状態を外へ持ち出すことができない、ということが型で保証されている点です。無理に持ち出そうとしても型検査で怒られます。

変更可能な参照が外へ漏れ出ることがなければ、他の場所で意図せず変更されてしまう心配はなくなりますよね。

STモナドの型

それではまず、STモナドの型を確認しておきましょう。

ST s a

右から、型変数 a は値を表し、型変数 s はスレッド（state thread）を表します。

このスレッドを表す s は、STモナドの中だけで生存するPhantom Typeです。Phantom Typeということは、実行時には存在しないけれど型検査時には存在する型、ということになりますが、捉え方としては、「STモナドを駆動するために内部的に専用スレッドが作られる。でもそれは実行時ではなく型検査時に」みたいな捉え方で良いと思います。

余談ですが、Thinking with Types という書籍では、STモナドを、

本質的には、phantom s parameterを持った単なるIdentity Monadだよ

と解説しています。

-- ST Monad
ST s a

-- Identity Monad
Identity a

STモナドの使用例

次に、STモナドを使用した簡単な例を見てみましょう。

import Control.Monad
import Control.Monad.ST
import Data.STRef

sum' :: [Int] -> Int
sum' xs = runST $ do
  ref <- newSTRef 0
  forM_ xs $ \i -> do
    modifySTRef ref (+ i)
  readSTRef ref

main :: IO ()
main = print $ sum' [1..10]
-- 結果: 55

sum' は、Int のリストを受け取り、集計した結果を Int として返す関数です。内部では、STモナドを使用して破壊的代入を繰り返しながら計算結果を求めています。STモナドを使用している範囲が関数 sum' の中に限定されていることに注目してください。

では、関数 sum' をもう少し詳しく見てみましょう。

まず、do構文の中で最初に登場する newSTRef は、初期値を与えると変更可能な参照 STRef を持つSTモナドを作成します。つまり、ref <- newSTRef 0 は、初期値 0 を与えてSTモナドを作成し、そこから STRef を取り出して ref に束縛していることになります。以降この ref は状態を扱う参照型として使用します。

次に forM_ xs $ \i -> do で、引数 xs の各要素を先頭から順番に i へ束縛し、 modifySTRef ref (+ i) で、参照型 ref に対して (+ i) の計算結果を破壊的に代入しています。

modifySTRef による破壊的代入を終えると、 readSTRef ref で、参照型 ref から値を読み取り、最後にdo構文の外で runST によって純粋な値を取り出しています。

このように、STモナドの参照型に対する破壊的代入という汚れ仕事は、モナドアクションの中で完全に閉じ込められていて、最後に計算した結果だけを取り出せることが分かりました。

STモナドで使用されるデータ型と各種関数

ここで、先ほどのSTモナドの使用例で登場したデータ型、それと各種関数のシグネチャを確認しておきましょう。

Data.STRef

Data.STRef は、STモナドで変更可能な参照として扱われ、破壊的代入や値の読み込みの際に必要となるデータ型です。

STRef s a

なお、型変数 s とa は、先ほど紹介したST s a の型変数と同じ役割になります。

newSTRef

初期値を与えて、初期状態の参照型 STRef s a を持つSTモナドを作成する関数です。

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

型変数 a は、与える引数によって型が決まり、参照型 STRef の値として設定されます。また、型変数 s は、この時点で型を決定するものが何も無いので、多相型のままスレッドとして設定されます。

ただ、この結果型 ST s (STRef s a) はちょっと変ですね。ST にも STRef にもスレッドを表す型変数 s がいます。

気持ち悪さは残りますが、これについては後ほど解説します。

modifySTRef

参照型 STRef s a に対して関数 a -> a で値の更新をします。

modifySTRef :: STRef s a -> (a -> a) -> ST s ()

readSTRef

参照型 STRef s a の値と状態を読み取ります。

readSTRef :: STRef s a -> ST s a

runST

関数 readSTRef で読み取った内容から値だけを取り出します。なお、ST s a が (forall s. ST s a) となっている理由は後述します。

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

変更可能な参照を外へ持ち出そうとすると

では、関数 newSTRef で変更可能な参照 ST s (STRef s a) を生成し、関数 runST で ST s a の a に設定されている参照型 (STRef s a) を持ち出そうとしたらどうなるでしょうか。

runST $ newSTRef 100

これは型検査に失敗し、以下のようなエラーメッセージが出力されます。

<interactive>:18:9: error:
• Couldn't match type ‘a’ with ‘STRef s Integer’
    because type variable ‘s’ would escape its scope
  This (rigid, skolem) type variable is bound by
    a type expected by the context:
      forall s. ST s a
    at <interactive>:18:9-18
  Expected type: ST s a
    Actual type: ST s (STRef s Integer)
• In the second argument of ‘($)’, namely ‘newSTRef 100’
  In the expression: runST $ newSTRef 100
  In an equation for ‘it’: it = runST $ newSTRef 100
• Relevant bindings include it :: a (bound at <interactive>:18:1)

なるほど、変更可能な参照 (STRef s a) をモナドの外へ持ち出すことはできませんね。

ちなみに先ほどのエラーメッセージでは、 Couldn't match type ‘a’ with ‘STRef s Integer’ because type variable ‘s’ would escape its scope と、スレッドを表す s をスコープの外に出そうとしているから型が合わないんだよと言っています。スコープって何でしょうか？

エラーメッセージから考察する

先ほどのエラーメッセージから forall s. ST s a、つまり関数 runST のシグネチャが鍵を握っていそうです。

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

runST :: ST s a -> a じゃなくて runST :: (forall s. ST s a) -> a となっているのは、なぜなのでしょうか。

ここで、forall s . を外したらどうなるか実験してみましょう。以下のコードは、Thinking with Types で紹介されていたコードを実験用に改変してみました。（コード全体は こちら になります）

runST' :: ST s a -> a  -- `forall s .` を削除
runST' = unsafeRunST

foo :: STRef s Integer
foo = runST' $ newSTRef 100

こうすると型検査で怒られることなく変更可能な参照 STRef s Integer を外へ持ち出せてしまいました！

やはり、関数 runST のシグネチャがSTモナドの安全性を支えるために重要なことが分かりました。

では、この forall って何でしょうか。

forallの探求

量化子は型に量的な意味を持たせる

forall の役割を知るために、まずは以下の関数を見てください。

id :: a -> a
id x = x

関数 id は、型変数 a を受け取りそのまま返す関数です。恒等関数というやつですね。引数は多相型なのでどのような型でも受け取ることができます。

この「どのような型でも」を言語拡張の ExplicitForAll を使用して明示的に書くとこのようになります。

{-# LANGUAGE ExplicitForAll #-}

id :: forall a. a -> a
id x = x

ここで forall が登場しましたね。

この forall は、全称量化子（universal quantifier、記号は∀）と呼ばれるもので、修飾した型変数に対して文字通り「すべての（for all）」という量的な意味を持たせることができます。つまり、forall a. a は、型変数 a に「すべての型に対応する」という意味を持たせています。*1

このように、全称量化子で型変数を量化する（量的な意味を持たせる）ことを、全称量化（Universal Quantification）と呼びます。*2

そして、通常は特に明示しなくても暗黙的に forall が付与されるので、以下はそれぞれ同じ意味になります。

{-# LANGUAGE ExplicitForAll #-}

{--
それぞれ上から順番に
- forallを省略
- forallを明示
- forallが修飾する範囲を分かりやすくするため括弧を記述
--}

id :: a -> a
id :: forall a. a -> a
id :: forall a. (a -> a)

reverse :: [a] -> [a]
reverse :: forall a. [a] -> [a]
reverse :: forall a. ([a] -> [a])

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

上記のコードで分かることは、暗黙的に付与される forall は、関数の最も外側に置かれ、関数全体を修飾するということです。括弧の中など、関数の内側には置かれません。

さて、全称量化について説明しましたが、結局のところforall を省略してもしなくても同じ意味になるので、forall の役割がまだ漠然としています。

それでは、forall の役割を更に探るため、次はランクN多相へと進みましょう。

量化子を関数の内側で定義する

言語拡張の RankNTypes（ランクN多相）を使用すると、全称量化子 forall を関数の内側で明示的に定義することができます。これにより、修飾した型変数のスコープを限定的にするとともに、型推論の制限を緩和させることができます。ランクN多相の詳細は後述するとして、これが何を意味するのか順を追って説明します。

以下の関数 applyTrue は、引数で受け取った関数 a -> a に True を設定し、その結果を Bool として返す関数です。

{-# LANGUAGE ExplicitForAll #-}

applyTrue :: forall a. (a -> a) -> Bool
applyTrue f = f True

これは型検査で失敗してしまいます。

• Couldn't match expected type ‘a’ with actual type ‘Bool’
  ‘a’ is a rigid type variable bound by
    the type signature for:
      applyTrue :: forall a. (a -> a) -> Bool
    at...

なぜなら、applyTrue と関数 a -> a との間で、下記の通り期待する型と実際の型が一致していないからです。（より詳しい解説は後ほど）

  • 関数 a -> a は引数に a を期待してるのに Bool を渡している
  • applyTrue の結果型は Bool を期待しているのに関数 a -> a は a を返している

このような場合は、言語拡張の RankNTypes を使用して、全称量化子 forall を関数の内側で明示することで、型推論の制限を緩和させます。

{-# LANGUAGE RankNTypes #-}

-- forallを括弧の中に入れる
applyTrue :: (forall a. a -> a) -> Bool
applyTrue f = f True

これは型検査に成功します。

forall a. (a -> a) を (forall a. a -> a) としただけですが、applyTrue と関数 forall a. a -> a との間で、期待する型と実際の型が一致したようです。

なぜこのようなことが実現できるのか、ランクN多相についてもっと調べてみる必要がありますね。

ランクN多相の概要と特徴

ランクN多相の概要

ランクN多相（Higher-rank polymorphism）*3 の「ランク」とは、関数の多相性の深さ（forall が修飾する関数の矢印 -> の深さ）を表しており、どのくらい深いかでランクのNが決まります。

具体例を見てみましょう。以下は、下に行くほど上位のランクになります。（ランクが高くなると関数の多相性は深くなります）

t                               -- ランク0単相
forall a. a -> t                -- ランク1多相
(forall a. a -> t) -> t         -- ランク2多相
((forall a. a -> t) -> t) -> t  -- ランク3多相

これでいくと、先ほどの applyTrue はこうなりますね。*4

  • applyTrue :: forall a. (a -> a) -> Bool はランク1多相
  • applyTrue :: (forall a. a -> a) -> Bool はランク2多相

では、ランクが高くなるとどのようなことが起こるのでしょうか。以下は、ランクN多相がもたらす2つの特徴をまとめてみました。

  1. 上位のランクの型は、下位のランクから決定することができないので、型の決定を先送りにできる（型推論の制限を緩和）
  2. 量化された型は、修飾したスコープから外に出られない（スコープ内での型の束縛）

特徴その1: 型推論の制限を緩和

まず1つ目の特徴について。

上位のランクの型は、下位のランクから決定することができないので、型の決定を先送りにできる（型推論の制限を緩和）

先ほどの関数 applyTrue で説明します。

最初に型検査で失敗したときは、applyTrue はランク1多相でした。

{-# LANGUAGE ExplicitForAll #-}

applyTrue :: forall a. (a -> a) -> Bool
applyTrue f = f True

実は forall が関数の最も外側にある場合、型の推論は関数の呼び出し元の責務になります。applyTrue の場合は、呼び出し元が型を推論してしまうので、関数 a -> a はランク0単相として扱われ、不十分な多相性のまま Bool の値を適用したのでエラーになったのでした。

型検査に失敗したときのエラーメッセージは、a は Bool かどうか分からない型に決定されているので、型が一致しないよと言っているわけですね。

• Couldn't match expected type ‘a’ with actual type ‘Bool’
  ‘a’ is a rigid type variable bound by
    the type signature for:
      applyTrue :: forall a. (a -> a) -> Bool
    at...

その後、applyTrue をランク2多相へ上げることで「applyTrue は呼び出し元から見て上位のランクである」という関係にしたのがこれですね。

{-# LANGUAGE RankNTypes #-}

applyTrue :: (forall a. a -> a) -> Bool
applyTrue f = f True

前述の通り、上位のランクの型は下位のランクから決定することができないので、関数の呼び出し元は型の推論を先送りにします。つまり、型推論の責務は関数の呼び出し先に変わったのです。

では、先送りにされた型の推論はどの時点で行われ型が決定するのか。実は、高ランクな多相型の場合、型を明示しない限り決定できません。明示しなければ型検査で失敗します。

applyTrue の場合は、関数内部で関数 forall a. a -> a に Bool の値を渡したので、この時点でようやく a は Bool であると推論されました。その結果、applyTrue と関数 forall a. a -> a との間で、期待する型と実際の型が一致したのです。

型の決定を先送りにするとこんなこともできるよ、という例をもう一つ。

以下の関数 applyTuple は、それぞれ異なる型の要素を持つタプル (True, 'a') に引数で受け取った関数 forall a. a -> a を適用する関数です。

{-# LANGUAGE RankNTypes #-}

applyTuple :: (forall a. a -> a) -> (Bool, Char)
applyTuple f = (f True, f 'a')

applyTrue のときと同じように、applyTuple が呼び出された時点では関数 forall a. a -> a の型の推論は先送りにされています。面白いのが、先送りにされた型の推論は、タプルのそれぞれ異なる型の要素に関数を適用する際、それぞれの型として推論できるのです。

特徴その2: スコープ内での型の束縛

次に、2つ目の特徴についてです。

量化された型は、修飾したスコープから外に出られない（スコープ内での型の束縛）

例えばランク2多相の (forall a. a -> a) は、括弧の中という限定されたスコープに対して型変数 a を量化しています。このような高ランクの型は、修飾したスコープの中で束縛されるので、外へ持ち出すことができません。

つまり、こういうことはできません。

(forall a. a -> a) -> a

そもそもスコープの中と外とではランクが違うので、a はスコープの外では存在できないのです。そして、このようなスコープに束縛された型は、スコーレム定数（skolem constants）と呼ばれています。

forallの探求はここで終わり

ここまでのforallの探求で、STモナドのトリックを解き明かすための準備が整いました。*5

次はいよいよ、STモナドはなぜ変更可能な参照を外へ持ち出せないのかを解き明かしていきます。

STモナドのトリック

それでは、先ほどのSTモナドから変更可能な参照を外へ持ち出そうとしたコードをもう一度見てみましょう。ここから読み解いていきます。

runST $ newSTRef 100

newSTRefの結果型の意味

まずは、newSTRef の部分です。シグネチャはこうでしたね。

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

ST s a の a は値を表しているので、newSTRef の結果型 ST s (STRef s a) で値を表しているのは、参照型の (STRef s a) ということになります。

それとスレッドを表す s ですが、少し前にこの s が ST と STRef の両方にいるのが変だと書きました。これは、ST の s を参照型 STRef にタグ付けすることで、STRef が ST の s に依存するという関係を作り出していたのです。

型変数 s のもう一つ注目すべき点は、型を推論する情報が何も無いので多相型を維持しているということです。先ほどの newSTRef 100 は、

GHCi> x = 100 :: Int
GHCi> :t newSTRef x
newSTRef x :: ST s (STRef s Int)

と s は多相型を維持したままになっています。

runSTの引数の型の意味

次に runST のシグネチャを見てみましょう。

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

runST は、(forall s. ST s a) -> a とランク2多相で、ST s a の s だけが限定されたスコープ内で量化されています。そのため、値の a はスコープの外へ持ち出すことができますが、s はスコープ内で束縛されたスコーレム定数なので外へ持ち出すことができません。

ここで疑問です。シグネチャを読み解く限り ST s a の a はスコープの外へ持ち出せるはずなのに、なぜこれは失敗するのでしょうか？

runST $ newSTRef 100

実はここで、newSTRef の結果型 ST s (STRef s a) のコレが効いてくるのです。

  • STRef は ST の s に依存している
  • s は多相型を維持したままになっている

つまり STRef は、スコーレム定数で型を推論するための注釈が何もない s に依存しているので、s に束縛される形でスコープの外へ持ち出すことができないのです。

以上が、STモナドはなぜ変更可能な参照を外へ持ち出せないのかの理由になります。

おわりに

最後まで読んでいただいてありがとうございました！

今回のSTモナドは、Haskell入門 関数型プログラミング言語の基礎と実践 の脚注で「STモナドは、GHCのRankNTypesという拡張を使っていて…」と書かれていて、「え？それってどういうこと？」というところから色々な記事や書籍を読んで、自分なりに理解できたことをまとめてみました。

Haskellの型システムの世界に魅了され今年5月に本格的に入門しましたが、探求すればするほど濃厚な世界が広がって行って楽しいですね。今後も探求を続けたいと思います！

訂正内容（2019/12/06）

以下の点で正確さに欠けていたので記事の一部を訂正しました。

「量化子を関数の内側で定義する」にて、タプルのそれぞれの要素に多相型関数を適用する例を挙げました。

{-# LANGUAGE ExplicitForAll #-}

applyTuple :: forall a. (a -> a) -> (Bool, Char)
applyTuple f = (f True, f 'a')

これに対して、「どちらか一方の型として推論されてしまい、両方の型に対応できない」と解説しました。実はそうではなくて、関数 a -> a の型は applyTuple の呼び出し元が推論してしまうので、関数 a -> a はランク0単相として扱われ、不十分な多相性のままタプルの各要素に適用したからエラーになったのでした。

これは単一の型でもエラーになります。

{-# LANGUAGE ExplicitForAll #-}

applyTrue :: forall a. (a -> a) -> Bool
applyTrue f = f True

この型の推論の制限を緩和し、呼び出された側で型の推論をさせるのが、ランクN多相というわけです。

上記の点、それと脚注のRank2Typesについても加筆修正しています。

@Mizunashi_Manaさん、ご指摘ありがとうございました！
https://twitter.com/Mizunashi_Mana/status/1201886227797950464

参考資料

*1:参考: 全称記号（Wikipedia）

*2:参考: 量化（Wikipedia）

*3:「任意ランク多相（Arbitrary-rank polymorphism）」と表記されることもあります。

*4:一般的にランク2以上はランクNとして表すことが多いようなので言語拡張は RankNTypes を使用しましたが、ランク2用の Rank2Types というのもあります。 Rank2TypesはRankNTypesのエイリアスで、歴史的経緯と互換性のために残されている非推奨の言語拡張なので、こちらの説明は無視してください。（参考）

*5:量化やスコーレムは述語論理の概念ですが、残念ながら私は述語論理を分かってないのでこれ以上詳しい説明はできないのです。