Idris勉強会

11/8(Wed) @BizReach (渋谷クロスタワー)

依存型

シグネチャだけで、よくあるエラーケース・コーナーケースを弾けて嬉しい

引数として受け取れたなら、必ず計算できる関数を書ける

code:tail.idr

tail : Vect (S n) a -> Vect n a

tail x :: xs = xs

tailやheadでも、Maybeでくるむ必要のないシロモノを書ける

下の方に書いてあるが、

code:zip.idr

zip : Vect n a -> Vect n b -> Vect n (a, b)

zip [] [] = []

zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys

長さの同じリストだけを要求できる

バリデーションは呼び出し側に強制できる

関数のシグネチャを満たすような値でなければ渡せない。コンパイルが通らない

バリデーションがダブることもない

ドキュメントも必要最小限で済む。

「同じ型の値の中でも例外があるケース」を別途記述しなくていい

同値型

長いので略。そのうち資料公開されることを祈る

Idris所感

遅い。ゲロ遅い。コンパイルも実行も遅いので実用的ではない

The constructors of the required type. If they have arguments, it will search recursively up to a maximum depth of 100.

その他面白いが色々罠はある

取り敢えず下記リンクが導入にいい