uehaj's blog

Grな日々 - GroovyとかGrailsとかElmとかRustとかHaskellとかReactとかFregeとかJavaとか -

Haskellのforallについて理解したことを書いておく(ランクN多相限定)。

haskell

Haskellのforallについて理解したことを書いておくyo!(ランクN多相限定*1 )。

前提知識のおさらい: 型・多相型・型検査・型推論…

最初に基本概念を整理しておきます。

  • IntやInt->Intは単相型、aやa->aは多相型である。ここでaを型変数と呼ぶ。型変数を含む型が多相型ってわけです。
  • 言語処理系の実装上、型という概念は型変数や型コンストラクタのツリー構造として表現される。Int,Char,[],->,(,),(,,,),IO aなどが型コンストラクタ。 a,bが型変数。組合せて(a->[Int])->[b]->(a,b)とか。::の右に書くやつです。
  • 型は、プログラムの字面上に直接的実体がある関数や変数だけではなく、値を生じさせる部分式すべてに付随し、コンパイル時に決定されるべき情報である(値あるところに型がある。*2 )。それを決定しようというのが(静的)型検査である。Haskellでは基本としてhindley-milner(以降、HMと記載するときもある)と呼ばれる型推論機構をベースにして多々拡張したもので型推論を行なう。この記事はhindley-milnerのロジック(こちらにscalaのコードがある)を読んで理解したことのみをベースにしHaskellに対して類推したものである*3。hindley-milnerでは型検査は型推論と一体化しているような気がするのでこの記事では「型検査」には「型推論」が含んでいるというつもりで「型検査」という用語を用いる。なお、Hindley-milner型推論の実装については、こちらの記事「Hindley-Milner型推論アルゴリズムをGroovyで書いてみた」もどうぞ。
  • 多相型は、1個以上の型変数を含んだ型であり、多相型を解決するための仕組み(後述)を「型スキーマ」もしくは「型抽象」と呼ぶ。型スキーマ中の特定型変数を置換し(結果、単相型が得られるかもしくは単相型に近づく)、その結果を得る操作を型スキーマのインスタンス化と呼ぶ。これは、λ抽象に引数の値を与えると、具体的な結果の値が得られるのと同じ。値の世界のλ抽象は、値を与えると値が返るが、型の世界の型抽象は、型を与えて型が返るような型の世界の関数である。多相型というのは「パラメタを持った型」であり「パラメタに具体値をあてはめることで初めて利用できるような型」なわけです。まあ直感的にそれはそうでしょう。(Javaのジェネリクスも同じだと言える)

HM型検査器の構造と実行

  • 「環境」という概念を導入する。環境は識別子*4から型スキーマへの対応表であり型検査に使用する(コンパイル一般のためには、環境は他の情報も含むのかもしれない。ASTとか)。環境は、処理開始時のトップレベルは「組み込み定義」情報だけを含んでいるところから始まり、関数を定義したり、あるいは他モジュールから識別子をインポートすることによって、あるいはラムダ束縛やlet束縛で識別子が定義されるたびに、エントリが拡張されそれぞれのネストレベルで使用される。
  • オリジナルhindley-milnerではトップレベルの関数のみ*5に型スキーマを明示的に付与できる*6。
    例: func :: a-> Int。これはfunc :: forall a. a -> Intの略記法である。

forallと型スキーマ・型抽象、インスタンス化のタイミング

  • forallは型スキーマ(型抽象)を表わし、型の世界のλである。forallをλに機械的に置換してみると良い。先の例func :: λa.(a->Int)について
    • (λa.(a->Int)) Int の返り値は、Int -> Int、
    • (λa.(a->Int)) [String]の返り値は、[String] -> Int
    みたいな。ただ、値の世界のλとは異なり、型抽象をプログラムから直接的に明示的に呼ぶものではない。構文木上の型検査や型推論の処理中で暗黙的に呼び出される。型検査・推論の中で型スキーマがどう扱われるか、どういうタイミングでインスタンス化されるかがforallの意味を決めている。
  • 型検査の過程において、プログラム字面上の「識別子の出現」が型スキーマのインスタンス化のタイミングである。なおインスタンス化一発ですべての型変数が消去できるわけではない。構文木をツリーとして再帰的に辿るhindley-milner型検査過程の各ステップで、型変数を媒介として双方向的・全体的に型がきまっていく*7。こんなことが可能なのはある意味驚きであるが、決まるそうなのである。これがHindley-milnerの凄いところである。処理対象プログラム中に識別子が現われたら、環境から型スキーマを引っぱってきてインスタンス化して、構文木構造(関数適用、let、lambda..)ごとに決められたルールで双方向パターンマッチ(ユニフィケーション、単一化)して型を決めていく。

ちなみに型検査器を外部から見て一言で言うと

  • 外部から見ると、hindley-milner型検査器は、型変数を含んだ連立程式を解く、制約問題ソルバとみなせる。

ランクN多相は型スキーマを一級市民の型として扱うこと

  • forallが型スキーマのトップレベルにしかあらわれないのがHindley-milner。これに対し、forall. .(.(.. (forall..)..).)という途中レベルで表われてよいのがランクN多相(SystemFに相当？良くわかってない)。これは、λ計算で言えば、「トップレベルの識別子に=で代入する右辺の最左でしかλが使えない」のがhindley-milnerであり、λ抽象を引数や関数の戻り値に使える高階λ計算がランクN多相に相当する。つまり関数を一級市民として扱える(高階操作)ような感じで型抽象を一級市民として扱えるのがランクN多相である。

forallの機能

  • 型スキーマのインスタンス化について機能面で言及すべきことがあって、それは型変数名をリネームすることによる衝突回避機能を持つということである(これもλ抽象でできるのと同じ話だが)。型変数に単相型をマッチさせる、という行為に関して、型変数はそれを媒介とした型の一致・不一致の判別の一意性を判定するものであるからして、一致させないためにリネームしたり、リネームの効果がおよぶ特定の範囲では一致させる、というようなコントロールができる。これを利用しているのがかの有名なST Monadで、詳しくはこちら「Lazy Functional State Threads 」(って原論文を読むしかないのか…。しかしweb上では他に理解可能な情報を見付けられませんでした。)。

HMの限界

  • hindley-milnerの型検査には双方向性があるため、「ある範囲」を対象とした「型変数の連立方程式」というか制約問題を解く必要があるのだが、そしてGHCはおそらくそれを「トップレベルに定義した関数」という単位でやる*8のだが、hindley-milnerオリジナルでは関数引数の型のインスタンス化について、「関数そのものに付随する型スキーマの実体化」1回分の中で決定しようとするため、識別子の複数回の使用それぞれで異なるインスタンス化ができない。このことは、多相関数を引数にとる関数を定義する際に多相性が1回限りしか発揮できないということなので不便なときがある。例えば、[a]->Intを引数にとる関数([a]->Int)->Intがあったとする。
    func:: ([a]->Int)->Int
    func f = f [1,2,3] + f["a","b","c"]
    これは型エラーになる。なぜならf[Int]、f[ [Char] ]というfの出現2つにそれぞれ対応してインスタンス化されることで生成された、f::[Int]->Intとf::[ [ Char ] ] -> Intというボトムアップで定まる2つの型制約を、引数としての識別子fの型が同時に満せないからである。

ランクN多相の意義と動作例

  • これを回避するために、「型スキーマを取ってきてインスタンス化する」という行為を、1つの関数の中で何回も行なえるようするための拡張が、GHCのランクN多相(XRankNTypes)である。その実装はたぶん、型スキーマ(型変数を含む型)を型の一種として扱い(型スキーマ型、forallつきの型として表現)、型スキーマを、関数トップレベルだけではなく、関数引数部分などに登場可能にした上で、λ変数が型スキーマ型にマッチしたとき、そのλ変数の使用(出現)それぞれでインスタンス化してマッチを継続するのである*9。
  • GHCiでの書き方としてはオプション-XRankNTypesを指定して、
    func:: (forall a. [a]->Int)->Int
    func f = f [1,2,3] + f["a","b","c"]
    こう。これでコンパイルも通って
    GHCi> func length
    6
    のように実行できる。ここで、fの出現ごとに「forall a.[a]->Int」という型スキーマがインスタンス化される様子が心に浮びますでしょうか。

名前が悪いぞforall

あとは非生産的な話。

  • プログラミング言語としてのHakellにおける、forallというキーワードで起動される言語機構を理解するのに、全称量化を理解する必要はないし形式論理学の知識は不要である。「全称量化」という単語を知る必要すら一切ない。それは理解に寄与しない。ていうか理解の妨げになるだけだッ。名称としてそれしかないので「全称量化子」とか「全称量化された」とか呼ぶしかないので、しょうがない面もあるのだろうが、ミスリーディングなだけである。forallというキーワードから「all(全ての)」という含意を読みとる必要すらない。必要があるってのなら値に関して同型であるλについてもどういう意味でallなのか、allを付けないのかプログラミングレベルでの説明を聞かせてほしい。 ∀が型抽象の型表記で慣例的に使われてるのを敬意を表してなのか論理学者は慣れてるからなのか、結果的には無批判に導入しただけだろ、っていう。最終的にはカリー・ハワード同型対応で、そういう方面に応用できるのだとは思うが、Haskellをプログラミングのみに使いたいプログラマにとっては不要なことである。迷惑なことである。

型システム入門 −プログラミング言語と型の理論−
型システム入門 −プログラミング言語と型の理論−
posted with amazlet at 14.01.23
Benjamin C. Pierce
オーム社
売り上げランキング: 220,470
Amazon.co.jpで詳細を見る

*1:ここを読むと、ランクN多相を実現する以外に2つぐらい意味があると。ExistentialQuantificationについてはきちんと理解してないが理解したら何か書くかも。

*2:加えて、値が無いところにもたまに型がある。

*3:本当は「型システム入門」とかにさぞ詳しく書いてあるであろう。でも読めてません。ごめんなさい。

*4:環境のキーとなる「識別子」はプログラム本体で使われる識別子である。型側でのみ使われる「型変数」の名前ではない。混同しないこと。両者は混在することは決してない。

*5:Haskellでは::でlambda変数とかにも他にも付与できる

*6:例のscalaのコードから読む限りでだが、letで定義する識別子には暗黙に形成された型スキーマが付与される。なのでletを介入させるとランクN多相を導入しなくても型スキーマを複数回インスタンス化できそう(未確認)(2014.01.26追記できない)。この意味でletはlambda+関数適用のシンタックスシュガーではない。haskellもそうなってるようだ。不思議。

*7:最終的にもすべてが単相型に落ちずに、型変数が残ることもあるだろう。つまり多相関数はそれである。

*8:これも予想でしかない。前述のScalaのコードでは、任意の構文木の枝に対して型チェック(tp() )を起動可能だが、それは正しい環境を引数に渡せる前提である。正しい環境を構築するためには、上の方から解析を結局していかなければならないよね。だから関数単位だろうと予想しました。遅延評価とかを使って全然違う単位・順序で解析するのかもしれませんが。

*9:この動作は裏をとってない。SystemFなりHaskellのランクN拡張でどう実装しているかは不明。「私だったらそう実装したい」というレベルの話である。