こわくない Idris (6) - M59のブログ こわくない Idris (6) - M59のブログ 1年前に書いた記事を読み返していたら、証明がすぐには理解できなかった。証明の内容を言葉で分かるように書いておきたいと思う。次のコードのMyHead.headは、全域函数だ。 %default total namespace MyHead head : (l : List a) -> (isCons l = True) -> a head Nil prf = FalseEli…

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

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

表明から証明へ (2) 型と命題 カリー゠ハワード同型対応により、プログラムと証明が対応すると述べた。実際にはどのように対応しているのだろうか? 実は、恒真である命題は、空でない（その型である値を持つ）型に対応しているのだ。 型と命題の対応関係を見てみよう。 型 命題 (x : A) -> P x (x : A ** P x) Not P (P, Q) Either P Q P -> Q ここで、NotはBuiltins.idrで次のように定義されている。 Not : Typ…

表明から証明へ 表明とテスト バグの原因のひとつとして、プログラム実行時に守るべき条件が守られていないことが挙げられるだろう。プログラムが一体どのような場合に正常に動作し、どのような場合に望まない結果をもたらすのかが分かっていなければ、バグのないプログラムは作れない。 言語の中には、表明という形でプログラムの条件を記述できるものがある。表明はプログラムの仕様をより明確にするし、誤った形でプログラムが使われた場合、バグはプログラムが不可解な挙動を引き起こす前に検出できるだろう。…

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

ハロー、依存型プログラミングの世界 (2) データ型の宣言 代数データ型を宣言する場合には、Haskellと同様の記法を使うことができる。HaskellでもおなじみのEitherやListの宣言はidrisではこうなっている。 data Either a b = Left a | Right b data List a = Nil | (::) a (List a)このようなデータ型宣言を行うと、型コンストラクターと値コンストラクターが定義される。Idrisでは型も値だから、…

はじめに Idrisという、Haskellに似ていて、依存型 dependent type を持っている言語がある。依存型を持った言語なんて他にもあるのだけれども、Idrisは general purpose を謳っている。わざわざ汎用って謳っているあたり、依存型ってのはもっと色々に使えるものなんだぞって主張があるように思う。そんなIdrisなんだけど、日本語による文献はとても少ない。今のところ、Idrisをやろうって人はまず英語のチュートリアル読まなきゃいけない。僕はIdr…