OSC Okinawa 当日

いつも通り、学生の発表資料がたこたこで。でも、発表当日よりは前日にぼこぼこにされた方が良いよね? ぼこぼこにすると、だいぶマシになるようです。最初から考えてやれと思うが、まぁ、それを教えるのが仕事でもあるからなぁ。

今回は Haskell 入門みたいな感じにしてもらったのですが、説明不足なスライドばかり。

「ソースコードは一つに絞って、それだけを丁寧にやれば?」

まぁ、そういうことをすれば少しは理解も深まるのではないかと。

そんな感じで、大学に泊まってしまったんですが、泊まった理由はどちらかといえば、

＊　Agda にハマったから

Agda 危ないです。詰将棋みたいな面白さがある。

(1) 型の部分(record の field) で自然変換やMonadが満たすべき性質を書く

(2) そいつのconstructorを別に作る (ここは比較的やさしい)

(3) 証明したい式を型で書く

(4) その型にあった証明を(1)や(2)で定義した関数の組み合わせdで書く

という方式。徐々に、進んでいけるのと、型が先導してくれるので、割と順列組み合わせでできる。その場で使う関数は、それほど多くないので。

コンパイラ書いている時も同じような感じなったことがあったっけ。

というわけなので、OSC 最中とっても眠かった。さて、次は懇親会か。