型理論が見えてきたかも

CS

きちんとした教科書に当たってない訳だが...
型理論というのは，データやソース片に付加し得る属性と言うか，今流行りの言葉で言えばアノテーション（？）を，ソースの静的分析によってどこまで詳しく自動付加できるか追求してるみたい．そしてそこで使われるアルゴリズムを抽象化すると新しい「論理学体系」が生まれる，と．もはやintがどうのというのをすっかり超えている．
線形型linear typeと依存型dependent type（そしてそれらのヴァリアント）を知ったことで上の話が見えてきた．「こんなものまで『型』と称するのか！」と．昔はただ「チェックする」とか「解析すると分かる」等と，曖昧に，個々の場合ごとに言われてた作業や手法が，「それらは値の持つ『型』だから『型推論』してやればいい」というパラダイムにまとめられつつある．

これはまさに現在進行形の「体系化」の一過程なのか？ そう言えばBackusチーム＠IBMが初めてFortranコンパイラを作ったとき，字句解析はアドホックで複雑な処理工程だった... と言うか分化すらしてなかったのかな？ それを次第に洗練し，ある意味では制限を加えることで，今のオートマトンによるとても見通しのよい（それゆえ研究としてはほぼ「終わった」）形が生まれた．