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

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

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

def f(arg) = result

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

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

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

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

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

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

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

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

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

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

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

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

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

Вот иллюстративный пример использования зависящих от пути типов Scala того, как мы можем попытаться реализовать функцию, fудовлетворяющую такому требованию:

case class Integer(v: Int) {
  object IsEven { require(v % 2 == 0) }
  object IsOdd { require(v % 2 != 0) }
}

def f(n: Integer)(implicit proof: n.IsEven.type) =  { 
  // do something with n safe in the knowledge it is even
}

val `42` = Integer(42)
implicit val proof42IsEven = `42`.IsEven

val `1` = Integer(1)
implicit val proof1IsOdd = `1`.IsOdd

f(`42`) // OK
f(`1`)  // compile-time error

Ключ в том, чтобы заметить, как значение nпоявляется в типе значения, proofа именно n.IsEven.type:

def f(n: Integer)(implicit proof: n.IsEven.type)
      ^                           ^
      |                           |
    value                       value

Мы говорим, что тип n.IsEven.type зависит от значения, n отсюда и термин зависимые типы .

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

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

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

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

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

Это очевидный мусор (и, вероятно, повреждает структуры данных), но он отлично справится с проверкой типов, поскольку «итератор в foo» и «итератор в бар» относятся к одному типу, IIMap::iteratorхотя они полностью несовместимы семантически.

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

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

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

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

Цитата из книги Типы и языки программирования (30.5):

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

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

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

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

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