Haskell/存在量化された型

存在型 (Existential types もしくは短く existentials) は型の集合をひとつの型へと圧縮する方法である。

最初に注意してくことがある。 存在型は GHC の 型システム拡張 の一部である。これらは Haskell98 の一部ではなく、-XExistentialQuantification という追加のコマンドライン引数をつけるか、{-# LANGUAGE ExistentialQuantification #-} をソースコードの先頭に置くかして、コンパイルしなければならないだろう。

forall キーワード

forall キーワードは明示的に型変数をスコープに持ってくるのに使われる。たとえば、これまで次のように書かれているのは何度も飽きるほど見てきただろう。

しかし、これらの a と b は何なのだろうか？まあ、これらは型変数だ、とあなたは答えるだろう。コンパイラは、小文字から始まる型名を見ると、その役割を埋めるためにどんな型も許容するものとみなす。これらの変数を '全称量化された' (universally quantified) するという方法もある。もし形式論理を学べば、量化子に出くわすに違いない。'任意の～について' (for all、$\mathrm{\forall }$) と '～が存在する' (exists、 $\mathrm{\exists }$)である。これらの '量化' はこれらの後に現れる。たとえば、$\mathrm{\exists }x$ は続く　少なくともひとつの値 x について続く命題が真であることを意味する。$\mathrm{\forall }x$ は想定されうるすべての x について続く命題が真であることを意味する。たとえば、$\mathrm{\forall }x,x^2\ge 0$ や $\mathrm{\exists }x,x^3=27$ だ。

同じように、forall キーワードは 型 を量化する。map の型を次のように書きなおすことができる。

そして、我々が考えるどんな a や b についても、map は (a -> b) -> [a] -> [b] という型をとることがわかる。たとえば、a = Int と b = String という型を選ぶかもしれない。そして、map は型 (Int -> String) -> [Int] -> [String] をもつというのは妥当だ。map の一般化された型をより具体的な型へと インスタンス化 しているのだ。

しかしながら、Haskell では、知っての通り、小文字で始まる型は暗黙的に forall を持つことになっており、つぎの 2 つの宣言が同じであるのと同様に、 map の 2 つの宣言は同じである。

どこに forall キーワードを置くかによって明示的に Haskell に伝え既定の振る舞いを上書きすることができるということは興味深い事実だろう。使い方のひとつは、存在型( existential types )や単に存在 ( existentials ) ともいう 存在量化された型 ( existentially quantified types ) を構築することである。だがちょっと待ってほしい。forall は 全称 量化子ではないのか？どうやってそこから抜けだして存在型にするのだろうか？これについては後の節で検討するが、まずは実際に存在型の力の例を見て、その深淵に飛び込んでみようではないか。

例: 異なる型が混合されたリスト

Haskell の型クラスシステムの根拠となっているのは、すべての共通の性質を共有する型のグルーピングである。つまり、もしなんらかのクラス C をインスタンス化している型を知っているなら、この型についていくらかわかっていることがあることになる。たとえば、Eq をインスタンス化する Int は、Int の要素は等値性を比較できることを知っている。

もし、あるクラスのインスタンスである様々な型の値を、一つのリストに入れることができれば便利であろう。しかし、リストの要素は全て同じ型でなければならないので、通常はこのようなことはできない。このようなときに、存在型を使って 'type hider' や 'type box' と呼ばれるものを定義することによってこの条件を緩めることができる。

このデータ型の定義が何を意味するかを詳しく説明するつもりはないが、この意味は直感的に明らかだろう。重要なのは、３つの異なる型の値に対して構築子を呼び出していて、すべてを一つのリストの中に置いていることだ。このことは、それぞれの値が結果的に同じ型になったということを示している。これは、forall キーワードを使い、この構築子に SB :: forall s. Show s => s -> ShowBox という型を与えたからである。heteroList を引数に取る関数を書いているとき、このリストの要素に not のような関数を適用することはできないだろう。なぜなら、このリストの要素は Bool とは限らないからである。しかし、これらの値のそれぞれについてわかっていることがある。show を通じて文字列に変換することができることだ。実際、わかっていることはこれだけである。

もうちょっとだけ踏み込んでみよう。ShowBox に対する show の定義――(*) see the comment in the text below とつけられた行――において、s の型はわからない。しかし先ほど述べたとおり、SB 構築子の制約によってその型が Show のインスタンスであることならわかる。それゆえ、この関数定義の右辺にみられるように、s に対して関数 show を使うことは妥当なのである。

f に関しては、print の型を思い出そう。

ShowBox は Show のインスタンスであると定義しただけで、リストの値を出力できる。

存在 という言葉の説明

先ほどの疑問に戻ろう。forall が全称量化子ならば、なぜ存在型と呼ぶのだろうか？

まずforall は、まさに '任意の～について' (for all) を意味する。型についての考え方として、その型の値の集合だと考えることができる。たとえば、Bool は集合 {True, False, ⊥} (ボトム ⊥ はいかなる型のメンバでもあることを思い出そう！)であり、Integer は整数(とボトム)の集合だし、String は可能なあらゆる文字列(とボトム)の集合などなど。forall はこれらの集合の共通集合を与える。たとえば、forall a. a はすべての型の共通部分であり、{⊥} のはずである。これは値(つまり要素)がボトムだけであるような型(つまり集合だ)である。なぜだろうか？考えてみよう。Bool に現れる要素はいくつだろうか？たとえば文字列は？ボトムはすべての型に共通する唯一の値だ。

さらにいくつか例を挙げる。

1. [forall a. a] はすべて型 forall a. a を持つ要素のリスト、つまりボトムのリストの型だ。
2. [forall a. Show a => a] はすべての要素が型 forall a. Show a => a を持つようなリストの型だ。Show クラス制約は集合を制限する(ここでは Show のインスタンスだけの共通集合である)が、まだこれらすべてに共通する値は $\perp$ だけだ。
3. [forall a. Num a => a]。再び、それぞれの要素がすべて Num のインスタンスであるような型の要素のリストである。これが含めるのは型 forall a. Num a => a を持つような数値リテラル、つまりまたボトムだけを含む。
4. forall a. [a] は、とにかく呼び出し側からみなされうる、なんらかの(同じ)型 a が要素であるリストの型である。

型は多くの値を共通に持つわけではなく、幾つかの方法でだいたいの型の共通集合が結局はボトムの組み合わせになることがわかった。

さきほどの節で 'type box' を使って異なる型を格納するリストを作ったこと思い出そう。理想的には、異なる型を格納するリストは [exists a. a]　という型、すなわちすべての要素が型 exists a. a を持つようなリストであるとよい。この 'exists' キーワード(これは Haskell には存在しない)は推測されるように型の 和集合 であり、そして [exists a. a] はすべての要素がどんな型も取れる(かつ異なる要素は同じ型である必要はない)リストの型なのである。

しかし、データ型を使ってほとんど同じ振る舞いを得たのだった。これを定義してみよう。

これは次のようなものを意味する。

そして、MkT に任意の値を渡すことができ、それは T へ変換されるだろう。では、MkT の値を分解 (deconstruct) するとき、何が起きるのだろうか？

示したように、x はどんな値でもとれる。これは、それがなんらかの任意の型の要素であることを意味し、型 x :: exists a. a を持つ。言い換えれば、この T の定義は次と同型(isomorphic)なのである。

そして突然存在型が現れた。いま、不統一 (heterogeneous) リストを作ることができる。

もちろん、heteroList をパターンマッチしたとき、知っているのはそれがなんらかの任意の型であることだけなので、その要素に対して何もすることはできない。しかしながら、もしクラス制約を導入すれば、

これ統一された (isomorphic) 型である。

再び和集合をとる型を制限をするため、クラス制約を提供する。MkT' の中にある値は、Show のインスタンスである何らかの任意の型の値であることがわかる。これが意味しているのは、型 exists a. Show a => a の値に対して show を適用することができるということだ。どの型なのかわかってもまったく問題はない。

まとめると、データ型を全称量化子の相互作用は存在型を生み出す。forall を含む型の多くの興味深いの適用がこの相互作用を使用することにより、それらの型を存在型とするのである。存在型が欲しい時はいつでもデータ構築子でそれをラップしなければならず、[exists a. a] のように公然と現れることはできないのだ。

例: runST

ST モナドはこれまで出くわしたことはないかもしれない。本質的にはこれは State モナドを強化したものだ。これはより複雑な構造を持ち、より高度な話題を含む。これは本来 Haskell に IO を提供するために書かれたものだ。[[../Understanding monads/]] の章で言及したように、IO は基本的には現実世界の情報すべての環境つきのただの State モナドである。実際、GHC 内部では少なくとも、ST が使われており、環境は RealWorld はと呼ばれる型である。

State モナドから外へ出るには、runState を使うことができる。ST における類似した関数は runST と呼ばれており、これは独特な型をもつ。

これはより複雑な rank-2 多相 (polymorphism) と呼ばれる言語機能の実例となっているが、ここでは詳細には立ち入らない。重要なのは初期状態を与える引数は存在しないことに気づくことである。代わりに、ST は State に対して異なる状態の記法を使用する。State は現在の状態を取得 (get) と設定 (put) することを可能にするのに加え、ST 参照 のインターフェイスを提供する。newSTRef :: a -> ST s (STRef s a) によって初期値を与え STRef という型を持つ参照を作ると、これを操作する readSTRef :: STRef s a -> ST s a と writeSTRef :: STRef s a -> a -> ST s () を使うことができる。ST 計算の内部環境はある特定のものではなく、それ自体は参照から値への対応付けである。それゆえ、初期状態は単に参照を含まない空の対応付けなので、runST に初期状態を提供する必要はない。

しかしながら、ことはそれほど単純ではない。ひとつの ST 計算において参照を作り、それが他で使われることを止めにはどうすればよいのだろうか？(スレッド安全性の理由で) ST 計算は初期内部環境はいかなる特定の参照を含むという仮定をも許容すべきではないので、これを許容したくはない。より具体的には、次のようなコードは不正としたい。

これを防ぐにはどうすればいいのだろうか？runST の型においての rank-2 多相の効果は最初の引数のなかだけに s のスコープを制約する ことだ。言い換えれば、この型変数 s はふたつめの引数には現れないが最初の引数に現れる。どうやってこれをうまくやるのかみていこう。次のコードのようにする。

コンパイラはこの型を一致させようと試みる。

最初の括弧の forall の重要性は、その名前 s を変更することができることだ。これは次のようにかける。

$\mathrm{\forall }x.x>5$というのは$\mathrm{\forall }y.y>5$というのとちょうど同じ、というのは数学的に理にかなっている。変数に別のラベルを与えているだけである。しかしながら、先ほどのコードには問題がある。runST の返り値の型に対しては forall はスコープに含めないので、そこでは s の名前を変えないことに注意しよう。しかし、突如として型の不一致が起きる！最初の引数において、ST 計算の返り値の型は runST の返り値の型と一致しなければならないが、そうなっていない！

この存在性の重要な機能は、最初の引数でコンパイラに状態の型を一般化することを可能にし、返り値の型はそれに依存することはできないことだ。これは　この依存性の問題をうまく回避し、異なる呼び出しの間で参照が共有されることができないことにより、それぞれの runST 呼び出しをそれ自身の小さなヒープ内に '区切る' (compartmentalise)のである。

組み込み要素としての量化

全称量化はまだ定義されていないデータ型を定義するのに便利である。Haskell に組のような型がなかったとしよう。量化は次のような定義を可能にする。

newtype Pair a b=Pair (forall c.(a->b->c)->c)

参考文献

• GHC のユーザガイドには、(あなたも知っておくべき)課せられている様々な制限を含む存在量化についての 役に立つ情報 がある。
• 　Simon Peyton-Jones および John Launchbury、Lazy Functional State Threads は ST の背後にある更に詳しいアイデアを説明している論文である。

---

テンプレート:Haskell navigation

en:en:Haskell/Existentially quantified types