JavaでMaybeを説明した以下の記事について, id:tozimaさんと某所*1でやりとりしていたら, 有益な話が出てきたのではないか, ということになったので, 紹介.
基本的にやりとりをそのまま*2抜粋したものに, 適宜補足を加えていきます.
発端
2012-06-29 04:29こんな記事があった。
Java の語彙で Maybe を説明してみる - ぐるぐる~
直和型のエンコーディングである、
でMaybeモナドを説明している、まっとうな記事です。気になったのは、上のエンコーディングを Java の上でやって、なにか変なことが起きないのかということ。例えば記事中では、
*3
みたいなことが、Javaでは禁止できない、ってことについて触れています。この他には変なことはおきないんでしょうか?僕には全然Java的な言語への直感がないので教えてください!!!
「......みたいなことが、Javaでは禁止できない、ってことについて触れています」というのは元記事の
just やら Just のコンストラクタやらに null を渡すとダメという点で、ポリモーフィズムなし版より残念なことになっていますが......
Java の語彙で Maybe を説明してみる - ぐるぐる~
という部分のことです.
nullの呪縛
2012-07-01 02:05になってしまうのは, そもそもだからだと思うので, このことがになってしまうこと以外に(安全性に関して)別の問題を引き起こしたりしないのか? という質問だと思います.
記事を読んでまず不安に思ったのは,
Maybe
自体もふつうのクラスなので,Maybe
を返すメソッドは実はふつうにnull
を返せてしまうこと. そうするとmatch
の呼出しがぬるぽで落ちる. これはかなり致命的だと思う.もう一つ不安に思ったのは,
ifJust
がnull
を返す場合. これもJust.match
で返り値をチェックして,null
を返そうとしたら例外とかでもいいのかも知れないけど, なんか結局例外なのかよ, という感じがしてnull
の呪縛から逃がれられなくて残念感が漂う. 一貫性のある実装としてはmatch
の返り値をMaybe
に強制するのだろうけど, 一つ目の不安と同じ理由でそれでもやっぱりnull
返せるからあんまり意味ない.
Javaにはnull
があるので(またnull
とそれ以外を型で区別できないので), 本質的に型検査によって安全性*4を保証することはできません*5.
Javaで直和型を実現?
2012-07-03 22:27それでは,
null
周り以外では大丈夫?
つまり,直和のクラスを次のように定義したとき,(構文が適当で申し訳ないけど...),∀<S, T> interface Sum { Sum<S, T> inl(e : S); Sum<S, T> inr(e : T); ∀<R> R match(f : S → R, g : T → R); }
null
さえなければ,これが期待通り直和として動くように実装できるってこと?Preservation + Canonical Form Lemma とかで期待通り動作することが示せるような気もするんだけど,FJの直感がないんで,そこんところを教えてください!
PreservationやCanonical Form Lemmaというのは, プログラミング言語を数学的に扱う上での性質の名前です. ラムダ計算と同様に, Javaのようなプログラミング言語も, 式を評価(ラムダ計算の簡約に相当)していって, もうこれ以上評価しても何も起きなくなった結果を実行結果とするという考え方を当てはめることができます.
- Preservation
- 式を評価する前後(評価結果も理論的には式の一つと捉える)で, その式に付くべき型が保存されるという性質(別名: Subject Reduction). このときの「保存される」の意味は, Javaのように部分型のある言語では「同じ型か, あるいはより具体的な型になる」というもので, たとえば
Number
型の変数を評価したら,Integer
型の値が得られた, という場合があっても, Preservationは成り立っていると見なします. - Canonical Form Lemma
- ある式を評価してもこれ以上何も起きず, その式に型が付くならば, その式は必ず特定の形をしている, という性質です. Javaの場合は, (定式化の方法にもよりますが)これ以上評価できない場合というのは, ある型のオブジェクトが得られた場合か, 例外が発生した(型の付かない例外オブジェクト*7が得られた)場合なので, 型が付いている場合はその型のオブジェクトが得られているはずだという直感が成り立ちます.
そしてFJというのはFeatherweight Javaの略で, Java(の基本的な機能に限定した極小言語)をモデル化して数学的に取り扱えるようにしたものです.
FJについての参考資料
- ソフトウェア基礎論配布資料(7) - オブジェクト計算: Featherweight Java (PDF)
- Featherweight Java: A Minimal Core Calculus for Java and GJ
- (Chapter 19)
Types and Programming Languages (The MIT Press)
- 作者:Pierce, Benjamin C.
- 発売日: 2002/01/04
- メディア: ハードカバー
Javaで直和型
ポリモーフィズムによる素直な実装
2012-07-04 14:44たぶんJava的には
abstract class Sum<S,T> { static <S,T> Sum<S,T> inl(S e){ return new Left<S,T>(e); } static <S,T> Sum<S,T> inr(T e){ return new Right<S,T>(e); } <R> R match(Func1<S,R> f, Func1<T,R> g); private static final class Left<S,T> extends Sum<S,T> { S value; Left(S e){ this.value = e; } <R> R match(Func1<S,R> f, Func1<T,R> g) { return f.apply(this.value); } } private static final class Right<S,T> extends Sum<S,T> { T value; Right(T e){ this.value = e; } <R> R match(Func1<S,R> f, Func1<T,R> g) { return g.apply(this.value); } } }と書くのだと思いますが, この場合
Sum.inl
とSum.inr
を使う限りは直和になると思います. というのは,Sum.inl
とSum.inr
は実行時の型としてLeft
かRight
しか返さず,Left
とRight
はそれぞれf
とg
を正しく呼ぶからです.Sum
が正しく直和になることは, この2つの点に関して実装にまで言及しないと(型上の話だけでは)もちろん証明できませんが,f
やg
が正しくS
やT
の値を受け取ることはPreservationから成り立つことです(詳細は後の別の形の場合の説明を見て下さい).
非常に素直なやり方で, ここを読んでいる皆さんも「このくらいは書けるぞ馬鹿にするな!」と思ったことでしょう. つまりid:tozimaさんが単にJavaに不慣れなだけだったのでしょうか? 実は, 「直和を型で表現する」という観点からすると上記のコードには欠点があります.
2012-07-04 14:44ただし
inl
とinr
を使っているかどうかわからなければ(Maybe
の例のように, ライブラリ関数が単にSum
を返すようになっているだけで, 内部でinl
やinr
を呼んでいる保証が無い場合), この限りではありません. たとえば,class Hetero<S,T> extends Sum<S,T> S value; Hetero(S e){ this.value = e; } <R> R match(Func1<S,R> f, Func1<T,R> g) { return g.apply(new T()); } }みたいなものを作って,
Sum
を返す関数が実はHetero
を返した, というときによくわからない感じになります. (細かいことを言うと, 実際にはこの例のようなことはできなくて, Javaでは型変数をnew
できない*8ので,new T()
を返すことは本当はできません. でもT
が何か具体的なもの, たとえばSum
を返すという場合には,String
に特化したバージョンのHetero
を作ることでnew String()
できてしまいます.)ただこの場合の「よくわからない感じ」というのは,
Hetero
にe
を渡した側からすればinl
相当になってほしいのにinr
みたいになっているという話であって,Sum
を返してもらう側からは全く見えないところで起こったことなので,Sum
を返してもらう側から見れば単にnew T()
がinr
されてきたと思えるだけの話で問題ないとも言えます. もちろん,Sum
が直和であるからにはLeft
とRight
以外の型であってほしくないところ, 第3のHetero
の存在を許してしまう(制限する方法が無い)という意味では直和型をきちんと実現できているとは言えません.
2012-07-07 03:25なるほど.確かに特化がありえると parametricity を失ってしまって,代数的データ型のエンコーディングにならない可能性があるわけですね.これは全然,思い付いていなかったです.
勝手なことはさせない版
2012-07-04 14:44ポリモーフィズムを使わない実装をすればもう少しstrictにできて,
final class Sum<S,T> { static final class Left<S> { S value; Left(S e){ this.value=e; } } static final class Right<T> { T value; Right(T e){ this.value=e; } } static <S,T> Sum<S,T> inl(S e){ return new Sum<S,T>(new Left<S>(e)); } static <S,T> Sum<S,T> inr(T e){ return new Sum<S,T>(new Right<T>(e)); } private Object value; private Sum(Object e){ this.value = e; } <R> R match(Func1<S,R> f, Func1<T,R> g) { if (this.value instanceof Left) { return f.apply(((Left)this.value).value); } else { return g.apply(((Right)this.value).value); } } }とすると意図通りになり, かつそれ以外のことはおおよそできないはずです.
まず,
Sum
のコンストラクタがprivate
でSum
がfinal class
なのでinl
とinr
以外からSum
のインスタンスが作られることはないと証明できます. またSum.value
はprivate
でコンストラクタでの初期化以外に値の代入は起きないので, Preservationを使うと,value
の実行時の型はinl
の場合はLeft
,inr
の場合はRight
になります. すなわち,inl
由来であることとinstanceof Left
が成立することが同値となります.inl
由来の場合はLeft
のコンストラクタに渡しているe
の値と(match
内の)this.value.value
の値が一致するので, Preservationより,this.value.value
の実行時の型はS
の部分型になります.inr
由来の場合も同様です. 従って,f
に渡されるのはinl
に渡したe
の値,g
に渡されるのはinr
に渡したe
の値であることが証明されます.
Left
とRight
を使わずにSum.value
にe
を渡すようにして,instanceof Left
の代わりにinstanceof S
としてもよさそうに思えますが, これだと, (1) 実はJavaでは型変数に対してinstanceof
できない*9, (2)T
がS
の部分型だった場合にinr
したのにf
が呼ばれる, という問題があります.
これはそこそこうまくいっていますが, instanceof
やキャストを使っている点がかなりイケてません. また, これは直和型を部分型のある言語で実現する上で避けられないことですが, 次のような注意点もあります.
2012-07-04 14:44(2)の問題に少し関連しますが, 部分型があるので,
S
とT
が部分型関係にあるとinl
とinr
のどちらでも可能という状況が発生することはあります. そのことを想定し忘れると, たとえばT
がS
の部分型のとき,f
の引数の実行時の型はT
ではないと仮定してf
を実装してしまうことになりますが, 実際にはinl
されうるので意図通りに動かないことになります.
合わせ技
2012-07-04 14:44部分型の小さな問題は残りますが, 最終的には1つ目と2つ目のやり方の合わせ技で,
final class Sum<S,T> { private interface SumI<S,T> { public <R> R match(Func1<S,R> f, Func1<T,R> g); } private static final class Left<S,T> implements SumI<S,T> { private S value; Left(S e){ this.value=e; } public <R> R match(Func1<S,R> f, Func1<T,R> g) { return f.apply(this.value); } } private static final class Right<S,T> implements SumI<S,T> { private T value; Right(T e){ this.value=e; } public <R> R match(Func1<S,R> f, Func1<T,R> g) { return g.apply(this.value); } } public static <S,T> Sum<S,T> inl(S e){ return new Sum<S,T>(new Left<S,T>(e)); } public static <S,T> Sum<S,T> inr(T e){ return new Sum<S,T>(new Right<S,T>(e)); } private SumI<S,T> sum; private Sum(SumI<S,T> sum){ this.sum=sum; } public <R> R match(Func1<S,R> f, Func1<T,R> g) { return this.sum.match(f, g); } }とすると, キャストや
instanceof
なしに, うまくいくようにできますね.
このクラスは(Java8でなくても),
public interface Func1<X,R> { R apply(X x); }
というインタフェースを用意しておけば, 実際に動かして確認できます.
2012-07-07 03:25おおよそ流れは追えたと思います.すばらしい解説をありがとう.残された課題は「証明を自力で書ききれない」という点だけだと思うので,これはいずれ勉強します.
最終的なコードでは,
SumI
,Left
,Right
の全てをprivate
にしていて,ここまで制限しないといけないんだということに驚きました.逆にここまで制限すれば SystemF の多相で言えるのような parametricity が復活させられて,一般の代数データ型(ただし型変数は covariant position にしか起きない)についても同様の理論を展開できそうですね.# 実は既にある?
FJとラムダ計算は,互いに埋め込みがあるとは言え,だいぶ違うんですね.
追記
id:keigoiさんから大変わかりやすい指摘をいただきました.
要するに JavaだとScalaでいうsealedが無いので真面目にやるなら最後の方法になるってことなのかな http://t.co/6NoDl9iU
— Keigo Imai (@keigoi) 2012年7月11日
その通りだと思います.
少し補足しておくと, この指摘に関して, Javaにそのようなものがないのは仕方ないとして, もしScalaのsealed
相当のものがあれば話が簡単で万事解決, と思う人もいるかも知れません. たしかに実用上はその通りだと思います. しかし, id:tozimaさんのもともとの意図としては, きちんと直和型が実現できていることを証明したい, ということでした. このためには今度はsealed
を組み入れた(FGJsealedというような)形式体系を定義して, その上でsealed
に関する性質を考慮した証明を行なうことになるので, private
やfinal
でどうにか頑張った場合と比べて必ずしも簡単になるわけではありません(もともとprivate
やfinal
を使っている時点で素のFJ/FGJでは扱えませんけどね).
そういうわけで, sealed
が使えるかどうかはともかく, 代数的データ型がダイレクトに入っている言語とはかなり勝手が違うという話でした.
*1:非公開なところ.
*2:一部誤字脱字等の修正と体裁を整え註をつけたり, あとは一部順番を前後させています.
*3:式に型が付くという意味. 以降「:」の意味は同じ.
*4:型の付いたプログラムがエラー(Javaの場合例外)を発生させることが無いこと.
*5:他にはたとえば(ダウン)キャストをすると例外が発生する可能性があり, また再帰呼び出しでスタックが溢れて例外が発生する場合もあるので, Javaの安全性についての理論を語る上ではこのような例外を除外するしかないので, 同様にNullPointerExceptionについては安全性の要件に入れなければ安全性は成り立つかもしれない(が, その安全性に何の意味があるのか).
*6:そもそもこの程度のことは元記事でも補足されていましたね.
*7:実際のJavaを考えるとこの表現は少し不自然かも知れません. ようするにあるオブジェクトが例外型かそれ以外かを区別するということです.
*8:これは現行のJavaではコンパイルのフェーズで型引数の情報を消去してしまっていて, 実行時には型引数として何が渡されたのかどうやっても分からないためです.
*9:これはnewの場合と同じく型消去のせいです.