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

Question

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

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

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

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

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

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

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

Answer 1

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

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

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

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

---

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

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

---

Таким образом, Σ (x∈A) B (x) есть a | A |-попродукт, индексируемый элементами A, тогда как Π (x∈A) B (x) есть a | A |-популярный продукт, проиндексированный элементами А.

Answer 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

Answer 3

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

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

Answer 4

Хороший вопрос. Название может происходить от Мартина-Лёфа, который использовал термин "декартово произведение семейства множеств" для типа "пи". См., Например, следующие заметки: 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 является одним из факторов продукта.

Answer 5

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

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

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

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

Answer 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.

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

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

Разница между Π и Σ, как видно из ответа Петра Пудлака, заключается в том, что для Σ некоторые значения B_i в кортеже могут отсутствовать - для некоторых i может отсутствовать соответствующий B_i.

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