Maybeに限らずJavaで直和型を実現できるか

JavaでMaybeを説明した以下の記事について, id:tozimaさんと某所*1でやりとりしていたら, 有益な話が出てきたのではないか, ということになったので, 紹介.

基本的にやりとりをそのまま*2抜粋したものに, 適宜補足を加えていきます.

発端

2012-06-29 04:29
id:tozima
こんな記事があった。
Java の語彙で Maybe を説明してみる - ぐるぐる～
直和型のエンコーディングである、
$A + B = \forall X. A \to B \to X$
でMaybeモナドを説明している、まっとうな記事です。気になったのは、上のエンコーディングを Java の上でやって、なにか変なことが起きないのかということ。例えば記事中では、
$\mathrm{inl}(\mathbf{null}) : \text{someClass} + \mathbf{unit}$ *3
みたいなことが、Javaでは禁止できない、ってことについて触れています。この他には変なことはおきないんでしょうか？
僕には全然Java的な言語への直感がないので教えてください！！！

「......みたいなことが、Javaでは禁止できない、ってことについて触れています」というのは元記事の

just やら Just のコンストラクタやらに null を渡すとダメという点で、ポリモーフィズムなし版より残念なことになっていますが......
Java の語彙で Maybe を説明してみる - ぐるぐる～

という部分のことです.

nullの呪縛

2012-07-01 02:05
id:tarao
$\mathrm{inl}(\mathbf{null}) : \text{someClass}+\mathbf{unit}$ になってしまうのは, そもそも $\mathbf{null} : \text{someClass}$ だからだと思うので, このことが $\mathrm{inl}(\mathbf{null}) : \text{someClass}+\mathbf{unit}$ になってしまうこと以外に(安全性に関して)別の問題を引き起こしたりしないのか? という質問だと思います.
記事を読んでまず不安に思ったのは, Maybe自体もふつうのクラスなので, Maybeを返すメソッドは実はふつうにnullを返せてしまうこと. そうするとmatchの呼出しがぬるぽで落ちる. これはかなり致命的だと思う.
もう一つ不安に思ったのは, ifJustがnullを返す場合. これもJust.matchで返り値をチェックして, nullを返そうとしたら例外とかでもいいのかも知れないけど, なんか結局例外なのかよ, という感じがしてnullの呪縛から逃がれられなくて残念感が漂う. 一貫性のある実装としてはmatchの返り値をMaybeに強制するのだろうけど, 一つ目の不安と同じ理由でそれでもやっぱりnull返せるからあんまり意味ない.

Javaにはnullがあるので(またnullとそれ以外を型で区別できないので), 本質的に型検査によって安全性*4を保証することはできません*5.

しかし, id:tozimaさんの疑問はこのことではありませんでした*6.

Javaで直和型を実現?

2012-07-03 22:27
id:tozima
それでは，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
Types and Programming Languages (The MIT Press)
- 作者:Pierce, Benjamin C.
- 発売日: 2002/01/04
- メディア: ハードカバー
(Chapter 19)

Javaで直和型

ポリモーフィズムによる素直な実装

2012-07-04 14:44
id:tarao
たぶん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
id:tarao
ただし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
id:tozima
なるほど．確かに特化がありえると parametricity を失ってしまって，代数的データ型のエンコーディングにならない可能性があるわけですね．これは全然，思い付いていなかったです．

勝手なことはさせない版

2012-07-04 14:44
id:tarao
ポリモーフィズムを使わない実装をすればもう少し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
id:tarao
(2)の問題に少し関連しますが, 部分型があるので, SとTが部分型関係にあるとinlとinrのどちらでも可能という状況が発生することはあります. そのことを想定し忘れると, たとえばTがSの部分型のとき, fの引数の実行時の型はTではないと仮定してfを実装してしまうことになりますが, 実際にはinlされうるので意図通りに動かないことになります.

合わせ技

2012-07-04 14:44

id:tarao

部分型の小さな問題は残りますが, 最終的には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
id:tozima
おおよそ流れは追えたと思います．すばらしい解説をありがとう．残された課題は「証明を自力で書ききれない」という点だけだと思うので，これはいずれ勉強します．
最終的なコードでは，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:式 $\mathrm{inl}(\mathbf{null})$ に型 $\text{someClass} + \mathbf{unit}$ が付くという意味. 以降「:」の意味は同じ.

*4:型の付いたプログラムがエラー(Javaの場合例外)を発生させることが無いこと.

*5:他にはたとえば(ダウン)キャストをすると例外が発生する可能性があり, また再帰呼び出しでスタックが溢れて例外が発生する場合もあるので, Javaの安全性についての理論を語る上ではこのような例外を除外するしかないので, 同様にNullPointerExceptionについては安全性の要件に入れなければ安全性は成り立つかもしれない(が, その安全性に何の意味があるのか).

*6:そもそもこの程度のことは元記事でも補足されていましたね.

*7:実際のJavaを考えるとこの表現は少し不自然かも知れません. ようするにあるオブジェクトが例外型かそれ以外かを区別するということです.

*8:これは現行のJavaではコンパイルのフェーズで型引数の情報を消去してしまっていて, 実行時には型引数として何が渡されたのかどうやっても分からないためです.

*9:これはnewの場合と同じく型消去のせいです.