null安全おじさんになりかわりそれがしがお見せつかまつる 機械が理解できる複雑な契約の型表現がもたらすものは つまるところこのようなもの ずぶぶ(切った腹から証明オブジェクトを引き摺り出す)— Noriyuki OHKAWA (@notogawa) 2016年11月18日 過ぎたるは…

依存型ならさらに安全にプログラミングできちまうんだ！と言ったところで，「無料で遊べちまうんだ！」とか「3000円払えば無料で10連まわせる」みたいな感があり， 依存型使わない場合とどう違ってくるのか 入出力から扱い始めるとどういった形のプログラム…

ghc 7.10 からみられるようになった現象で，放置しているうちにやや旬を過ぎてしまっている感もある話題なのだが，その後特に改善してるわけでもないのと最近踏まれたのを見たので念のために記しておこうかなと．コンパイル時間ghc-7.8で1分40秒なやつがghc-…

関数プログラミング実践入門という本を書きました - ぼくのぬまち 出張版 に引き続き，よろしくおねがいします．[増補改訂]関数プログラミング実践入門 ──簡潔で、正しいコードを書くために (WEB+DB PRESS plus)作者: 大川徳之出版社/メーカー: 技術評論社発…

(追記) cabal update で反映される模様？Agda-2.4.2.5のDependenciesで，unordered-containersを見て欲しい．依存関係が >=0.2.5.0 && メタデータのみをパッケージアップロード後に編集したもので，実際2016/1/25現在見えているメタデータはrev 1となってい…