8 月 1 日に行われた第十二回渋谷 Java で Java の型システムについて LT をしてきました。以下が使用したスライドです。
ちなみに Featherweight Java を導入した論文はここで読めます。今回の LT では時間の都合上細かい内容をほとんど述べていないので、もし興味があればぜひ元論文に目を通してみると面白いと思います。なお LT で扱ったのは第 2 章で述べられている（ジェネリクスを持たない）FJ の部分です。
スライドの補足
型付け規則と簡約規則について、時間の制限もあり LT の中では例を 1 つずつ挙げるだけに留めました。しかしそのせいでスライド 25 ページ目の主張で "two impolite rules" という表現を用いて規則の詳細から逃げています。
元論文の系 2.4.6 (p.408) を見て頂ければおわかりのように、ここで言っている "two impolite rules" は
- ダウンキャスト式の型付け (p.404, Fig. 2,
T-DCast) - ダウンでもアップでもないキャスト式の型付け (p.404, Fig. 2,
T-SCast)
のことを指しています。FJ において、この 2 つの規則を用いずに型が付く式については正規系まで簡約したときに結果が値である、というのがもともとの主張です。
ジェネリクスの意味論
今回はシンプルな FJ についてのみ触れましたが、元論文ではこの後にジェネリクスを導入した体系 Featherweight GJ が論じられています。というより、分量的にもジェネリクスの方が元論文の「本体」で、今回紹介できた部分はいわばその前哨戦。
もし何か機会があればこのジェネリクスについても話したいと思っているのですが、それはまた別の話。
