deniok

Отталкиваясь от полученной в прошлом посту просьбы, попытаюсь рассказать о Σ-типах.

Напомню, что Π-абстракция аналогична λ-абстракции, но производит не терм (зависящий от связанной абстракцией переменной), а тип (зависящий от связанной абстракцией переменной). В прошлом посту мы рассматривали терм a:A, который параметризовал семейство типов Ba - нижний индекс указывает на зависимость типа от терма. Если рассматривать функцию, принимающую значение типа A и возвращающую некоторого представителя ba:Ba, то получившаяся лямбда

 
(λa:A.ba)

не может быть типизирована в обычной стрелочной нотации; способ

 
(λa:A.ba):(A → Ba)

плох, поскольку не позволяет пометить связанность переменной a в типе. Решением и является Π-абстракция:

 
(λa:A.ba):(Πa:A.Ba)

В примере с типом списка заданной длины (см. предыдущий пост)

 
(λn:Nat.replicate 'z' n):(Πn:Nat.ListOfChar n)

Сам по себе знак Π описывает индексированное произведение типов. Когда тип B не зависит от термов типа A, Π-абстракция эквивалентна обычной функциональной стрелке

 
Πa:A.B ≡ B^A ≡ (A → B)

Здесь функция для каждого значения a:A возвращает один и тот же тип B. Обозначение со степенью как раз и является маркером произведения. Чтобы задать функцию из типа A нам нужно задать возвращаемое значения одного и того же типа (B) столько раз, сколько "населения" есть в типе A. В общем, "зависимом", случае каждый сомножитель Ba уникален и запись со степенью (или стрелкой) не проходит.

Предположим теперь, что мы хотим типизировать не функцию от a:A, у которой тип результата зависит от значения a, а пару, первым элементом которой служит значение a:A, а вторым значение ba:Ba с типом, зависящим от значения первого элемента пары. Наивная попытка типизации такой пары:

 
(a:A, ba:Ba):(A,Ba)

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

 
(a:A, ba:Ba):(Σa:A.Ba)

Происхождение значка суммы легко понять, посмотрев на простейший случай отсутствия зависимости. Если тип B не зависит от термов типа A, Σ-абстракция эквивалентна обычному декартову произведению

 
Σa:A.B ≡ A × B

Это отражает тот факт, что B берется столько раз, сколько элементов в A. Что, как и следовало ожидать, совпадает с типом обычной, не-зависимой пары.

PS. Не следует искать глубокой философии в терминах сумма и произведение. Простая мнемоника груба, но действенна: пар из типов A и B мы можем образовать m(A)*m(B) штук, а функций из A в B - m(B)^m(A) штук, где m() возвращает число элементов в множестве ;-)