2005-04-07 [長年日記]
λ. 入学式
![[壇上の写真]](./images/20050407_0.jpg)
朝早くて大変だった。でも、僕が着いたときにはまだほとんど来ていなくて、前から2番目の列になってしまった。8:40までに入場ということだったんだが、時間になってもまだ半分も埋まっていない。こんなことならもっとゆっくり来れば良かったかも。
式辞で安西先生は「志」を強調していた。「自分に志はあるだろうか?」と考えて憂鬱になったりもしたけれど、お話自体はよいお話だったと思う。これからのことを考えるとプレッシャーを感じる。入学式は結局正味三十分くらいで終わった。学部の卒業式もこれくらい短いと良かったのだが。
ところで、三田に来るのは学部の入学手続きの時以来なので、ずいぶん久し振りだ。時間もあるので、キャンパスを少しゆっくり周る。そして思う。ここには伝統がある。そして伝統に裏付けられた自信が感じられる。それが心地よい。SFCは三田と比べるとなんというか「人工的」で、どこか心が落ち着かないところがあるように思う。もちろん、どちらが良いとか悪いとか言うつもりはない。
λ. 桜
キャンパス内に咲いている桜が綺麗だった。帰りにもあちこちで桜が咲いているのが見えた。ついでに、中島千波作品展「桜花爛漫」というのを見てきた。世間は桜の季節ですな。
桜といえば、西行法師が「願はくは花の下にて春死なむ そのきさらぎの望月のころ」と詠んだ通りに没したのは文治6年(建久元年) 2月16日だった。これはユリウス暦だと1190年3月23日、グレゴリオ暦だと1190年3月30日にあたるそうだ*1。今年の3月30日はもう過ぎちゃったな。一週間前は桜はまだあまり咲いていなかったように思うが、これはまあ誤差みたいなものか。ちと残念ではある*2。
- 参考
λ. Ωmega
イネムリネズミ日記(2005-04-04)より。スライド「Generalizing Algebraic Datatypes in Ωmega」を見た感想。
- Syntax は GADT のものではなく、Phantom types に似てる。
- New Kind の概念を導入してるのは、現在のGHCのGADTよりもスマートだな。
- Some example に挙がっている A Language with Security Domains はなんだろう。興味を引かれる。
-
[2005-04-07 追記] 説明ありがとうございます。
type-basedの情報流解析(information flow analysis)
と言われると良くわかります。このスライドの例だと確かにLowであるような式がHighの変数を参照しないことを強制できてますね。
SLam Calculus *1 についても後で調べてみよっと……*2
-
[2005-04-07 追記] 説明ありがとうございます。
- A Language with Security Domains の例を見ると、lazyでないのにはそれなりに意味がありそう。これは Hughes の Dependent Types in Haskell を読んだときにも思ったのだけど、undefined は「証明」の値として不適。
- Computing over types のところはあまり細かいことは書かれていないが、型上の計算をどこまで許すかというのは多分微妙で、そこにはデザインデシジョンがあるのではないかと思う。
- [2006-04-23追記] Programming with Static Invariants in Ωmegaも参照
