Что зависит от ввода?

Ответ 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}

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

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

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

Ответ 2

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

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

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), является именно тем, что зависит от типа ввода.

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

Ответ 3

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

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

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

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

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

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

Ответ 4

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