Nominal and Structural Type Systems

以前、ちょっと話題になっていて、どうも私の理解とは異なる結論だったので気になっていた。コードの読みやすさは、どれだけ型推論に頼るかの問題であり、確かにその差は型システムの違いから生じるものではあるが、他のもっと本質的な問題を無視するのは問題ではないかと感じていた。まあ、でもそこまで強く主張したいとも考えていたので特にコメントはしなかったのだが、今日TAPLを読んでいたら言及があったので、やっぱり書いてみることにする。

「19 Case Study: Featherweight Java」の「19.3 Nominal and Structural Type Systems」のあたり。*1

まず、nominalな型システムとstructuralな型システムの定義から。TAPLでは、

  • subtypingに型の名前が重要な役割を果たすのがnominalな型システム
  • subtypingが型の構造から決定されるのがstructuralな型システム

と説明されている。もちろん、Featherweight Java(FJ)はnominalな型システムの例である。*2

TAPLでは、nominalな型システムのメリットとして次の4つが挙げられている。

  1. 型検査以降も、特に実行時に型情報を活用できる
  2. 再帰的な型の取り扱いが容易
  3. 型検査、特にsubtypingの検査が自明なまでに簡単
  4. 明示的にsubtypingを宣言するため、誤りが生じにくい

型システムとして本質的なのは、最初の二つとされている。

一つ目から。通常、nominalな型システムをもつ言語では、値の型がそれぞれ名前で保存されていると言うことである。そのため、リフレクションやマーシャリング、画面出力などで、活用できる。もちろん、structuralな型システムでも、値に型を示すタグを埋め込めばいいわけだが、あまり活用されているとは言いがたいね、という結論。

二つ目。structuralな型システムにおける再帰的な型の取り扱いの難しさは、私自身身をもって知っていることである。特に多相型がからんでくると、絶望的になってくる。nominalな型システムでは、名前を書いておけばいいのだから、なにも難しいことはない。MLなんかでは、いろんな機能でstructuralな再帰型を取り扱っているので、特に気にせずに使えるんだけどね、という結論。

三つ目。これはなにも難しいことがない。

四つ目。これもわかりやすい。明示的にsubtypingの関係を宣言するわけだから、プログラマにとってあほなバグを仕込むことがなくなるらしい。本当かどうか、ちょっと疑問だけど。

ただ、nominalな型システムには良いことも悪いこともあるよ、と書いてあるのだが、disadvantageは書いてないように見える。いろんなところにreferが書かれているので、その辺にバラして書いてあるのか知らん(そこまで読んでない)。


まあ、こんなところ。1の話と言うのは、純粋なstructuralな型システム以外では問題にならない*3ので、実際には無視できるでしょう。しかし一方で、2は未だに本質的な問題であり続けている、というのが私の理解。


これからどうしようかなあ…

*1:Featherweight Javaとは、Javaの型システムを考えるための小さなサブセットで、Javaと似たような型システムになっている。ただし、ここではどうでもよい。

*2:structural polymorphismな型システムはどうなるんだろうとか、天邪鬼な私は考えてしまうが、FJの話をしていることを念頭に置けば自然な定義だろう。

*3:例:Ruby