Idris勉強会
11/8(Wed) @BizReach (渋谷クロスタワー)
依存型
シグネチャだけで、よくあるエラーケース・コーナーケースを弾けて嬉しい
引数として受け取れたなら、必ず計算できる関数を書ける
tail.idrtail : Vect (S n) a -> Vect n a
tail x :: xs = xs
S n は O にマッチしないので非空リストを要求できる。
tailやheadでも、Maybeでくるむ必要のないシロモノを書ける
下の方に書いてあるが、
zip.idrzip : Vect n a -> Vect n b -> Vect n (a, b)
zip [] [] = []
zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys
長さの同じリストだけを要求できる
バリデーションは呼び出し側に強制できる
関数のシグネチャを満たすような値でなければ渡せない。コンパイルが通らない
バリデーションがダブることもない
ドキュメントも必要最小限で済む。
「同じ型の値の中でも例外があるケース」を別途記述しなくていい
同値型
2つの Nat が同値であることを型レベルで表現するテクニック（ EqNat ）を使って、 zip が常に成功するようなバリデーションをする例
長いので略。そのうち資料公開されることを祈る
Idris所感
遅い。ゲロ遅い。コンパイルも実行も遅いので実用的ではない
LTE Nat Nat によるチェックが失敗するので 100 - 100 ができないとかいう罠
> The constructors of the required type. If they have arguments, it will search recursively up to a maximum depth of 100.
その他面白いが色々罠はある
取り敢えず下記リンクが導入にいい