К типизации лямбды с зависимыми типами (2)

[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() возвращает число элементов в множестве ;-)

Comments

[thesz.livejournal.com]

Вот насчет exponentation - можно поподробней?

Я не понимаю, откуда вылезает N^M.

[deni-ok.livejournal.com]

Смотри: A={a1,a2,...,am} - домен (область определения), B={b1,b2,...,bn} - кодомен (мн-во значений). Всевозможные упорядоченные пары образуют матрицу элементов вида (ai,bj), в ней m*n элементов. Чтобы задать некоторую функцию f, мы должны каждому элементу домена сопоставить единственный элемент кодомена, то есть из каждой строки этой матрицы выбрать ровно одну пару:

f={(a1,bкакая-то),(a2,bсякая-то),...,(an,bнекоторая)}

Сколькими способами можно это сделать? Пару a1 можно выбрать n способами (столько у нас разных b-шек); для каждого такого выбора пару a2 можно выбрать тоже n способами, и т.д (m раз). Получаем

n*n*n*...*n=n^m

штук различных функций можем смонтировать над заданными доменом и кодоменом.

[zelych.livejournal.com]

По поводу "глубокой философии в терминах".

Где-то я слышал, что этимология примерно такова:
- Π является типом для ∀-выражений. Предикат ∀a:A.B_a можно представить как коньюнкцию B_a0∧B_a1∧B_a2∧...
∧ можно сравнить с произведением (в каком контексте, сказать не могу. В булевом кольце and вроде как произведение, но там с коньюнкцией нестыковка. Можно представить and и or как операции над множествами, но я не знаю как эта модель называется). Ну так вот, ∧ соответствует произведению, поэтому Π-тип называют зависимым произведением (dependent product);

- Σ — вроде как, тип для ∃-выражений. Предикат ∃a:A.B_a можно представить как B_a0∨B_a1∨B_a2∨...
∨ является аналогом суммы, поэтому Σ-тип называют зависимой суммой (dependent sum).

Если элементов в A слишком много, то коньюнкции и дизьюнкции получаются бесконечными. Не конструктивно.
Ходят легенды, что в стане интуиционистов Π и Σ-типы назывались иначе:
- с конструктивной точки зрения, предикат ∀a:A.B_a говорит о том, что у нас есть способ построения объекта B_a для каждого объекта a∈A. Т.е. есть некоторая функция из A в B_a. А Πa:A.B_a — обобщение функционального типа. Поэтому его называют зависимым функциональным типом dependent function type;

- ∃a:A.B_a значит, что у нас есть пара: объект a∈A и объект B_a (который мы смогли построить из а). Поскольку пара является элементом произведения двух множеств, то Σ-тип называют зависимым произведением dependent product (ага, в первом варианте было совсем наоборот).

Вроде, как-то так.

[deni-ok.livejournal.com]

Ага, спасибо, полезное дополнение