2001-07-15
λ. それで後者なんですが、僕が気になったのは、dump出来ないオブジェクトを含む複数の値を返すようなメソッドをリモートで呼び出した場合に、返り値の配列全体がDRbObjectになってしまって、呼び出した側で多重代入が出来ないという点です。
ただ、Rubyが多値を配列を使って表現している以上、これは仕方無いと思うので、気にしないことにしました。DRb側で解決するのは、不可能ではないにしても、綺麗な方法では難しいでしょうし。
λ. 朝
起きたらまだ熱があったので、英検はパス。ここでこじらせたら学校のレポートと試験がやばすぎだし。
2002-07-15 ありがとう。そしてさようなら。
λ. rbnamazu
.namazurcでのReplaceの置換結果に「#」を使おうとしてはまってしまった。
--- nmzdoc.rb~ Sat Nov 10 23:29:37 2001
+++ nmzdoc.rb Sun Jul 14 00:10:38 2002
@@ -77,7 +77,7 @@
if FileTest.readable?(confname)
open(confname) do |conffile|
conffile.each_line() do |line|
- cindex = line.index(/\s*\#/)
+ cindex = line.index(/^\s*\#/)
if cindex
line[cindex .. line.length() - 1] = ''
end
λ. 働く車占い
chikoさんのとこから。結果
のんびり屋さんのあなたはまさに気球。風に任せて他人や社会の規則にとらわれることなくふわりふわりと生活します。また、いったん軌道に乗ると真っ直ぐに目標に向かって突進し頼もしく見えます。純真な性格なのですが、孤立してしまうことも。
λ. 『デフレの経済学』 岩田 規久男
を借りた。
2008-07-15
λ. ICFP Programming Contest 2008 終了
結局、結果はだせなかったけど、72時間とても楽しかった。
【2008-10-05 追記】 最後にsubmitしたアーカイブを一応晒しておく。icfp08.tgz
2009-07-15
λ. “Observational equality, now!” by Thorsten Altenkirch, Conor Mcbride, Wouter Swierstra
Thorsten Altenkirch らの Observational equality シリーズ最新作、といっても2007年のだけど。
通常の内包的型理論で何かやろうとすると、propositional equality が関数の外延性 (∀x. f x = g x) ⇒ f = g を満たさないために、いろいろ面倒なことになる。一方で、外延性を単純に公理として追加すると、canonical form に簡約出来ない閉項が出てきてしまう。 また、propositional equality から definitional equality を導くことを許す外延的型理論では、関数の外延性は成り立つが、definitional equality の判定が決定不能になるので、型検査が決定不能になってしまう。 まとめると、以下の三つの性質を同時に満たす型理論はこれまでなかった。
- propositional equality が関数の外延性 (∀x. f x = g x) ⇒ f = g を満たす
- 閉項はその型の canonical form に簡約出来る (canonicity)
- definitional equality (≡) と型検査が決定可能
この問題を解決しようとする著者らのアプローチが observational equality を用いる observational type theory (OTT)。基本的には等号をすべての型に対して一様に定義するのではなく、値の振る舞いに着目した等号を型の構造に応じて定義していく。 例えば、関数型A→Bだったらすべての引数に対する値が等しいことによって定義するとか。
ただ、それだけではうまくいかなくて…… (省略)
著者らの前の論文 Towards Observational Equality からの大きな変化としては以下の二つ。
- 通常の型の世界(set)と命題の世界(prop)の明確な分離
- Type-directed quotation による definitional equality の拡張
通常の型の世界(set)と命題の世界(prop)を明確に分離し、setでの計算にpropから影響を与えられるのは矛盾を導けたときだけであることを示している。それによって、矛盾しない限りpropには幾らでも規則を追加出来るようになる。それによって、これまでのややこしかった構成が非常に簡単になっているように思える。
また、型主導で canonical form (やボックス)への置き換えを行う Type-directed quotation を用いて definitional equality を拡張し、命題を proof irrelevant にしている。 これにより、S≡T implies (s[Q:S=T〉 : T) ≡ (s : T) が成り立つようになり、definitional equality が成り立つ型の間での型変換が無視できるようになる。 それによって、これまで懸念だった、帰納的データ型をW-Typesにエンコードする場合の問題が解決する。
Agda2上への実装が示されていて、分かりやすかった。
