…て、代数／余代数とかインスティチューションとかもあるのですが、知名度(?)から言ってモナドかな、結局。と、まーそういうことです。最初は、モナドの具体例を丁寧に紹介するつもりです。僕の感覚では、リストモナドが典型的モナドなので、リストから入るかもしれません。「圏論やモナドが、どうして文書処理やXMLと関係するのですか？」で紹介したテンプレートモナドも具体的で面白いですね。「世界で一番か二番くらいにやさしい「モナド入門」」で扱った大域変数への代入とか、ファイル入出力とか例外とかも…

…することにします。「インスティチューション」という言葉を表だっては出しませんが、僕の気持ちとしては、インスティチューション入門も意図しています。「もっと型理論」の続きみたいな感じかな。内容： 言葉と記法の準備 インターフェースの実例 リネーム 指標射 モデル（＝実装クラス）のリダクト操作 セオリーでプログラマの気持ちを表す もう一回くらいは続くでしょう ●言葉と記法の準備毎度毎度愚痴っていることですが、用語法がいっぱいありすぎてやんなる。おおざっぱな対応表↓ オブジェクト指向…

… 僕がたまに口にするインスティチューションや余代数の説明も、いつかJavaScriptを使ってするかもしれません（無保証言明）。 これの準備のつもりなんですが、それは置いといて、単に「できるだけ小さな言語仕様」ってことなら、いくらでも案はあると思います。「通常のプログラミング言語に類似の構文」という制限も別に意識しなくてもいいでしょう。そういう自由に決めていい「極小プログラミング言語」って、個人の好みや経験や価値観をけっこう反映することになりそうだな。僕自身は、なんだかんだ言…

…れないな（背後にあるインスティチューションが好きなんだろうが）。続き物にする気はなかったのだけど、また型理論の話を少し。昨日のエントリー「もっと型理論」で： "types as specifications/theories"の立場では、サブタイプ／スーパータイプの定義は複雑になります。問題は、サブタイプ／スーパータイプ概念が、extendsだけで尽きているわけではないことです。まだ説明すべきことが残っているのです。 と書いたけど、extendsだけも分かること／説明できるこ…

…す。しかし、T extends Sが成立しているなら、確かに「TがSのサブタイプ」だとは言えます。問題は、サブタイプ／スーパータイプ概念が、extendsだけで尽きているわけではないことです。まだ説明すべきことが残っているのです。残っている肝心なことはまた次の機会にします。[追記]インスティチューションとの関係に興味があれば、http://d.hatena.ne.jp/m-hiyama-memo/20060302/1141280252 にちょっとした補足があります。[/追記]

…：多重継承万歳！ 多重継承死ね！）を声を荒げて言いつのっても、どうせ何の結論も出ませんよ（少なくとも、ロジカルに意味のある結論が出る見込みはない）。まーもっとも、形式化が僕の趣味嗜好に合致しているのであり、それゆえ、「可能なら形式化すべき」との主義主張に至り、「形式化が明晰性をもたらす」という信仰を抱いているわけだから、天に唾を吐いているのは僕ですけどね。 *1:GoguenとBurstallがインスティチューションを導入したのは1984ですから、実は20年以上もたってます。

…では、日本語の本で「インスティチューション」に言及しているのはこれだけです。まー、それはともかく、講義の改善ポイントは何であったかというと、実装寄りの説明を採用したこと以外に、「型とクラスの違いを明確にしたこと」、「値の集合としての「型」から、代数としての「型」に飛躍が起こっていることを時間をとって説明したこと」となるでしょう。型概念を、値の集合から代数（代数系、代数構造）にまで引き上げることは大賛成です。値の集合としての型（types as sets）で理解できるのは、ごく…

…vaScriptで十分な気がしてます。僕がたまに口にするインスティチューションや余代数の説明も、いつかJavaScriptを使ってするかもしれません（無保証言明）。実を言えば、このあいだまでJavaScriptは「なんかトンデモない言語仕様の、ひどく貧弱な言語」-- みにくいアヒルの子と捉えていたのですが、りっぱな白鳥に、でも灰色の斑点が少し残った白鳥に成長しそうですね。いくらりっぱになっても、最適化コンパイラがEXEやDLLを吐く、とかはやって欲しくないな、可愛くなくなる。

…だけ記しておきます。インスティチューションの中心人物はGoguen（http://www.cs.ucsd.edu/users/goguen/）です。彼のインスティチューション・ページ（http://www.cs.ucsd.edu/~goguen/projs/inst.html）をハブに使えます。抽象モデル論という発想はバーワイズ（Barwise）が先のようですが、文（sentence、命題、制約）の集合を天下りに“単なる集合SenΣ”にしてしまったところが、Goguen/Bu…

…。枠組み大枠としてはインスティチューションでしょう、やっぱり。ただし、インスティチューションは何にでも使えるので、オブジェクト指向に特有な現象を説明できるわけではないですね。もっと狭くて強い枠組みには余代数があります。単一のクラスを説明するには余代数はけっこういいですよ。（いまいち中途半端な入門だけど→http://www.chimaira.org/docs/AlgebrasCoalgebras.htm）複数のクラスが絡んだシステムは、代数／余代数だけでは定式化が辛い。ここは…

…ちょっとイメージ落ちた。著者にも印税が入るのだろうが、CiteSeer, arXiv.org, 自分のWebサイトなどに論文を置いたほうが、より「文化と学術に貢献する」ような気がします。それはそうと、しゃくにさわる感情を横に置いて"Institutions:"を眺めて、まー、インスティチューションの例が載っている（当たり前だ）のがいいか、と。（$30の価値があったかといえば、、、いやっ、それは言うまい。）僕としては、当面、インスティチューションのいろんな具体例を知りたいから。

…、余代数／隠蔽代数、インスティチューション、トレース付きモノイド圏、コンパクト閉圏、デカルト閉圏あたりが使えそうな気がしている。各種モナド、トポス、テンソル圏、インデックス圏／ファイバー圏（indexed categories/fibred categories）あたりも道具にはなりそうだが、あんまりよくわかってない。 キマイラ・サイトの圏論コーナーは、http://www.chimaira.org/docs/indexCategoryTheory.htm 圏論に関係しそうな…

…へ 伴意から含意へ インスティチューション論理／モデル論をベースとした仕様技術といえば、現状利用できる最も便利な枠組みはインスティチューション（Institution）だろう。以下に、キマイラ・サイトの記事からインスティチューションに関する注釈を引用する： インスティチューションは、（僕は読んでないけど）Joseph Goguen & Rod Burstall "Institutions: Abstract model theory for specification and…

…だ。[蛇足] もし、インスティチューション（institution）を知っているなら、指標（signature）Σを1つ固定してモデル圏Mod=ModΣと文集合Sen=SenΣを考えれば、M、N∈Obj(Mod)に対して同値関係≡を定義できることを確認できるだろう。つまり、空間X=XΣはインスティチューションに対して定義できる。Σ |→ XΣ は関手に拡張できて、これは指標圏から位相空間の圏への関手になる。（細部をチェックしてないから、まちがっていたらゴメンね。）論理式が定義…

…は意訳しているが）をインスティチューション（institutions）で扱いたいのだ。Aを入力、Bを出力、Xを状態空間とするtransducerはf:A×X→B×X in Set で記述できる。transducerの圏は、SetからのCirc構成で、feedback付き圏になる。このままではtracedにならないが、タイミング（フィードバックの遅れ）をうまく処理すれば、たぶんtracedになる。さらにInt構成すれば、コンパクト閉圏になるはず。transducerの圏は、二圏…

…en program σ:Σ→Σ'からinduceされるreduct functor Mod(Σ')→Mod(Σ) も自然なものに思える。もとの指標圏Signから作ったKleisli圏の射の向きを逆向き（opposite）にするかどうかで、またまた悩む！ あーーー、向きや符号はいつもいつも悩みの種だぁ。が、作ったKleisli圏が有限余完備なら、そこでさらにCospan構成をすれば、かなり使いやすいインスティチューションが得られそうだ。って、ホントに作れるかどうかわからんが。

…しい!。具体的には、インスティチューション(Sign, Sen, Mod, |=)の指標圏Signが有限余完備な状況を考える。Maude（http://maude.cs.uiuc.edu/）やCASL（http://www.cofi.info/CASL.html）でも、この状況は仮定している。この状況で、Signがプアなとき、Sign上のモナドLを使ってSignを拡張したいことがあるのだ。そもそもインスティチューション自体をKleisli圏まで持ち上げなくてはならないのだが、…

… 次の2箇所でchimairaサイトに好意的な言及をしていただいております。 http://mag.autumn.org/Content.modf?id=20050127163831 : 「正気の試み」は「狂気の沙汰」の婉曲表現ですね。 http://aquamarine.c.oka-pu.ac.jp/weblog/archives/2005/01/post_2.html : ソフトウェア工学の本で、圏やインスティチューションに触れているのは、松本先生のアノ本以外知りません。