このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

型→代数→…それから:型理論入門(の前半)

「念願のネタで原稿を依頼された(が、…)」のごとき事情で、ウーンとか、考え込んでいます。なんか書き散らしているうちに焦点が定まるかも、という目論見。(日記の文面を原稿に流用するようなことはしません(できません)けどね。)

ここ3年、5年というスパンで考えると、形式手法にとって、わずかながらもいい傾向がいくつか見えます。

  • インターフェースという概念が浸透したこと。
  • xUnitと呼ばれるツール類とか、テストファーストが認知されたこと。
  • Generics(パラメータ付き型)などの登場で、「型」概念(の常識)が拡張されたこと。

などです。

さてここで、発展的蒸し返しの手法(ってナンダソレ)を使います。国島先生のエントリーを引き合いに出します。国島先生は、ご自身の今期Java講座に対して次の感想を述べておられます。

教えるべき内容がずいぶん体系化され、情報数学的に扱えるようになった。これは教える側にとってとてもありがたいし、学生さんにとっても興味をひく内容になったのではないかと思う(単に私の自己満足かもしれないが…)。松本吉弘先生の「ソフトウェア工学」の序文に「数学(情報数学)的体系に基づいて構成的に話しが進められる部分に関しては、(学生に)大変評判がよい」とあるが、まさにその通りだと思う。

いやー、すばらしい。ちなみに、松本吉弘先生の著書『ソフトウェア工学』は僕も紹介・引用しています。僕の知る範囲内では、日本語の本で「インスティチューション」に言及しているのはこれだけです。

まー、それはともかく、講義の改善ポイントは何であったかというと、実装寄りの説明を採用したこと以外に、「型とクラスの違いを明確にしたこと」、「値の集合としての「型」から、代数としての「型」に飛躍が起こっていることを時間をとって説明したこと」となるでしょう。型概念を、値の集合から代数(代数系、代数構造)にまで引き上げることは大賛成です。

値の集合としての型(types as sets)で理解できるのは、ごく素朴(悪い意味での“ナイーブ”)なレベルまでで、やっぱり、代数としての型(types as algebras)への“飛躍”は必要です。出来ることなら、もう一声; セオリーとしての型(types as theories)まで飛躍すると、さらに広い視野が手に入ります。セオリーとしての型は、仕様としての型(types as specifications)、制約としての型(types as constraints)と言っても同じことであり、上で松本先生にからめて出した単語「インスティチューション(institution)」につながります。

型理論やインスティチューションの話を系統的にする気は全然ないのですが、具体的かつ典型的な例を1つか2つ出して、雰囲気が伝わる話をしようと思います。一エントリーで済ます予定だったのだけど、僕の都合で、ここでいったん切って、続きは次のエントリーにします。