https://twitter.com/kinaba のログ (twilog の方が便利です。)
| @kinaba コラッツやグッドスタインみたいな止まり方がよくわからん数列で決まる連分数を使えばなんかそれっぽくなるか。自然かどうかはさておき | |
| ICFP の Accepted Paper が出てる http://icfpconference.org/icfp2014/accepted.html | |
| McBride の新作 http://icfpconference.org/icfp2014/accepted.html 半分まで読んだ。相変らず面白い。データ構造に値がソートされて入ってることを依存型で保証するときに、普通の関数型で書いたコードが自然と、証明項など明示的に足さず、型が勝手に語りだし証明完了するように型を作る奮戦記 |