Зависимые типы. Как тип зависимых пар аналогичен несвязному объединению?

Я изучаю зависимые типы, и я понимаю следующее:

Почему универсальная квантификация представляется как зависимый тип функции. ∀(x:A).B(x) означает "для всех x типа A существует значение типа B(x)". Следовательно, он представляется как функция, которая при задании любого значения x типа A возвращает значение типа B(x).
Почему экзистенциальная квантификация представляется как тип зависимой пары. ∃(x:A).B(x) означает "существует x типа A, для которого существует значение типа B(x)". Следовательно, он представлен как пара, первым элементом которой является конкретное значение x типа A и вторым элементом которого является значение типа B(x).

Кроме того: Также интересно отметить, что универсальная квантификация всегда используется с материальной импликацией, в то время как экзистенциальная квантификация всегда используется с логической связью.

В любом случае, статья Википедии о зависимых типах утверждает, что:

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

Как получается, что тип пары (обычно это тип продукта) аналогичен несвязному объединению (который является типом суммы)? Это меня всегда путало.

Кроме того, как зависит тип зависимой функции, аналогичный типу продукта?

Ответ 1

Путаница возникает из-за использования аналогичной терминологии для структуры типа Σ и для того, как выглядят ее значения.

A значение для Σ (x: A) B (x) - пара (a, b), где a∈A и b∈B (a). Тип второго элемента зависит от значения первого.

Если мы посмотрим на структуру из Σ (x: A) B (x), то a непересекающееся объединение (копроизведение) B (x) для всех возможных x∈A.

Если B (x) постоянна (не зависит от x), то Σ (x: A) B будет просто | A | копии B, то есть A⨯B (произведение двух типов).

Если мы посмотрим на структуру of Π (x: A) B (x), то это будет произведение для B (x) для всех возможных x∈A. Его значения можно рассматривать как | A | -tuples, где a-й компонент имеет тип B (a).

Если B (x) постоянна (не зависит от x), то Π (x: A) B будет просто A → B - функциями от A до B, то есть Bᴬ (от B до A), используя обозначение теории множеств - произведение | A | копии B.

Итак, Σ (x∈A) B (x) является ковариантом | A | -а, индексированным элементами A, а П (x∈A) B (x) является | A | -иром, проиндексированным по элементы A.

Ответ 2

Зависимая пара вводится с типом и функцией от значений этого типа к другому типу. Зависимая пара имеет значения пар значения первого типа и значение второго типа, применяемого к первому значению.

data Sg (S : Set) (T : S -> Set) : Set where
  Ex : (s : S) -> T s -> Sg S T

Мы можем отбирать типы сумм, показывая, как Either канонически выражается как тип сигмы: это просто Sg Bool (choice a b), где

choice : a -> a -> Bool -> a
choice l r True  = l
choice l r False = r

- канонический выпрямитель булей.

eitherIsSg : {a b : Set} -> Either a b -> Sg Bool (choice a b)
eitherIsSg (Left  a) = Sg True  a
eitherIsSg (Right b) = Sg False b

sgIsEither : {a b : Set} -> Sg Bool (choice a b) -> Either a b
sgIsEither (Sg True  a) = Left  a
sgIsEither (Sg False b) = Right b

Ответ 3

Основываясь на Петре Пудлаке, другой угол, чтобы увидеть это чисто не зависящим образом, - заметить, что тип Either a a изоморфен типу (Bool, a). Хотя последний, на первый взгляд, продукт, имеет смысл сказать его тип суммы, так как он представляет собой сумму двух экземпляров a.

Мне нужно сделать этот пример с Either a a вместо Either a b, потому что для того, чтобы последний был выражен как произведение, нам нужны - хорошо зависимые типы.

Ответ 4

Хороший вопрос. Название могло происходить от Мартина-Лёфа, который использовал термин "декартово произведение семейства множеств" для типа pi. См. Следующие примечания, например: http://www.cs.cmu.edu/afs/cs/Web/People/crary/819-f09/Martin-Lof80.pdf Дело в том, что в то время как тип pi в принципе аналогичен экспоненте, вы всегда можете видеть экспоненту как n-арный продукт, где n - показатель степени. Более конкретно, независящую функцию A → B можно рассматривать как экспоненциальный тип B ^ A или бесконечное произведение Pi_ {a в A} B = B x B x B x... x B (A раз). Зависимым продуктом является в этом смысле потенциально бесконечное произведение Pi_ {a в A} B (a) = B (a_1) x B (a_2) x... x B (a_n) (один раз для каждого a_i в A).

Обоснование зависимой суммы может быть аналогичным, так как вы можете видеть продукт как n-мерную сумму, где n является одним из факторов продукта.

Ответ 5

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

Как получается, что тип пары (обычно это тип продукта) аналогичен несвязному объединению (который является типом суммы)? Это меня всегда путало.

Но что такое продукт, но сумма равных чисел? например 4 × 3 = 3 + 3 + 3 + 3.

То же самое относится к типам, наборам или подобным вещам. В самом деле, неотрицательные целые числа - это просто детерминирование конечных множеств. Определения сложения и умножения на числа выбираются так, чтобы мощность непересекающегося объединения множеств была суммой мощностей множеств, а мощность произведения множеств равна произведению мощностей множеств. Фактически, если вы замените "набор" на "стадо овец", это, вероятно, то, как была изобретена арифметика.

Ответ 6

Во-первых, посмотрите, что такое совлокальный продукт.

Сопутствующий продукт является терминальным объектом A для всех объектов B_i таких, что для всех стрелок B_i → X существует стрелка B_i → A и единственный A → X такой, что соответствующие треугольники коммутируют.

Вы можете просмотреть это как тип данных Haskell A с B_i → A, являющимся связкой конструкторов с единственным аргументом типа B_i. Ясно тогда, что для каждого B_i → X можно поставить стрелку из A → X таким образом, что с помощью сопоставления шаблонов вы можете применить эту стрелку к B_i, чтобы получить X.

Важным подключением к сигма-типам является то, что индекс я в B_i может быть любого типа, а не только типа натуральных чисел.

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

Разница между & Pi; и & Sigma;, как видно из ответа Петра Пудлака, это для & Sigma; некоторые из значений B_i в кортеже могут отсутствовать - для некоторого я не может быть соответствующего B_i.

Другая явная разница между & Pi; и & Sigma; что & Pi; характеризует произведение B_i, предоставляя i-й проектор из произведения & Pi; к каждому B_i (это то, что означает функция я → B_i), но & Sigma; обеспечивает стрелки в обратном направлении - он обеспечивает i-ю инъекцию из B_i в & Sigma;.