Coqで依存型 - にわとり小屋でのプログラミング
最近Agdaがはやっているみたいなので、Coqでも依存型（dependent type）を使ってみた。 実装したのは長さ n のベクトル型だ。このベクトル型を使うと、空でないとか、長さが等しいとかを型の段階で保証できるので、より安全なプログラムを書くことができるのだ。 Variable A:Set. Inductive Vec : nat -> Set := | VNil : Vec O | VCons : forall n, A -> Vec n -> Vec (S n). このベクトル型を使えば、コンパイル時に長さの整合性もチェックしてくれて、間違いがある場所を教えてくれる。コンパイルさえ通れば、OutOfBoundsExceptionのような実行時エラーは起こりえないことが保証される。 例えば、一般的にリストのhead関数は、引数が1以上の長さのときのみ定義でき、空リストの場合には値
ヒビルテ(2009-04-18)
λ. 型レベルプログラミングの会 (以下書きかけ) 参加した。 稲葉さんのまとめ 以下は個人的メモ。 Scala 型レベルプログラミングの会 - Onion開発再開しつつある日記(2009-04-18) チャーチエンコーディングするまえに普通の表現を考えようよw 演算結果の型を type member として表現するのはちょっとC++っぽいな。あと、型レベルVisitorパターンはなるほどという感じだった。 型レベルの再帰の上限を-Yrecursionオプションで指定するという話に対して、「terminationチェッカを使うような方向性はないのか?」という質問をしたが、考えてみたらこの辺りは他の言語でも同じ話だし、開いた関数に対してはあまりうまくいかないのかも知れず。 C++ 可変引数テンプレートでの型リストまとめ - Faith and Brave - C++で遊ぼう C++というだけ
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
