https://twitter.com/kinaba のログ (twilog の方が便利です。)
| http://d.hatena.ne.jp/niha/20080920#1221933252 そうかc_or_g(...) でいいのか！！！俺の (out_or_g(g))(c_or_cp) とか遠すぎる | |
| http://jinakanishi.tumblr.com/post/50699972/reading-test-jpg これって http://med-legend.com/mt/archives/2003/09/#000096 これだよな。ElingshがCmabrigdeに進化してるのは5年の間にソース見つかったのか | |
| イカ画像を探してたらこんな時間に。http://animals.web.infoseek.co.jp/others/bigfinreefsquid.html アオリイカかっこいい | |
| そんな用語は全くないけれども、どちらかというとvalueがfirst class typeなのがdependent type、というイメージがある | |
| @ranha ふつーの型システムだと型のパラメタにできるのは型だけだけど、整数とか文字列とかもパラメータにできるのがDependent Type。"typeがfirst class value"だと「普通の関数が整数とか文字列しかに加えて型もパラメタにとれる」なのである意味逆 | |
| 突き詰めていくと最終的には型も値も区別がなくなってくるので（http://en.wikipedia.org/wiki/Dependent_type → Calculus of constructions）、究極的には同じと言えなくもないかもだけど、まあ入り口は別だと思う | |
| そろそろCoqのチュートリアルを書かないと、@chunjp先生の年次計画を阻害してしまうという畏れおおいことになりかねないのを思い出した。 | |
| いやそれは冗談としてもCoqチュートリアルはすごく書きたいんだけど、いい題材が全然思いつかないんだよね。生の命題論理の定理を証明して遊んで楽しいのはよほどの論理オタクだけだろうから避けたいと思うと全然簡単なネタがない |