Суммы и произведения
Не понимаю, почему в теориях зависимых типов сигмы называют суммами, а пи называют произведениями, и почему вообще были использованы эти греческие буквы. Очевидно же, что сигмы, т.е. зависимые пары, это произведения, а пи, т.е. функции, -- экспоненты, пусть и какие-то корявые. Может, там кто-то типы прологарифмировал?
Категорные лимит и колимит всё объясняют - и что это за обозначения, и каков у них смысл. (Как там размышлял настоящий изобретатель этих обозначений - неважно; но категорное объяснение толкует неплохо.)
Лимит - это такой объект диаграммы, в который есть уникальная стрелка из всех конусов диаграммы, и при этом диаграмма коммутирует. Это обобщение проекций тупля.
Так, X - это произведение нескольких типов, если из X существуют стрелки во все типы, на которые "опирается" конус. По идее можно было бы стрелки (проекции) пронумеровать, но в общем виде их индексируют некоторым сетоидом. Ну и запись Πx:AB(x) однозначным образом описывает такой тип и все возможные стрелки из него. Взят символ произведения Π по той причине, что любой объект A можно представить в виде произведения с 1: A ≡ A×1, поскольку из любого объекта есть стрелка в себя и в терминальный объект 1 (а также A является терминальным среди всех конусов, опирающихся на A и 1).
Колимит - это такой объект диаграммы, из которого есть уникальная стрелка во все ко-конусы диаграммы, и при этом диаграмма коммутирует. Это обобщение нескольких конструкторов одного типа.
Так, Y - это сумма нескольких типов, если в Y существуют стрелки изо всех типов, на которые "опирается" коконус. Можно было бы стрелки (инъекции) пронумеровать, но в общем виде их индексируют некоторым сетоидом. Соответственно, запись Σx:AB(x) однозначным образом описывает тип и все возможные стрелки в него. Символ суммы Σ по той причине, что любой объект A можно представить в виде суммы с 0: A ≡ A+0, поскольку в любой объект есть стрелка из себя и из инициального объекта 0.
data Stream a = S {head :: a} {tail :: Stream a} -- произведение типов a и Stream a, описываемое стрелками head :: Stream a -> a и tail :: Stream a -> Stream a
Тогда Π-тип - это функция, позволяющая выбрать либо head, либо tail с помощью некоторого типа-индекса (и скрывает Stream a "внутри").
data Nat = Zero | Succ Nat -- сумма типов () и Nat, описываемая стрелками Zero : () -> Nat и Succ : Nat -> Nat
Тогда Σ-тип - это результат функции, которая некоторым образом выбрала одну из инъекций - один из конструкторов, и передала этому конструктору значение нужного типа.
Разложение Σ на проекции - вопрос чисто технический; это тупль на уровне, на котором категория не оперирует, т.е. произведение не в том же смысле, в каком произведением является A×B. Это всего-лишь 2×Y, никакого произвола с выбором индекса проекций.
Reply
Leave a comment