Зависимые типы

Question

Некоторое время назад я сталкивался с языком программирования Идрисом, который «уникальной точкой продажи», по-видимому, является зависимым. Может ли кто-нибудь объяснить, что такое зависимые типы, и какую проблему они решают?

Answer 1

Ну, зависимые типы позволяют выражать инварианты типа данных, которые проверяются во время компиляции. Канонический пример для зависимых типов - это индексы с индексом длины, также известные как векторы. Определение Идриса векторов:

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

где тип Nat соответствует натуральным числам Пеано нотации:

data Nat = Z | S Nat 

Следует отметить, что, Vec A типа это то, что мы называем тип семьи: для каждого значения n : Nat мы имеют тип Vec A n, векторов длины n.

Имея длину в своем типе, некоторые функции списка могут быть правильными по конструкции. Простой примером является безопасной функцией списка:

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

Поскольку мы требуем, чтобы только непустые векторы передаются head функции - обратите внимание на показателе 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. Я этого не делал, но считаю, что все примеры этой статьи могут быть перенесены в Идрис без трудностей.