Idrisみたいに、函数プログラミングを前提にしている言語には函数を合成する演算が標準で用意されているよね。 (.) : (b -> c) -> (a -> b) -> a -> cこの演算子を使うと、函数を合成してくれる。函数の合成を使えば、プログラムを変数を使わないで書くこと…

帰納と余帰納 制限された再帰 Idrisには函数が全域函数であるかチェックする機能があるのだけれども、プログラムに制限なく再帰が使われていると、その函数が値を返すのか、それとも停止しないで値が返らないままなのか判定する方法が存在し得ない。そこで、…

表明から証明へ (3) headを証明する HaskellのPrelude.headとは異なり、IdrisのPrelude.List.headは、引数にコンスセルである証明をとるので、全域函数になっている。Idrisのシステムでは次のように、%assert_total宣言によって、全域函数であることが「表明…

表明から証明へ (2) 型と命題 カリー゠ハワード同型対応により、プログラムと証明が対応すると述べた。実際にはどのように対応しているのだろうか? 実は、恒真である命題は、空でない（その型である値を持つ）型に対応しているのだ。 型と命題の対応関係を見…

表明から証明へ 表明とテスト バグの原因のひとつとして、プログラム実行時に守るべき条件が守られていないことが挙げられるだろう。プログラムが一体どのような場合に正常に動作し、どのような場合に望まない結果をもたらすのかが分かっていなければ、バグ…

ハロー、依存型プログラミングの世界 (3) 依存ペア 依存ペア dependent pair とは、ある値と、その値に依存した型を持つ値のペアのことだ。 data Exists : (a : Type) -> (P : a -> Type) -> Type where Ex_intro : {P : a -> Type} -> (x : a) -> P x -> Ex…

ハロー、依存型プログラミングの世界 (2) データ型の宣言 代数データ型を宣言する場合には、Haskellと同様の記法を使うことができる。HaskellでもおなじみのEitherやListの宣言はidrisではこうなっている。 data Either a b = Left a | Right b data List a …

はじめに Idrisという、Haskellに似ていて、依存型 dependent type を持っている言語がある。依存型を持った言語なんて他にもあるのだけれども、Idrisは general purpose を謳っている。わざわざ汎用って謳っているあたり、依存型ってのはもっと色々に使える…