Agda の驚き

今年もかなり Agda 面白かったんですけど

　　自分で最初に思い描いてたのと、違う方向にいく

一つは自分がたこなんだとは思うけど、

　　Agda の発想と、人の発想が異なる

ってのはあるかも。例えば

　　配列とAgdaの相性は良くないが、N -> Hoge ならよい
　　List でなんでもやるのは、だめで、やはり、N -> Hoge ならよい

みたいな感じ。

有限オートマトンの有限性がどこに効くのかとかを確認できて面白かった。例えば、正規表現の微分法には有限性は不要とか。

綺麗に仕上がると面白いけど、なかなかね。