Groovy 2.3のtraitをもうちょっと調べてみるついでにScalaのtraitを理解する
(訂正2014/4/17)以下の記事ではGroovy 2.3のtaritはスタッカブルには使えない、と書いておりますが、以下によれば次のベータ(Groovy 2.3-beta-3かな)ではスタッカブルトレイトが利用可能になるようです。
次βでGroovy 2.3のtraitはスタッカブルになるようですヤター RT @CedricChampeau: @tim_yates yes it is. See the other examples in the test case, stackable traits
— uehaj (@uehaj) April 17, 2014
先の記事ではGroovy 2.3のtraitをかるく紹介してみました。
Scalaの比較も試みましたが、なにしろScalaのtraitをあんまり知らないので、「Groovyのtraitにある機能に限っての、Scalaの対応物と比較」という比較になっておりました。その意味で、「Scalaにしか無い機能」というのは比較の眼中になかったのです。
ということで「Scalaスケーラブルプログラミング」のtraitの章を読んでtraitを理解したつもりになったので、本格的な比較をしてみます。
Scalaスケーラブルプログラミング第2版
posted with amazlet at 14.04.16
Scalaのtraitは単なる多重継承じゃないよ(という主張)
上記の本のScalaのtraitのとこを読んでると、「単なる多重継承じゃないよ」という主張がひしひしと伝わります。その根拠の一つは、traitでは「super」の意味が拡張されているということのようです。
superの意味が拡張されなければならない理由はごく単純で、素朴な多重継承では「super」が示す親クラスは一つではないからです。多重継承というのは親が複数あるということですからね。かといってsuperを利用不可にしてしまうと、単一継承でのsuperの使い道であるところの「super経由で親のインスタンスを取り出して、superのメソッドを呼び出し、その前後に処理を追加する」という定番のテクニックが使えなくなってしまいます。
Scalaでは、この問題を発展的に解決するために、トレイトの多重継承によって形成されるDAGの要素であるトレイトを、特定のルールに従って線形に並べ直します。線形化すれば、単一継承の様にsuperいっちょうで親を次々とたどっていけるようになります。その順序は良くわかんないものですが、最後に根っこに到達するDAG上の一筆書の経路です。
「発展的解決」の意味は、withの指定順序を替えると処理順序が変わるので、動作のバリエーションが作れるということです。このようなトレイトの用法をスタッカブルトレイトと呼ぶようです。もっとも、試験しなければならないパターンの組み合わせ爆発を考えると、容易に悪夢になり得るとも思うわけですが。
ポイントとして、この線形化経路、すなわち任意のトレイトにおいてsuperが何を指すかは、一つのトレイトを見ただけでは決定できません。あるトレイトが、どうwithで指定されたか(Groovyで言うtraitの複数implements)、によって、順序が変わっていくからです。
trait C extends A with B;
のときBのsuperは(たぶん)Aですが、
trait C extends B with A;
のときのBのsuperは(確か)Cになるでしょう*1。これは、new ... with構文で生成される内部クラスを含め、withを使用してトレイトをミックスインしたクラス定義ごとに、線形化された順序になるようにsuperのチェインを構成・初期化するようなコードないしデータ構造が用意されるのでしょう。
クラス定義に指定されたwithのパターンが、この線形順序をコンパイル時に決定します。superを辿っていくと、この線形化順序で「多重継承上のすべての親」を辿り尽せることが保証されます。superが実際に示す先のインスタンスの型は、実行時にならないと決定されませんので、その意味でsuperは動的です(ただ動的といっても、JavaのメソッドでList型の引数に渡ってくるインスタンスがArrayListなのかLinkedListなのかあるいはそれを継承した他のクラスのインスタンスなのか動的に決まる、のと同じ意味で動的です。「superの型」が抽象クラスかインターフェースになるということです)。
方やGroovyでは
Groovyでは、(トレイトを明示指定しない)superが利用できないので、必要なトレイトを必要な順序で組み替えてsuperを頼りに処理を組み合せるスタッカブルトレイト的に利用することはできませんヨー(2014/04/17追記。冒頭に書いたように次のβでは可能になるようです。ヤター。)。あと、Groovyでは親トレイトの探索順序が違います。例えsuperの参照ができないとしても、「祖父と伯父」の両方で定義されたメソッドのどっちが優先されるか、といった疑問に答えるためには、線形化された順序が定まっているはずです。調べると、Groovyのトレイトは単純な深さ優先探索です。これに対してScalaはとんでもなくわからないルールで決まります。
ちなみにGroovyの親トレイトの探索順序は以下で調べました。
trait A1 {/* String whoami(){"A1"}*/ }
trait B1 implements A1 { /*String whoami(){"B1"}*/ };trait B2 implements A1 { /*String whoami(){"B2"}*/ };
trait C1 implements B1 { /*String whoami(){"C1"}*/ };trait C2 implements B1 { /*String whoami(){"C2"}*/ };trait C3 implements B2 { /*String whoami(){"C3"}*/ };trait C4 implements B2 { /*String whoami(){"C4"}*/ };
trait D1 implements C1,C2,C3,C4 { /*String whoami(){"D1"}*/ };trait D2 implements C1,C2,C3,C4 { /*String whoami(){"D2"}*/ };
class E1 implements D1,D2 { /*String whoami(){"E1"}*/ };
E1 e1 = new E1()
println e1.whoami()
// 上を実行し、表示されたものからwhoami()を削除していくと、その次に到達する
// ノードが判るのでそれを繰り返すと親の順序がわかる。結果は以下のとおり
// E1 -> D2 -> C4 -> B2 -> A1 -> C3 -> C2 -> B1 -> C1 -> D1
// これは下から深さ優先探索してるのと同じ。
さてここで、@ForceOverrideが指定されたメソッドが1つでもあると、それは@ForceOverride指定されていないメソッドすべてに勝ちます(但しE1を除く。例え@ForceOverrideであろうとも、E1の普通メソッドに勝つことはない。そこまで強くはない。)。@ForceOverride同士では、やはり上と同じように、下から上への深さ優先探索(浅さ優先探索)となるのです。
(追記)
Groovy.2.3正式版では@ForceOverrideはデフォルトかつ必須の動作になり、アノテーション自体は削除されました。
この線形化順序(探索順序)の違いが実用上どういう得失として表われてくるのかというと…ものすごくわからないな。見当もつかないな…。
Groovyでしかできないこと
共通の親トレイトを必要としない形でのトレイト側メソッドの優先
(本節は、2014/4/17訂正あり。Scalaでもself type annotationにより可能とのこと。id:xuweiさん、指摘ありがとうございます。)
Scalaで、スタッカブルを構成するには、組み合せたいトレイト群から構成されるDAG全体の親となるようなトレイト(抽象もしくは具象でも別に良い)が1個必要です。それから、すべてのトレイトだけでなく、末端のクラスがそれを継承していないと、superが作れませんし、トレイトがクラスのメソッドに優先するoverrideにもなりません(いわゆる「abstract override」の話)。
このabstract overrideを使って、ScalaでAOPをやる、という記事がありますが、これだと任意のメソッドをインターセプトできません。インターセプトしたいメソッドを定義したトレイトを作りかつそれをextendsしたクラスに対してしか適用できません。
(次のパラグラフは、2014/04/17追記)
しかし、Scalaには「self type annotation」という機能があり、共通の親トレイトなしでもミックスインによりクラスのメソッドをオーバーライドできます(このときsuperをスタッカブルに使えるかは未確認）。コード例はid:xuweiさんが提示してくれたこちらを参照してください。
これに対応するのですが、Groovyでも、共通の親トレイトはなしで既存クラスに対するオーバーライドができます。置換したいメソッドを持ったクラスに何らかのトレイトをextendsさせるために編集する必要も、ソースコードがある必要もありません。
例えば。
trait FileNameIsHogeHoge {
@groovy.transform.ForceOverride
String getPath() {
return "hogehoge" // (1)
}
}
class MyFile extends File implements FileNameIsHogeHoge {
MyFile(String fileName) {
super(fileName)
}
}
f = new MyFile("/tmp/file.txt")
assert f.getPath() == "hogehoge"
こんな感じ。
泣き言を正直に言えば、(1)でやっぱりsuperを参照したくなることですね。わけですが、次のβを待ちましょう。
今日はこんなところで。
Scalaスケーラブルプログラミング第2版
posted with amazlet at 14.04.16
*1:自信なし!!たぶん違うと思う。
Groovy 2.3.0-betaが出たのでtraitを触ってみたメモ
Groovy 2.3.0-beta-1とbeta-2が出たので新機能traitをかるく触ってみました。
注意! 以下は現時点で2.3.0-beta-1と2の振舞いとドキュメントを調べた限りの情報です。正式リリースに向けて変更される可能性があります。
traitの概要と目的
Groovyのtraitは、一言で言って「実装の多重継承」を可能とする仕組みです。詳しくはこちらの本家ドキュメント(英語)をどうぞ。
GroovyおよびJava 7までのJavaでは、インターフェースは多重継承することができましたが、クラスは多重継承できませんでした。実装、すなわちメソッド本体の定義や、非public static finalなフィールド(インスタンス変数)定義はクラスでのみ可能であり、そしてクラスの継承は単一継承のみ(親が1つだけ)が可能なので、実装の継承は、ツリー型に制限されていました。北斗真拳と南斗聖拳の系列があったときDAG型の「両方の継承者」という統合はできないわけです(少なくとも実装の意味では。ジャギは実装は継承してない。上っ面のインターフェースのみです謎)。とにかく、いままでは実装の多重継承はできなかったということです。
Groovyのtraitでは以下の両方ができます。
- クラスのようにメソッド本体やフィールドを定義する
- インターフェースのように多重継承する
結果として、実装の多重継承ができるようになりました。
Java8のインターフェースでは、デフォルトとしての実装(メソッド本体)が定義でき、実装の多重継承もできるので、近いものがありますが、以下のような差異があります。
- groovyのtraitではインスタンス変数(フィールド)も定義できる。つまりtraitで定義されたメソッド群の間でインスタンス固有のデータを共有・保持できる。(Scalaのtraitも同様)
- groovyのtraitは、メソッドのデフォルト実装を定義するだけではなく、親traitのメソッドをオーバーライド定義することもできる。
- groovyのtraitで定義したメソッドは、親クラスや他のtraitのメソッドに優先する(
@ForceOverride使用。(Groovy.2.3正式版では@ForceOverrideはデフォルトかつ必須の動作になりアノテーションは削除された。) Scalaのabstract overrideの動作) - groovyのtraitはJava 8以前のJava VM(Java 6,7..)でgroovyを実行する場合でも利用できる(Scalaのtraitも同様)
GroovyのtraitはScalaのtraitと極めて良く似ています。traitの定義と静的な使用についてはscalaのそれとほぼ同様です*1。差異は、主に動的なtraitの実装に関するところであり、後述します。
表にまとめるとこんな感じ。
| Java/Groovyクラス | Java(〜Java7)およびGroovyのインターフェース | Java8以降のインターフェース | Groovyのtrait | Scalaのtrait | |
|---|---|---|---|---|---|
| 定義に使用するキーワード | class | interface | interface | trait | 同左 |
| 実装の単一継承 | ○ | × | ○(メソッドのデフォルト実装のみ) | ○(フィールド使用・定義およびtrait側メソッド優先も可) | 同左 |
| 実装の多重継承 | × | × | ○(メソッドのデフォルト実装のみ) | ○(フィールド使用・定義およびtrait側メソッド優先も可) | 同左 |
コード例
たとえばこんな感じです。
trait A {}
trait B extends A {}
trait C extends A {}
class D implements B, C {}
詳しくはドキュメントをみてください。
以下もよろしければどうぞ。
www.slideshare.net
衝突!
さて実装の継承においては、多重継承だろうが単一継承であろうが、衝突というものを考慮する必要があります。
継承というのは親のフィールドやメソッドを引き継ぐということなので、子供は親のメソッドやフィールドを持っているかのように振る舞う必要があります。
単一継承であれば、お爺ちゃんと父で衝突すれば(名前が同じで実装が異なるようなものがあれば)、子供は(子供自身でオーバーライドしない限り)より近い祖先である父のものを持っているかのように振舞います。
多重継承の場合、加えて、父親(もしくはその祖先)と母親(もしくはその祖先)がそれぞれ同名で異なるメソッド実装やフィールドを持っているとき(=衝突)の考慮が必要ですが、子供はどっちのものを持っているかのように振る舞うべきでしょうか。
Groovyのtraitにおける衝突の解決もしくは回避
メソッド名に関しては、Groovyのtraitの衝突解決のデフォルトは指定したトレイトの順に、後勝ちです。つまり「implements 父,母」もしくは後述の形式「withTrait(父,母)」のように複数トレイトを親として指定したときに、所属トレイトを明示指定しないメソッド名が衝突していれば、指定がより後ろである母側のメソッドが指定されたとみなされます。後勝ちが嫌な場合、子供でオーバーライド定義して明示的に後じゃない方を呼ぶこともできます(「トレイト名.super.メソッド名」で指定する)。ちなみにScalaでは潜在的に衝突しているとき、衝突しているメソッドを子供でオーバーライドしないとエラーになり、常に明示的な手動の衝突の解決が求められるそうですが、Groovyではそんな配慮は無いので「意図せざる偶然の衝突」に注意が必要になります。
コード例としてはこういうことです。
trait A { String foo(){"A"}}
trait B { String foo(){"B"}}
class C implements A,B {
}
class D implements B,A {
}
c = new C()
assert c.foo() == "B"
d = new D()
assert d.foo() == "A"
class E implements A,B {
String foo(){A.super.foo()}
}
d = new E()
assert d.foo() == "A"
フィールドに関しては、フィールドの値を保持する変数名のリネームによって衝突が事前回避されます。トレイトで定義したフィールドは、そのトレイトの実装時に、
トレイトのFQCNの'.'を'_'に置換したもの+'__'+フィールド名
にリネームされた変数名のフィールドが、子クラス側で暗黙に定義されます。フィールドがprivateの場合も、publicの場合もいずれもです。子クラス側のインスタンスのフィールド名を直接指定する場合、後勝ちもクソもなく、このリネームされた名前で常に明示する必要があります。(リネームされる前、トレイト内のメソッドの定義においては、リネーム前の本来のフィールド名をソース記述上は使えます。しかしリフレクションとかでは違う名前になっているでしょうから注意)。
もっとも、フィールドがprivateであれば外部から指定することはできない(建前上不可視*2 )ので、問題になるとすればフィールドがpublicな場合のみでしょう。以下は例です。
trait A {
public int a;
}
trait B extends A {
public int b;
}
trait C extends A {
public int c;
}
class D implements B, C {}
def d = new D()
println d.A__a
println d.B__b
println d.C__c
このようなフィールド名のリネームは、やや不自然に感じるかもしれませんが、フィールドを直接参照するのではなくgetter/setterを通じて扱えば、メソッド名の解決の話になりリネームされたフィールド名は隠蔽されるので、プログラマが意識することはなく、実際問題としては意識する機会はあまり多くないでしょう。
重要なのは、このリネームルールから、継承経路上に表われるすべてのトレイト実装は、そのFQCNによって単一化されるということです。ダイヤモンド継承(菱形継承)問題はこの形で解決されています。C++で言えば「仮想基底からの継承(仮想継承)」だけの扱いになるわけです。まあ、それでいいね。なんぼか直観的です。Scalaではどうなるかは知らない。
trait定義
classやinterfaceの代わりにキーワードtraitを使用します。それでだいたい期待通りに動作するでしょう。traitのコンパイル結果は、実体としては(クラスファイル上は)インターフェースといくつかの内部ヘルパクラス群になります。Javaからはトレイトはインターフェースとして見えるので、Groovyのtraitを実装しているGroovyのインスタンスはJavaから扱えます。Groovyのtraitをtraitとして継承したクラスをJavaで定義するのはおそらく無理でしょう(traitを単なるインターフェースとしてJava側でimplementsすることはたぶんできる)。
静的なtrait実装
クラス定義時にトレイトを(インターフェースのように)implementsします。それでだいたい期待通りに動作するでしょう。
実行時のtrait実装
Groovyのtraitは、実行時にそれを実装したオブジェクトを作り出すことができます。Scalaも表面上似たことができるのですが、ここはGroovyとScalaで考え方が一番違うところです。
Scalaの場合を参考に
Scalaでtraitをnew時に実装するには、new..with構文を使用します。この構文は無名内部クラス構文によるインスタンスnewの拡張と言えましょう。無名内部クラスのように、内部的にクラスを生成した上でそのインスタンスを作るのです。Javaの無名内部クラスによるnewではできないこととして、複数のtraitを実装(with)する、対象クラスのサブクラスである無名内部クラスのインスタンスを生成します。これは完全に静的なものです。
たとえば、Xがクラス、Tがtraitだとしたとき
var x:X = new X() with T
であれば、xはXを継承したクラスのインスタンスであり、同時にトレイトTを継承(Scala的にはmixin)したインスタンスです。帰結として、finalクラスにはtraitを実装させることはできません。XがfinalならXのサブクラスが作れないからです。
Groovyでの実行時トレイト実装
Groovyでは、newと独立したタイミングで、既存の任意のインスタンスに対して、traitを実装した新規のプロキシインスタンス*3を作成します。
def x = new X() as T
こうです。トレイトが複数の時はこう。
def x = new X().withTrait(T1,T2)
new Xしてはいますが、そのインスタンスに対するメソッド呼び出しです。だから上はこうも書けます。
def tmp = new X() def x = tmp as T
def tmp = new X() def x = tmp.withTrait(T1,T2)
xはトレイトであるTやT1,T2を実装する、実行時に生成される動的プロキシのクラスのインスタンスです。Scalaとの重要な違いとして、このときのtmpとxはインスタンスが別で、かつxはXのサブクラスのインスタンスではない*4ということです。xはtmpに対するプロキシで、インスタンスのライフサイクルが違うのです。一つのtmpに対して複数回asやwithTraitで複数のプロキシを得ることもできるでしょう。
構文上の類似性があるので混同してしまうかもしれませんが、Scalaのnew時のtrait実装が無名クラス構文によるnewの拡張的な静的なものであるのに対して、Groovyの実行時trait実装はデコレータの生成であると言えます。つまり全然違います。traitの定番(?)の用途であろうDCIへの適用、つまりtraitをロールとして使用する際においては、Groovyの動作もできた方が親和性が高いとワシは思います。
Stringなどのfinalクラスにtraitを注入できる、という点も結果的な差異になります。まあ本当に注入したいのか、というのは置いておいて、ですが*5。
なお、proxyから元のオブジェクトのproxyTargetというプロパティを取得できます(GROOVY-6692とGROOVY-6695)。
落穂拾い
Groovyのtraitは、metaClass.mixinメソッドの上位互換*6的な代替であると見ることもできるかもしれません。metaClassは静的Groovy(@TypeChecked,@CompileStatic)配下では使えませんが、traitは使えるので、静的型チェックに親和性が高いバージョンのmixinと見ることができるかもしれません。さらに憶測ですが、traitの実行時実装の動作で奇妙にも思えるところは、metaClass.mixinのユースケースをカバーするためにそうなっているのかもしれません。
とりあえずおしまい。
*1:たぶん。Scalaは良く知らないので間違いがありましたらご指摘をお願いします。
*2:実際は思い切り見えるがw
*3:この機能は実はインターフェースに関してもともと従来のGroovyにある。「"String" as Runnable」とかやれる!!!。
*4:Groovy 2.3beta1,2では、xに対するメソッドコールはx的にmethodMissingなものについてはtmpに転送されます。そういうディスパッチを行なう「proxy」なのです。しかしXのインスタンスではなく代入互換ではない、さらにDGM非対応とか、mehodMissingなのでXよりもObjectのメソッドequals,hashCodeなどが優先されるとか、静的型チェックには対応できないとか、初学者には混乱を招き得る点がある気もする。
*5:DGMや拡張メソッド、metaClassによるメソッド注入では状態が単純には保持できないので意味あるかといえば意味はある。
Java VM上の言語の覇者を決める(但しJava以外)スクリプトボウルの履歴
米国開催のJavaOneカンファレンスで恒例の人気セッションとなっている「スクリプト・ボウル」というのがあります。Java VM上で動作する言語同士のガチ勝負で、コード例とか、技術力とかいろいろな側面からパネルセッションでバトルして、その年勝者を決める、というものです。
自分では残念ながら直接見たことはないので想像ですが、「朝まで生テレビ」で言語バトルするようなものです。違うか。
エンターテイメント要素も多々あるでしょうし、人気とか「情熱」みたいなのも評価されるかもしれないし、コミュニティの「動員力」とかの要素もひょっとしたらあるかもしれませんね。そういうものも含めて、おもしろい勝負なのではないかと思います。もちろん技術者同士でやってるので、技術的なおもしろみとかもあるでしょう。プレゼンのうまさとかもあるでしょう。
んでその過去の結果をまとめてみました。
| 年 | 候補 | 結果 |
|---|---|---|
| 2008 | Scala,Groovy,JRuby,Jython | JRuby優勝 リンク |
| 2009 | Scala,Groovy,JRuby,Jython,Clojure | Groovy優勝 リンク |
| 2010 | Scala,Groovy,JRuby,Clojure | Groovy優勝 リンク |
| 2011 | Scala,Groovy,JRuby | ScalaとGroovyが同位優勝 リンク*1 |
| 2012 | Scala,Groovy,JRuby,Clojure | Scalaが優勝 リンク |
| 2013 | Scala,Groovy,Nashorn,Clojure | Groovyが優勝 リンク |
圧倒的じゃないか!!
とか言ってみる。
少なくとも皆勤賞ではある。
Grails 2.x脆弱性情報(WEB-INF配下が読みとられる)
脆弱性情報のアナウンスがでています。
http://cxsecurity.com/issue/WLB-2014020172
Grails 2.xのリソースプラグインのデフォルト値が問題があって、リソースプラグインを使っている場合(外してない場合)、WEB-INF配下のクラスファイル群などが第三者に読みとられてしまうという結構シリアスな問題です。2.3.6へのアップグレードもしくは設定変更で対処できるとのことです。
あてはまる方はご注意を。
まだ以下には出てませんね。
http://www.cvedetails.com/product/23317/Springsource-Grails.html?vendor_id=9664
Hindley-Milner型推論アルゴリズムをGroovyで書いてみた
こないだ「Haskellのforallについて理解したことを書いておく(ランクN多相限定)」の記事を書いたときにHindley-Milner型推論アルゴリズム*1を調査するにあたって、こちらにある「Scala by Example」の16章にあるScalaでの実装例をGroovyに書きなおしたので晒しておきます。
以下のような型検査・推論ができます。実行はできません。
def listLenTest = LetRec('len', Lam('xs', App(App(App(Var('if'), App(Var('isEmpty'), Var('xs'))), Var('zero')), App(Var('succ'), App(Var('len'), App(Var('tail'), Var('xs')))) )), App(Var('len'), App( App(Var('cons'), Var('zero')), Var('nil')) ) ); assert listLenTest.toString() == 'letrec len = λ xs . (((if (isEmpty xs)) zero) (succ (len (tail xs)))) in (len ((cons zero) nil))' assert typeInfer.showType(listLenTest) == "Int[]"
型理論としてのHMを理論的に(型付ラムダ計算の定理の集合として)理解して実装しているわけではないのですが、先の「Scala By Example」の著者はScala開発者にしてJava Genericsの開発者、著名なる型理論学者Martin Odersky先生様その人ですので、プログラムの動作としてはまあ間違いはないと思っています。
コードから読み取ったことについて、多数のコメントを追記してあります。また、テストコードも追加したフルバージョンはこちらのgistにのせました。
Hindley-Milner型推論の特徴は、
- 双方向性。左辺・右辺の型、仮引数と実引数、宣言の型と使用側が期待する型、リターンしている型と返り値宣言の型、など、どっちかが決まれば、どっちかが決まるのだが、HMでは前後関係も関係なく、双方向で決まる。ここはScalaとかJava7/8とかGroovyの「型推論」と大きく異なる*2。
- 上の結果でもあるが、明示的な型宣言が(多くの場合?)不要*3。リテラルの型さえ決まっていれば、波及して型が決まる。矛盾があれば、エラーになる。字面上、明示された型指定が全く無いのに、例外無くすべて宣言されているのと同じように扱われる。もし決まらなければ(「\a->a」など)、自動的に多相型になる。
- 多相型に対応。つまり以下のコードはGenericsに対応している。こんな簡潔なコードなのに!!
- 多相型の解決と型推論の統合。つまり「型推論の開始時に未知の型」は、「多相型の型変数」と同じ枠組みで扱われて解決しようとする。
- 多相型の解決は識別子の使用を契機とするが、let変数とlambda変数では多相型解決についての意味上の違いがある。詳細はコメント参照。
でしょうかね。
Hindleyによって論文が書かれたのが1969年とのこと。なんかもう。
で、Groovy 2.1のカスタムタイプチェッカとしてHMを実装してみる野望(ゴゴゴゴ)*4
import groovy.transform.* import static TypeInfer.typeInfer @InheritConstructors class TypeError extends Exception {} /** * 構文木や式木をnewキーワード無しでオブジェクトを生成するために、 * @Newify AST変換を適用するアノテーション@ApplyNewifyを定義する。 * @AnnotationCollectorは、Groovyの合成アノテーション作成機能。 * [annotations]* @AnnocationCollector @interface 新規アノテーション {} * で、[annotations]*を指定したのと等価な新規アノテーションを作成する。 */ @Newify([Var,Lam,App,Let,LetRec,Tyvar,Arrow,Tycon]) @AnnotationCollector @interface ApplyNewify {} /** * Termおよびそのサブクラスによって構文木を構成する項を定義する。 * 項とは以下のいずれか。 * - 変数(Var) * - λ抽象(Lambda) * - 関数適用(App) * - let式(Let) * - letrec式(LetRec) * @Immutable AST変換を適用するとTupleConstructorと同様に、 * メンバーを引数で初期化するコンストラクタが生成される。 */ interface Term {} @Immutable class Var implements Term { String x @Override String toString(){ x } } @Immutable class Lam implements Term { String x; Term e @Override String toString(){ "λ $x . $e" } } @Immutable class App implements Term { Term f; Term e @Override String toString(){ "($f $e)" } } @Immutable class Let implements Term { String x; Term e; Term f @Override String toString(){ "let $x = $e in $f" } } @Immutable class LetRec implements Term { String x; Term e; Term f @Override String toString(){ "letrec $x = $e in $f" } } /** * Typeおよびそのサブクラスによって式木の構成要素を定義する。 * 型とは以下のいずれか。 * - 型変数(Tyvar) * - 関数型(Arrow) * - 型コンストラクタ呼び出し(Tycon)(具体型) * 型変数を含む型を多相型と呼ぶ。 */ interface Type {} @Immutable class Tyvar implements Type { String a @Override String toString(){ a } } @Immutable class Arrow implements Type { Type t1; Type t2 @Override String toString(){ "($t1 -> $t2)" } } @Immutable class Tycon implements Type { String k; List<Type> ts = [] @Override String toString(){ k + "[${ts.join(',')}]" } } /** * Substは「型に含まれる型変数の置換処理」を表わす。 * Subst represent a step of substitution of type variables of polymorphic type. * * Substはcallメソッドが定義されているので、Subst(のサブクラス)のイ * ンスタンスに対して関数のように呼び出すことができる(Groovyの機能)。 * 例えばx = new Subst(); x(..)と呼べるということ。 * 2種類の引数の型に対してcallが定義されている。 * * - call(Type) * 型中に含まれる型変数を置換する。 * - call(Env) * Envに含まれるすべての型スキーマに含まれる型変数を置換したEnvを返す。 * * 実装機構としては、Substのサブクラスのインスタンス1つは、「Innerクラ * ス→内部クラスを含むOuterクラスのインスタンス」、それをまた含む * Outerクラス…というチェインを構成する。そのチェインは複数の置換処理 * を連鎖である。callはOuterクラスのcallを呼び、という再帰処理が行なわ * れるので、複数の置換が適用できる。Innerクラスのインスタンスを作成す * るには、extendを呼ぶ。 */ @ApplyNewify abstract class Subst { /** * 指定した型変数の置換結果を返す。 * SubstのOuter/Innerクラス関係から構成されるチェインを辿って探す。 */ protected abstract Type lookup(Tyvar x) abstract String toString() /** * 型Type t中に含まれる型変数を置換した結果の型を返す。 * 型に含まれる型変数(つまり多相型の型変数)の変数を、変化しなく * なるまでひたすら置換する。置換の結果がさらに置換可能であれば、 * 置換がなされなくなるまで置換を繰り返す。(循環参照の対処はさ * れてないので現実装は置換がループしてないことが前提)。 */ Type call(Type t) { switch (t) { case Tyvar: def u = lookup(t); return (t == u) ? t : call(u) // TODO: this code could throw stack overflow in the case of cyclick substitution. case Arrow: return Arrow(call(t.t1), call(t.t2)) case Tycon: return Tycon(t.k, t.ts.collect{owner.call(it)}) } } /** * 環境Env eに含まれるすべての型スキーマに含まれる型変数を置換した * Envを返す。 */ Env call(Env env) { env.collectEntries { String x, TypeScheme ts -> // assumes tyvars don't occur in this substitution def tmp = new TypeScheme(ts.tyvars, owner.call(ts.tpe)) [x, tmp] } } /** * Innerクラスのインスタンスを生成する操作がextend()であり、「1つの * 型変数を一つの型へ置換」に対応するインスタンス1つを返す。ただし * extendで生成されたインスタンスは、extendを呼び出した元のオブジェ * クト(extendにとってのthisオブジェクト) =Outerクラスのインスタン * スとチェインしており、さらにcallにおいて、Outerクラスを呼び出し * て実行した置換の結果に対して追加的に置換を行うので、元の置換に対 * して「拡張された置換」になる。 */ Subst extend(Tyvar x, Type t) { new Subst() { Type lookup(Tyvar y) { if (x == y) t else Subst.this.lookup(y) } String toString() { Subst.this.toString() + "\n$x = $t" } } } /** * 初期値としての空の置換を返す。 * 任意のSubstインスタンスについて、OuterクラスのOuterクラスの… * という連鎖の最終端となる。 */ static final Subst emptySubst = new Subst() { Type lookup(Tyvar t) { t } String toString() { "(empty)" } } } /** * TypeSchemeは、型抽象(∀X.T)を表わす。 * 型抽象とは、「型引数」を引数に取り、型変数を含むテンプレートのよう * なものを本体とするような、λ式のようなもの。 * * TypeSchemeはTypeを継承していない。その結果、Typeの構造の途中に * TypeSchemeが表われることもない。 * * Haskellの「forall.」は型スキーマ(型抽象)に対応しているが、このHMアル * ゴリズムでは型スキーマ(抽象)はトップレベルの環境における識別子に直接 * 結びつく形でしか存在しない。つまりランクN多相を許していない。 * * もしTypeSchemeが型の一種であり、型構造の任意の部分に表われ得るなら * (つまりmgu()やtp()の型推定の解決対象の型コンストラクタなら)、ランク * N多相が実現されることになる。 */ @Canonical class TypeScheme { /** * tyvarsは型抽象において全称量化された型変数の集合を表す。 * tyvars are set of universally quantified types in the type scheme. * * tyvarsは「その外側に対して名前が衝突しないことの保証」を持った型 * 変数である。なぜなら型スキーマの使用に際してnewInstance()するこ * とでtpe中でのtyvars変数の使用がリネームされるからである。 * * 具体的には、プログラム中にVar(x)の形で識別子xが使用されるとき、 * 識別子xの型を得るために、環境に登録された「xに対応する型スキーマ」 * を取得した上で、Type型に変換する処理(TypeScheme.newInstance())が * 行なわれる。newInstance()は、type中のtyvarsと同じ名前を持った変数 * を、すべて重ならない新規の名前にリネーム置換したバージョンのtpe * を返す。 */ List<Tyvar> tyvars /** * 型のテンプレートを表わす。全称量化されている型変数と同じ型変数を * 含んでいれば、その型変数は、型スキーマがインスタンス化されるとき * に重ならない別名に置換される。 */ Type tpe /** * 型スキーマ(型抽象)を型に具体化する操作。 * * newInstance: TypeSchema → Type * * ちなみにgen()は反対に型から型スキーマを生み出す操作である。 * * gen: Type → TypeSchema * * newInstance()は、全称限量指定された変数およびそれに束縛された変 * 数(つまりフリー型変数を除いた全ての型変数)の使用を、新規の変数名 * にリネームする。この操作の結果は、環境には左右されず、 * TypeSchemeインスタンスのみの情報によって確定される。(変数名のシー * ドとなるtypeInfer.nの値には依存するが) * * newInstance()の結果として得られる型には全称限量で指定されていた * 型変数は含まれない。たとえば、型スキーマ * * TypeSchema s = ∀ a,b . (a,b型を含む型) * * に対して、newInstanceした結果は、 * * s.newInstance() = (a',b'型を含む型) * * であり、a,bは、a'b'に置換されるので、結果の型には決して現われな * い。 */ Type newInstance() { tyvars.inject(Subst.emptySubst){ s, tv -> s.extend(tv, TypeInfer.instance.newTyvar())} (tpe) } String toString() { "∀ (${tyvars.join(',')}) . ($tpe)" } } /** * 環境Envは、プログラムのある位置における、識別子と型情報(型スキー * マ)の対応表である。 * Env is map of identifier to type schema. * 環境Envは、意味的には型変数を含む制約の集合と見做すことができる。 * Env can be regarded as set of constraints of relationships concerning * types include type variables. So HM type checker is constraints solver for it. * 環境は、tp()が解くべき、型方程式の制約条件を表現している。 * Env: 「プログラム中の識別子→型スキーマ」の対応の集合 * * ちなみに、Substもある種の対応表であるが、型変数の書き換えルールの * 集合。 * * Subst: 「型変数→型(型変数|Arrow|Tycon)」という書き換え規則の集合 * * なお、明かにこの実装は空間効率が悪い。Scalaではタプルのリスト(連想リ * スト)で実現されていたところをGroovy化する際に、安易にMapにしてコピー * して受け渡すようにしたが、実用的には連想リストにすべき。 */ @InheritConstructors @ApplyNewify class Env extends LinkedHashMap<String, TypeScheme> { } /** * TypeInferはHM型推論の全体を含む。Scalaではオブジェクトだったので、 * @Singletonとして定義してある。サービスメソッドを呼び出すための静的 * import可能な変数として、static typeInferを容易してある。 * 型チェックの全体の流れは、 * * showType -> predefinedEnv * -> typeOf -> tp -> mgu * * である。 */ @ApplyNewify @Singleton class TypeInfer { int n = 0 def reset() { n = 0 } /** * 名前が重ならない新規の型変数を作成する。 */ Type newTyvar() { Tyvar("a${n++}") } /** * 環境中にで定義された識別子xに対応する型スキーマを取得する。 */ TypeScheme lookup(Env e, String x) { return e.get(x) } /** * 型tに含まれているすべての型変数の集合(A)から、この環境に登録され * ているすべての型スキーマの「全称量化に関するフリー型変数の集合 * (※1)」=(B)を除外したもの((A)-(B))を全称量化することで型スキーマ * を生成する。 * * (※1)λx.yのとき変数xに束縛されていることを「λ束縛」と呼び、 * 「λ束縛されていない変数」をフリー変数と呼ぶが、それと同様に、 * 型変数に関する∀y...のとき型変数yに束縛されていることを「全 * 称量化束縛」と呼び、「全称量化束縛」されていない型変数を「全 * 称量化に関するフリー型変数」とする(ここで作った言葉)。 * * 環境において「全称量化に関するフリー型変数」が発生するケースとい * うのは、具体的にはラムダ式 * * λ x . y * * において、識別子xに対応する型は、新規の型変数として環境に登録さ * れ、そのもとでyが型推論されるが、y解析中でのxの登場はスキーマ内 * で全称量化されていない、という状態である。 */ TypeScheme gen(Env env, Type t) { new TypeScheme(tyvars(t) - tyvars(env), t) } /** * 型に対するtyvars()は、指定した型Type t中に含まれる型変数のリスト * を返す。 */ List<Tyvar> tyvars(Type t) { switch (t) { case Tyvar: return [t] case Arrow: return tyvars(t.t1) + tyvars(t.t2) // 型コンストラクタ T[a,b]のとき、Tは型変数ではない。 case Tycon: return t.ts.inject([]) { List<Tyvar> tvs, Type elem -> tvs + tyvars(elem) } } } /** * 型スキーマに対するtyvars()は、指定した型スキーマTypeSchema tsの * 型テンプレート(ts.tpe)が使用している型変数から、全称量化された変 * 数(ts.tyvars)を除外したものを返す。これは、何かというと、型スキー * マの型テンプレート(TypeSchema.tpe)が含む「全称量化に関するフリー * 型変数)の集合」である。 */ List<Tyvar> tyvars(TypeScheme ts) { tyvars(ts.tpe) - ts.tyvars } /** * 環境Envに対するtyvarsは、その環境に登録されているすべての型スキー * マに対するtvarsの値全体を返す。 * つまり、環境全体が含む「全称量化に関するフリー変数の集合」を返す。 */ List<Tyvar> tyvars(Env env) { env.values().inject([]){ acc, it -> acc+tyvars(it)} } /** * 型tと型uのユニフィケーション。 * 型tと型uに対してs'(t) s'(u)が一致するような、sを拡張した置換s' * を返す。 */ Subst mgu(Type t, Type u, Subst s) { def (st, su) = [s(t), s(u)] if (st instanceof Tyvar && su instanceof Tyvar && st.a == su.a) { return s } // 等しい型変数 else if (st instanceof Tyvar) { return s.extend(st, su) } // 左辺が型変数 else if (su instanceof Tyvar) { return mgu(u, t, s) } // 右辺が型変数 else if (st instanceof Arrow && su instanceof Arrow) { // Arrow同士 return mgu(su.t1, st.t1, mgu(su.t2, st.t2, s)) } else if (st instanceof Tycon && su instanceof Tycon && st.k == su.k) { return zip(st.ts, su.ts).inject(s) { acc, it -> mgu(it[0], it[1], acc) } } throw new TypeError("cannot unify $st with $su") } /** * 二つのリストxs=[x1,x2,x3..], ys=[y1,y2,y3]のとき、 * [[x1,y1],[x2,y2],[x3,y3]..]を返す。 */ static zip(xs, ys) { if (xs.size() != ys.size()) { throw new TypeError("cannot unify $xs with $ys, number of type arguments are different") } Iterator itor = ys.iterator() xs.collect { [it, itor.next()] } } /** * エラーメッセージに含めるための、処理中の項への参照。 */ Term current = null /** * envのもとで、eの型がt型に一致するためのsを拡張した置換s'を返す。 * 数式で書くと以下のとおり。 * * s'(env) ├ ∈ e:s'(t) * * つまり、型の間の関係制約式(型変数を含む)の集合envのもとで、「s'(env)の * 型はs'(t)である」を満たすような、sを拡張した置換s'を値を返す。 */ Subst tp(Env env, Term e, Type t, Subst s) { current = e switch (e) { case Var: // 変数参照eの型は、eの識別子e.xとして登録された型スキーマを実体化(全称量 // 化された変数のリネーム)をした型である。 TypeScheme u = lookup(env, e.x) if (u == null) throw new TypeError("undefined: "+e.x) return mgu(u.newInstance(), t, s) case Lam: // λで束縛される変数とletで束縛される変数の扱いの違いにつ // いて。 // 変数(識別子)は、HMの多相型の解決において、キーとなる存在 // である。型スキーマは変数(識別子)にのみ結びつく。変数を介 // 在して得た型スキーマを基軸に、インスタンス化=全称量化=型 // 変数置換が実行される。 // // 識別子x,yに束縛される式が多相型であるとき、型変数の解決 // の扱いに関して両者には違いがある。 // // λx.eの場合、xに対応して環境に登録されるのは、xの型を表 // わす新規の型変数(a = newTyvar())を型テンプレートとする型 // スキーマ(型抽象)であり、かつaについては全称限量されない。 // つまり「全称量化に関するフリー型変数を含む型スキーマ」に // なっている。 // // let y=e1 in e2の場合、yに対応して環境に登録されるのは、 // e1の型を元にして、e1中の型変数群 // // 「e1.tyvars-tyvars(e1.e)」…(*) // // を全称限量した型スキーマ(型抽象)。例えば「new // TypeScheme(tyvars(e1), e1)」が登録される。 // なお、(*)における、tyvars(e1.e)は、e1中のフリー型変数だ // が、これが生じるのは、λ束縛の本体の型検査の場合である。 // つまり // // \ x -> let y=e1 in e2 // // のように、λ本体の中にlet式が出現するときに、let束縛され // る識別子yのために登録される型スキーマでは、xに対応する型 // スキーマで使用されている型変数がフリーなので全称限量対象 // から除外される。 // // [ここでのλとletの違いがどのような動作の違いとして現われるか?] // // Haskellで確認する。 // // ghci> let x=length in x [1,2,3]+x "abc" // 6 // ghci> (\ x -> x [1,2,3]+x "abc") length // <interactive>:5:12: // No instance for (Num Char) // arising from the literal `1' // Possible fix: add an instance declaration for (Num Char) // In the expression: 1 // In the first argument of `x', namely `[1, 2, 3]' // In the first argument of `(+)', namely `x [1, 2, 3]' // // letでのxに束縛された多相関数lengthの型(a->a)における型変 // 数aは全称限量される(Haskell流に書くとforall a.a->a)ので、 // 「x [1,2,3]」と「x "abc"」それぞれにおけるxの出現それぞ // れでaがリネームされ(1回目はa',二回目はa''など)、別の型変 // 数扱いになる。そのため、a'とa''がそれぞれのIntとCharに実 // 体化されても、型エラーにならない。 // // λの場合、xの型は全称限量されない(a->a)なので、a=Intと // a=Charの型制約が解決できず型エラーとなる。この動作はテス // トケースtestTpLamP2()、testTpLetP1() で確認する。 def (Tyvar a, Tyvar b) = [newTyvar(), newTyvar()] Subst s1 = mgu(t, Arrow(a, b), s) return tp(new Env(env)+[(e.x):new TypeScheme([], a)], e.e, b, s1) case App: Tyvar a = newTyvar() Subst s1 = tp(env, e.f, Arrow(a, t), s) return tp(env, e.e, a, s1) case Let: // λ x ...で束縛される変数とlet x= ..in..で束縛され // る変数の違いについては前述の通り。 Tyvar a = newTyvar() Subst s1 = tp(env, e.e, a, s) return tp(new Env(env) + [(e.x):gen(s1(env), s1(a))], e.f, t, s1) case LetRec: def (Tyvar a, Tyvar b) = [newTyvar(), newTyvar()] def s1 = tp(new Env(env) + [(e.x):new TypeScheme([], a)], e.e, b, s) def s2 = mgu(a, b, s1) return tp(new Env(env) + [(e.x):gen(s2(env), s2(a))], e.f, t, s2) } } /** * 環境envにおいてTerm eの型として推定される型を返す。 */ Type typeOf(Env env, Term e) { def a = newTyvar() tp(env, e, a, Subst.emptySubst)(a) } /** * 既定義の識別子(処理系の組み込み関数もしくはライブラリ関数を想定)を * いくつか定義した型環境を返す。型のみの情報でありそれらに対する構 * 文木の情報はない。 */ Env predefinedEnv() { Type booleanType = Tycon("Boolean", []) Type intType = Tycon("Int", []) Closure<Type> listType = { Type t -> Tycon("List", [t]) } Closure<TypeScheme> gen = { Type t -> gen(new Env(), t) } def a = newTyvar() return new Env(['true':gen(booleanType), 'false':gen(booleanType), 'if':gen(Arrow(booleanType, Arrow(a, Arrow(a, a)))), 'zero':gen(intType), 'succ':gen(Arrow(intType, intType)), 'nil':gen(listType(a)), 'cons':gen(Arrow(a, Arrow(listType(a), listType(a)))), 'isEmpty':gen(Arrow(listType(a), booleanType)), 'head':gen(Arrow(listType(a), a)), 'tail':gen(Arrow(listType(a), listType(a))), 'fix':gen(Arrow(Arrow(a, a), a))]) } /** * 項の型を返す。 */ String showType(Term e) { try { typeOf(predefinedEnv(), e).toString() } catch (TypeError ex) { "\n cannot type: $current"+ "\n reason: ${ex.message}" } } /** * @Singleton宣言したクラスのシングルトンはTypeInfer.instanceで保持 * されており、クラス外からも取得できる。しかし、 * 「TypeInfer.instance」が少し冗長なのと、Scala版に合せるため、シ * ングルトンを以下で定義する静的変数TypeInfer.typeInferで取得でき * るようにする。ただしSingletonの初期化タイミングの都合上か、遅延 * 設定のAST変換@Lazyを指定しないとうまくいかないようである。 */ @Lazy static typeInfer = TypeInfer.instance }
テストコードつきはこちら。
上記は元コード同様関数型っぽい作りになってる(Substによる実現とか)が、書き換えを許す前提でならもっと簡潔になりそう。型変数の一意性保証のために「型変数名」とかの置き換えにたよらず、型変数オブジェクトを単にシェアすればいいんじゃないかな…。
HaskellにおけるIOモナドとSTモナドの関係
HaskellにおけるIOモナド(IO a型)とSTモナド(ST s a型)について整理してみました。
IOの定義から知るST
IOモナドの考え方についての原論文に相当する「Lazy Functional State Threads」においては、IOの定義は
newtype IO a = ST RealWorld a
のようにST型を直接使用して定義されるものとして説明されています。ただ、「IO inside」によれば、GHCのライブラリ実装においてIO aの定義は
newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))
だそうで直接STを使ってはいません。後者のは正格タプル非ボックス化タプルを使ってます(知らん!)。
IOモナドとSTモナドとの機能的関係
直接的な利用関係があるかどうかはともかく、記事「第7回 入出力と遅延評価の間を取り持つIOモナド - ITpro」からすると
STモナドは、「状態」を参照型などのより効率の良い仕組みで利用できるようにするため、IOモナドと同じ技術を使って実装されています
とのことです。
まず、IOモナドの機能を整理しよう
上記を踏まえて私の理解した限りでは、まずIOモナドには以下(1),(2)の2つの役割りがあります。
- (1) 副作用コードを分離する
- (1-1)純粋コードから副作用コードを呼べなくする。
- 静的型チェックおよびランタイムがmainを経由してからしかIOアクションを起動できないことによって
- (1-2)更新状態を外に持ち出せなくする。
- 静的型(多相型)チェックでコンパイル時に保証(ランクN多相によって)。ただし、IOでは(1-1)があるので(1-2)は試みることもできず、IO利用者からは(1-1)と一体的に認識される役割りである。
- (1-1)純粋コードから副作用コードを呼べなくする。
- 副作用は以下の二種類に分けて考えることができるが、実行順序の保証はいずれに対しても必須。
- (2-1)外部から観測可能なもの→入出力
- (2-2)外部から観測不能なもの→変数更新(IORef,newIORef,...)
おさらいでした。
そして、STモナドは?
STモナドは、機能的に前述の青字の(1-2)と(2-2)を得るものです。つまり、入出力を行なわず、変数更新(STRef,newSTRef..)だけを行なう用途に使用できます。STモナドには、入出力を行なえない、という制限がありますが、実行順序は保証されるので変数更新はでき、さらに有用なことに(1-1),(2-1)が無いので純粋関数からも呼べるという利点が得られます。
もうちょっと詳しく言うと、
- 「変数更新」のみを実行するコードは、そのコードがもはやコードの見た目としても実質としても状態更新バリバリの命令型(=評価順序が結果に影響を与える)であったとしても、呼び出し側から見たときの参照透過性さえ保てれば、純粋コードから呼んでも大丈夫だ問題ない(呼ぶ側のコードは純粋なので、呼ばれるかどうか、呼ばれる順序などはわからないが、一旦呼ばれたならその呼ばれるコード内なら順序が保たれる)。なぜなら、プログラムの外部から見て検知不能だからである。プログラムの最適化と同じである。ばれなきゃイカサマじゃないんだぜby承太郎である。
- しかし「入出力(=プログラム外とのインタラクション)」を行うコードは、たとえそれが「呼び出し側から見て参照透過(引数のみによって返り値が定まる)」としても、純粋コードから呼ばれるわけにはいかない。純粋コード自身が遅延評価によって、呼ばれるかよばれないか、あるいは呼び出し順序について保証がないからで、その状況下では外部から見ておかしなこと(起きて欲しい副作用が起きない・順序が変、など)が検出でき都合が悪いからである*1。だから純粋コードのような恐ろしいものから呼ばれないようにIOで守り、mainにつらなる「見えないバトン*2」の唯一の連鎖(the chain)に繋げる必要がある。
- IOは、入出力も変数更新も両方行なうことができる。しかし、入出力を行なわず、変数更新だけを行うコードをIOにするのは、純粋コードから呼べなくなるので嫌である。STモナドは、その目的のためにある。STモナドは入出力はできないが変数更新は行うことができる(ただし更新中の状態を外に持ち出せないように工夫がしてある)。そして、純粋コードからも(IOからも)任意に呼び出すことができる。
表にすると
| 入出力 | 起動方法 | 純粋関数から | 変数更新 | 順序の保証 | 相互に呼べるか | |
|---|---|---|---|---|---|---|
| STモナド | できない | runST | 呼べる | できる | ある | IOを呼べない(純粋関数と同様) |
| IOモナド | できる | mainで起動 | 呼べない | できる | ある | ST,State含め純粋関数を呼べる |
| Stateモナド | できない | runState | 呼べる | できない | ある | IOを呼べない(純粋関数と同様) |
まとめ
Haskellのforallについて理解したことを書いておく(ランクN多相限定)。
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
- 型検査の過程において、プログラム字面上の「識別子の出現」が型スキーマのインスタンス化のタイミングである。なおインスタンス化一発ですべての型変数が消去できるわけではない。構文木をツリーとして再帰的に辿るhindley-milner型検査過程の各ステップで、型変数を媒介として双方向的・全体的に型がきまっていく*7。こんなことが可能なのはある意味驚きであるが、決まるそうなのである。これがHindley-milnerの凄いところである。処理対象プログラム中に識別子が現われたら、環境から型スキーマを引っぱってきてインスタンス化して、構文木構造(関数適用、let、lambda..)ごとに決められたルールで双方向パターンマッチ(ユニフィケーション、単一化)して型を決めていく。
ちなみに型検査器を外部から見て一言で言うと
- 外部から見ると、hindley-milner型検査器は、型変数を含んだ連立程式を解く、制約問題ソルバとみなせる。
ランク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
これは型エラーになる。なぜならf[Int]、f[ [Char] ]というfの出現2つにそれぞれ対応してインスタンス化されることで生成された、f::[Int]->Intとf::[ [ Char ] ] -> Intというボトムアップで定まる2つの型制約を、引数としての識別子fの型が同時に満せないからである。
func f = f [1,2,3] + f["a","b","c"]
ランクN多相の意義と動作例
名前が悪いぞforall
あとは非生産的な話。
- プログラミング言語としてのHakellにおける、forallというキーワードで起動される言語機構を理解するのに、全称量化を理解する必要はないし形式論理学の知識は不要である。「全称量化」という単語を知る必要すら一切ない。それは理解に寄与しない。ていうか理解の妨げになるだけだッ。名称としてそれしかないので「全称量化子」とか「全称量化された」とか呼ぶしかないので、しょうがない面もあるのだろうが、ミスリーディングなだけである。forallというキーワードから「all(全ての)」という含意を読みとる必要すらない。必要があるってのなら値に関して同型であるλについてもどういう意味でallなのか、allを付けないのかプログラミングレベルでの説明を聞かせてほしい。 ∀が型抽象の型表記で慣例的に使われてるのを敬意を表してなのか論理学者は慣れてるからなのか、結果的には無批判に導入しただけだろ、っていう。最終的にはカリー・ハワード同型対応で、そういう方面に応用できるのだとは思うが、Haskellをプログラミングのみに使いたいプログラマにとっては不要なことである。迷惑なことである。
型システム入門 −プログラミング言語と型の理論−
posted with amazlet at 14.01.23
*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拡張でどう実装しているかは不明。「私だったらそう実装したい」というレベルの話である。
