• idris • coq • agda

все мы имеем представление о типах данных, скажем "сообщение" или "список". можно параметризовать типы значениями, что даёт возможность сказать

типы функций тогда могут принимать вид вместо более распространённого что ведёт к точным спецификациям. это и есть зависимые типы

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

с названиями зависимых типов очень все запутано. попробуем разобраться

давайте подумаем о ∃ (кванторе существования) с конструктивной точки зрения

(∃x . P x) значит "я уверен, что у меня есть (пока что - неопределенное) значение х и, ВМЕСТЕ с ним, СПОСОБ доказательства того, что для х имеет место свойство Р"

а естественным подтверждением существования х является ПАРА, состоящая из самого х и из терма, показывающего, что (Р х) выполнимо. поэтому Сигма-Типы еще называются "зависимыми парами". такая структура данных просто-таки требует, чтобы ТИП второго элемента зависел от ЗНАЧЕНИЯ первого

с точки зрения классической логики (∃x . P x) означает, что (Р х) выполняется, но только вы точно не знаете, для какого именно значения х. таким образом вы понимаете это как: наличие очень большого логического "ИЛИ" (обьединения):

         P(x0) \/ P(x1) \/ P(x2) \/ P(x3) \/ ...
а поскольку логическая операция "ИЛИ" тесно связана с типами "тэгированной суммы (обьединения)", то и Сигма-Типы иногда назвают "зависимыми суммами"

предположим, что мы говорим о логике предикатов на множестве натуральных чисел

в этом случае в формуле (∀x . P x) переменная x пробегает весь ряд натуральных чисел

в конструктивной математике вы можете сказать, что: "если мне дадут любое натруальное число x, то я смогу предьявить методу для построения обьекта с типом (P x)"

это сразу наводит на мысль о функциях, а именно - о семействе функций : 

  f : nat -> foo
  f : nat -> bar
  f : nat -> baz
       ...
  f : nat -> qux
       ...
т.е. таких, что тип результата (foo|bar|baz|...|qux|...) зависит от x (т.е. может быть и bar, и baz, и т.д. и qux и т.д.)

т.о. в конструктивной логике квантор всеобщности интерпретируется как генерализация функций. поэтому Pi-Типы еще называют "зависимыми функциональными типами"

в классической логике предикатов универсальный квантификатор (∀x . P x) означает, что вы УВЕРЕНЫ в том, что (P x) выполняется для ВСЕХ натуральных чисел. но это все равно, что сказать, что универсальный квантификатор равнозначен следующей формуле бесконечного логического "И" (пересечения): 

            P(0) /\ P(1) /\ P(2) /\ P(3) /\ ...
а поскольку операция "И" и типы "картезианского произведения" связаны, Pi-Типы часто называют "зависимым произведением"

зависимый тип B : A → Type - это на самом деле семейство типов

так вот, "произведение ∏" и "сумма ∑" - имеются в виду пересечение (произведение) и обьединение (сумма) всех типов данного семейства

например, элемент типа ∏ (x : A) B(x) - это кортеж из |A| значений типов семейства B, по одному B(x) на каждое x:A

эквивалентно выражается в виде проекций кортежа для каждого индекса x:A - функция 

    π: (x:A) → B x

элемент типа ∑ (x : A) B(x) - это элемент disjoint union значений типов семейства B. если вспомнить, как пишется disjoint union, ∏ вверх ногами, ∐, и как он определяется - как кортеж из значения и индекса, указывающего, из какого множества это значение взято, то это и есть сигма, ∑. disjoint union иногда так и записывают, через ∑, а не ∐

грубо говоря, для просто union достаточно было бы указать значение типа B(x) для некоторого x:A, а для disjoint union нужно ещё и указать само x:A, индексирующее тип из семейства B - "номер" инъекции, индекс конструктора. так что, это сумма в том же смысле, в каком disjoint union можно было бы назвать суммой множеств