従属型

Question

私は「ユニークなセールスポイント」が依存型のように見えるプログラミング言語Idrisに遭遇しました。どのような依存型があるのか​​、どのような問題に取り組んでいるのかを誰かが説明できますか？

Answer 1

まあ、依存型は、コンパイル時にチェックされるデータ型不変量を表現することを可能にします。従属型の標準的な例は、ベクトルとも呼ばれる長さインデックス付きのリストです。ベクトルのイドリス定義は次のとおりです。

data Vec (A : Type) : Nat -> Type where 
    Nil : Vec A 0 
    Cons : A -> Vec A n -> Vec A (S n) 

タイプ Natはペアノ表記で自然数に対応

：Vec Aタイプは、我々はタイプファミリー呼んでいる、

data Nat = Z | S Nat 

注：各値n : Natのために我々タイプVec A n、長さがnのベクトルである。

長さがその型であることにより、構造によっていくつかのリスト関数が正しいことが可能になります。我々は唯一の非空のベクトルがhead関数に渡されることを要求するので

head : Vec a (S n) -> a 
head (x :: xs) = x 

ヘッドはなることはありませんことをイドリスコンパイラの保証 - - 非ゼロ値のインデックスにS n需要の点に注意してください。簡単な例では、セーフリストの先頭機能です空のリストに適用されます。連結長プロパティが連結機能の種類によって保証されること

(++) : Vec a n -> Vec a m -> Vec a (n + m) 
[] ++ ys = ys 
(x :: xs) ++ ys = x :: (xs ++ ys) 

注

他の例では、その結果がそのパラメータの長さの和に等しい長さを有することを確実にベクターの連結です。

map : (a -> b) -> Vec a n -> Vec b n 
map f [] = [] 
map f (x :: xs) = f x :: map f xs 

ここでも、ベクトル長の保存がmap型注釈によって保証される：他のアプリケーションは、ベクター上の伝統的なマップ機能は、その長さを保持することを証明することです。これらは、従属型がどのように建設ソフトウェアによって正しいことを保証するのに役立つかの非常に簡単な例です。

依存型プログラミング（Agdaプログラミング言語を使用）のもっと説得力のある例は、The Power of Piにあります。私はこれをしていないが、私はこの論文のすべての例が困難なしでIdrisに移植できると信じている。