Что такое зависимая типизация?

Question

Может кто-нибудь объяснить мне зависимую типизацию?У меня мало опыта работы с Haskell, Cayenne, Epigram или другими функциональными языками, поэтому чем проще использовать термины, тем больше я это ценю!

Answer 1

Учтите это: на всех приличных языках программирования вы можете писать функции, например,

def f(arg) = result

Здесь f принимает значение arg и вычисляет значение result. Это функция от значений к значениям.

Теперь, некоторые языки позволяют вам определять полиморфные (или универсальные) значения:

def empty<T> = new List<T>()

Здесь empty принимает тип T и вычисляет значение. Это функция от типов к значениям.

Обычно вы также можете иметь определения общего типа:

type Matrix<T> = List<List<T>>

Это определение принимает тип и возвращает тип. Его можно рассматривать как функцию от типов к типам.

Так много для того, что предлагают обычные языки. Язык называется зависимо типизированным, если он также предлагает 4-ю возможность, а именно определение функций от значений до типов. Или, другими словами, параметризация определения типа по значению:

type BoundedInt(n) = {i:Int | i<=n}

Некоторые основные языки имеют некоторую поддельную форму, которую не следует путать. Например. в C ++ шаблоны могут принимать значения в качестве параметров, но при применении они должны быть константами времени компиляции. Не так на действительно зависимом языке. Например, я мог бы использовать вышеупомянутый тип как это:

def min(i : Int, j : Int) : BoundedInt(j) =
  if i < j then i else j

Здесь тип результата функции зависит от фактического значения аргумента j, то есть от терминологии.

Answer 2

Если вы знаете C ++, легко привести мотивирующий пример:

Допустим, у нас есть некоторый тип контейнера и два его экземпляра

typedef std::map<int,int> IIMap;
IIMap foo;
IIMap bar;

и рассмотрим этот фрагмент кода (выможет предполагать, что foo не пусто):

IIMap::iterator i = foo.begin();
bar.erase(i);

Это очевидный мусор (и, вероятно, повреждает структуры данных), но он прекрасно проверит тип, так как "итератор в foo" и "итератор вbar "одного типа, IIMap::iterator, даже если они семантически несовместимы.

Проблема в том, что тип итератора должен зависеть не только от контейнера type , но на самом делев контейнере объект , т. е. это должен быть «нестатический тип элемента»:

foo.iterator i = foo.begin();
bar.erase(i);  // ERROR: bar.iterator argument expected

Такая функция, возможность выражать тип (foo.iterator), которыйзависит от термина (foo), это именно то, что означает зависимая типизация.

Причина, по которой вы не часто видите эту функцию, заключается в том, что она открывает большую банку с червями: вы неожиданно попадаете в ситуации, когдапроверить во время компиляцииНезависимо от того, являются ли два типа одинаковыми, вам в конечном итоге придется доказать, что два выражения эквивалентны (всегда будет давать одно и то же значение во время выполнения).В результате, если вы сравните список википедии с зависимой типизацией со списком доказательств теорем , вы можете заметить подозрительное сходство.; -)

Answer 3

Зависимые типы позволяют устранить больший набор логических ошибок во время времени компиляции . Чтобы проиллюстрировать это, рассмотрим следующую спецификацию функции f:

Функция f должна принимать только даже целых чисел в качестве входных данных.

Без зависимых типов вы можете сделать что-то вроде этого:

def f(n: Integer) := {
  if  n mod 2 != 0 then 
    throw RuntimeException
  else
    // do something with n
}

Здесь компилятор не может определить, является ли n действительно четным, то есть, с точки зрения компилятора, следующее выражение в порядке:

f(1)    // compiles OK despite being a logic error!

Эта программа будет запускаться, а затем генерировать исключение во время выполнения, то есть в вашей программе будет логическая ошибка.

Теперь зависимые типы позволяют вам быть более выразительными и позволяют писать что-то вроде этого:

def f(n: {n: Integer | n mod 2 == 0}) := {
  // do something with n
}

Здесь n имеет зависимый тип {n: Integer | n mod 2 == 0}. Это может помочь прочитать вслух как

n является членом набора целых чисел, так что каждое целое число делится на 2.

В этом случае компилятор обнаружит во время компиляции логическую ошибку, когда вы передали нечетное число в f, и в первую очередь предотвратит выполнение программы:

f(1)    // compiler error

Answer 4

Цитирование книги «Типы и языки программирования» (30,5):

Большая часть этой книги была посвящена формализации абстракции механизмы разных видов. В простом наборе лямбда-исчисления мы формализовал операцию взятия термина и абстрагирование субтерм, давая функцию, которая может быть позже создана применяя это к разным условиям. В Системе F мы рассмотрели операция взятия термина и абстрагирования типа с получением термина это может быть реализовано путем применения его к различным типам. В λω мы Перечислим механизмы простейшего лямбда-исчисления «один уровень вверх », принимая тип и абстрагируя подвыражение, чтобы получить оператор типа, который позже можно создать, применив его к Различные типы. Удобный способ мышления всех этих форм абстракция в терминах семейств выражений, проиндексированных другими выражения. Обычная лямбда-абстракция λx:T1.t2 - это семейство условия [x -> s]t1 проиндексированы условиями s. Аналогично, абстракция типа λX::K1.t2 - это семейство терминов, проиндексированных по типам, и оператор типа семейство типов, проиндексированных по типам.

• λx:T1.t2 семейство терминов, проиндексированных по терминам

• λX::K1.t2 семейство терминов, проиндексированных по типам

• λX::K1.T2 семейство типов, проиндексированных по типам

Глядя на этот список, становится ясно, что есть одна возможность мы еще не рассмотрели: семейства типов индексируются по срокам. это форма абстракции также широко изучалась в рамках рубрика зависимых типов.