「念願のネタで原稿を依頼された(が、…)」のごとき事情で、ウーンとか、考え込んでいます。なんか書き散らしているうちに焦点が定まるかも、という目論見。(日記の文面を原稿に流用するようなことはしません(できません)けどね。)
ここ3年、5年というスパンで考えると、形式手法にとって、わずかながらもいい傾向がいくつか見えます。
- インターフェースという概念が浸透したこと。
- xUnitと呼ばれるツール類とか、テストファーストが認知されたこと。
- Generics(パラメータ付き型)などの登場で、「型」概念(の常識)が拡張されたこと。
などです。
さてここで、発展的蒸し返しの手法(ってナンダソレ)を使います。国島先生のエントリーを引き合いに出します。国島先生は、ご自身の今期Java講座に対して次の感想を述べておられます。
教えるべき内容がずいぶん体系化され、情報数学的に扱えるようになった。これは教える側にとってとてもありがたいし、学生さんにとっても興味をひく内容になったのではないかと思う(単に私の自己満足かもしれないが…)。松本吉弘先生の「ソフトウェア工学」の序文に「数学(情報数学)的体系に基づいて構成的に話しが進められる部分に関しては、(学生に)大変評判がよい」とあるが、まさにその通りだと思う。
いやー、すばらしい。ちなみに、松本吉弘先生の著書『ソフトウェア工学』は僕も紹介・引用しています。僕の知る範囲内では、日本語の本で「インスティチューション」に言及しているのはこれだけです。
まー、それはともかく、講義の改善ポイントは何であったかというと、実装寄りの説明を採用したこと以外に、「型とクラスの違いを明確にしたこと」、「値の集合としての「型」から、代数としての「型」に飛躍が起こっていることを時間をとって説明したこと」となるでしょう。型概念を、値の集合から代数(代数系、代数構造)にまで引き上げることは大賛成です。
値の集合としての型(types as sets)で理解できるのは、ごく素朴(悪い意味での“ナイーブ”)なレベルまでで、やっぱり、代数としての型(types as algebras)への“飛躍”は必要です。出来ることなら、もう一声; セオリーとしての型(types as theories)まで飛躍すると、さらに広い視野が手に入ります。セオリーとしての型は、仕様としての型(types as specifications)、制約としての型(types as constraints)と言っても同じことであり、上で松本先生にからめて出した単語「インスティチューション(institution)」につながります。
型理論やインスティチューションの話を系統的にする気は全然ないのですが、具体的かつ典型的な例を1つか2つ出して、雰囲気が伝わる話をしようと思います。一エントリーで済ます予定だったのだけど、僕の都合で、ここでいったん切って、続きは次のエントリーにします。