Abhängige Typen

Question

Vor einiger Zeit stoße ich auf die Programmiersprache Idris, die als "Alleinstellungsmerkmal" abhängige Typen zu sein scheinen. Kann jemand erklären, welche abhängigen Typen sind und welche Art von Problem sie angehen?

Answer 1

Nun, abhängige Typen können Datentyp-Invarianten ausdrücken, die während der Kompilierungszeit überprüft werden. Das kanonische Beispiel für abhängige Typen sind die längenindexierten Listen, die auch als Vektoren bezeichnet werden. Die Idris Definition von Vektoren ist:

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

wo Typ Nat auf natürliche Zahlen in Peano Notation entspricht:

data Nat = Z | S Nat 

anzumerken, dass Vec A Typ ist, was wir eine Art Familie nennen: für jeden Wert n : Nat wir habe einen Typ , von Vektoren der Länge n.

Die Länge in ihrem Typ ermöglicht es, dass einige Listenfunktionen durch die Konstruktion korrekt sind. Ein einfaches Beispiel ist eine Liste sichere Kopffunktion:

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

Da wir fordern, dass nur nicht-leeren Vektoren head Funktion übergeben werden - beachten Sie den Index S n Anforderungen Nicht-Null-Werte - Idris Compiler garantiert, dass Kopf nie sein auf leere Listen angewendet.

Anderes Beispiel ist Verkettung von Vektoren, die sicherstellt, dass die Ergebnisse Länge der Summe seines Parameter Länge gleich haben:

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

beachten, dass die Verkettungs Länge Eigenschaft durch Verkettung Funktionstyp gewährleistet ist. Andere Anwendung ist zu beweisen, dass traditionelle Kartenfunktion auf Vektor bewahrt seine Länge:

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

Auch die Vektor-Länge Erhaltung von map Typenannotation gewährleistet ist. Dies sind sehr einfache Beispiele dafür, wie abhängige Typen helfen, eine korrekte Konstruktionssoftware zu gewährleisten.

Weitere überzeugende Beispiele für abhängige Typ-Programmierung (mit Agda Programmiersprache) finden Sie in The Power of Pi. Ich habe das nicht getan, aber ich glaube, dass alle Beispiele dieses Papiers ohne Schwierigkeiten auf Idris übertragen werden können.