От теории множеств к теории типов

[deniok]

От теории множеств к теории типов. Хорошая вводная статья Майка Шульмана о том, почему именно теорию типов стоит положить в основания математики. Ну немножко философского характера, конечно, но тематика обязывает. Настоятельно рекомендую, спасибо alexey_rom за ссылку.

Comments

[nivanych.livejournal.com]

> а как тогда сказать, что X is X×1?

"X is" это оборот речи, а "изоморфен" — строгое определение! ;-)
То есть, зависит от того, что понимается под "is".

> которые можно взять за проекции в 1 и X

Проекции _из_ произведения, а не в него!
Для любого X существуют морфизмы, которые можно взять за проекции 1 ← 1×X → X

> А как мы можем отличить,
> у кого X слева, а у кого - справа?

Если мы собираемся все конструкции производить "по модулю" изоморфизма, тогда придётся как-то по-другому определять произведение. Способы подсказывает классическая теория множеств, впрочем.
Но на мой взгляд, лучше смириться с тем, что не всегда бывает удобно отождествлять изоморфное.

[sassa-nf.livejournal.com]

"Проекции _из_ произведения, а не в него!"

ага, я это и хотел сказать - проекции в 1 и в X (поотдельности)


"Если мы собираемся все конструкции производить "по модулю" изоморфизма, тогда придётся как-то по-другому определять произведение. Способы подсказывает классическая теория множеств, впрочем.
Но на мой взгляд, лучше смириться с тем, что не всегда бывает удобно отождествлять изоморфное."

да я бы и рад не отождествлять :)

про "слева" и "справа" я расспрашиваю исключительно потому, что раз пишем X×Y ≈ Y×X, то имеем в виду..........просто, что они разные? Я не пойму, как можно "направленность" определить, раз объекты не тождественные.

Примерно так:

когда в х-е пишем fst, то, конечно, легко видеть, что существенна "направленность" - кто там первый X или Y. Но в теор кате стрелки из одного объекта не имеют отношения к стрелкам из другого объекта, т.е. нет способа выразить "полиморфные" стрелки fst, которые делают что-то там одинаково. Или такой способ есть?

Для себя я объясняю эту разницу тем, что на самом деле в х-е fst работает не с прямо объектами X×Y, а с изоморфными им объектами Pair, построенными конструктором (Pair^Y)^X - а вот здесь уже порядок X и Y можно определить из порядка eval.

[nivanych.livejournal.com]

> раз пишем X×Y ≈ Y×X, то имеем в виду..........
> просто, что они разные?

Когда так пишут, это дословно означает, что существует изоморфизм. Вне зависимости от того, разные они там или одинаковые.

> когда в х-е пишем fst

Ну так и в категориях есть первая и вторая проекции.
Если не стараться отождествлять изоморфное, то и различать запросто.

> Но в теор кате стрелки из одного объекта
> не имеют отношения к стрелкам из другого объекта,

Если эти два объекта изоморфны, то имеет же.
Можно просто и тупо делать композицию с этим изоморфизмом.

> т.е. нет способа выразить "полиморфные" стрелки fst,
> которые делают что-то там одинаково.

Функтор произведения имеет соответствующие свойства, что создаёт соответствующие "вспомогательные" стрелки.

В хацкеле с категорной семантикой мутновато. Но в довольно хорошем первом приближении, можно считать, что пары, это такие "хитрые" начальные алгебры.

[sassa-nf.livejournal.com]

"Ну так и в категориях есть первая и вторая проекции."

хм. я думал из определения следует "одна и другая" проекции :) типа как здесь: - я не знаю, означает ли это, что порядок у I есть? если порядок есть, то тогда понятно.


"Можно просто и тупо делать композицию с этим изоморфизмом."

но тогда не ясно, как это отличается от композиции с snd вместо fst :)

ок, пора почитать про произведение заданное через функтор.

[nivanych.livejournal.com]

> порядок у I есть?
> если порядок есть, то тогда понятно.

Скажем так — порядка нет, но это setoid.
То есть, элементы индексов мы можем отличать друг от друга.
И естественно, что конечное множество (мы вообще говорили о двух элементах) мы вполне можем вполне упорядочить, но в данном случае, это не важно.
Есть элемент i есть элемент k. Вот и будет говорить об i-й проекции и k-й проекции, не упорядочивая множество индексов.

[sassa-nf.livejournal.com]

вот я так себе и представлял. А отсюда следует, что и у X×Y, и у Y×X один и тот же сетоид используется? Если нет, то хотя мы и можем выбрать i-ю проекцию X×Y, может у Y×X её и нет вообще?

[nivanych.livejournal.com]

Из записи XxY не следует какое-то представление индексов, а только то, что их два штук.
Несколько образно, индексами мы обозначаем места, куда можно что-то "положить".
Так вот, если есть два индекса x и y, то мы на место x можем "положить" Y, а можем и X, например.

Декартово произведение задаёт с собой сразу и проекции. Это хорошее такое произведение.
Но не каждое моноидальное произведение позволяет потом "раздербанить" произведение по составляющим.

[sassa-nf.livejournal.com]

"Из записи XxY не следует какое-то представление индексов, а только то, что их два штук."

да, я это понимаю. я пытаюсь понять, "направленность" у X×Y "глобально видима" или как? То есть, "какое-то представление индексов" понятно.

Я оба произведения понимаю, и понимаю, почему изоморфны. Я не знаю наверняка, существенно ли, что Y×X пишется в обратном порядке. Это просто запись такая, чтобы не выглядело тавтологично "X×Y ≈ X×Y"? Или есть способ выделить "направленность" и для каких-то двух объектов можно выяснить, что они одинаковой "направленности"?

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

[nivanych.livejournal.com]

> выяснить "направленность"

Исходя из каких данных выяснить?
Произведение уже направлено по определению — есть две различимых проекции, составляется произведение тоже вполне так "направленно".
Принято в n-арном произведении всякое умножаемое писать упорядоченной цепочкой типа XxYxZxTxUxV или (X,Y,Z,T,U,V). И то, что отдаст первая проекция, принято писать слева. Соответственно, отличать XxY от YxX, если как-то отличаем X и Y.
Тем не менее, в категорном, достаточно часто выписывают проекции явно, тем самым, устраняя ещё одну возможность неоднозначности понимания. И это хорошо, как правило.

[sassa-nf.livejournal.com]

Я не знаю, как уточнить свой вопрос. Пока что понятно не стало.

"Исходя из каких данных выяснить?"

ага, это мой вопрос.


"Произведение уже направлено по определению"

блин, ну, как же направлено, если проекции индексируются сетоидом I. Я понимаю, что можно записать сетоид в виде списка. Я понимаю, что сетоида достаточно, чтобы знать, как применить проекцию.

давайте попробую ещё раз по частям.

∏{X}_{i,j} и ∏{X}_{i,k}

1. это произведения одного и того же X_i и разных X_j, X_k? или в каждом случае i - просто индекс, а потому X_i первого не обязательно X_i второго? Типа как в арифметике запись ΣX_i i не означает ничего, кроме способа выбрать X_i в этой одной сумме, и не означает, что в двух разных записях X_i references одно и то же значение.

2. если X_i в обоих записях означает один и тот же X_i, то что задаёт порядок i в сетоиде, ...кроме договорённости записывать i, j, k в алфавитном порядке.

3. Я сейчас считаю, что ∏{X}_{i,j} эквивалентно записи X_i×X_j и эквивалентно записи X_j×X_i, поскольку порядок i, j отсутствует. Откуда тогда следует направленность произведения?

[nivanych.livejournal.com]

> проекции индексируются сетоидом I.

Строго говоря, классические проекции индексируются дискретной категорией (в которой стрелки только единичные).
И произведение, это предел некоторого функтора из этой категории.
Какие претензии к этом определению? ;-)

А касаемо вопросов — это должно быть всегда ясно из контекста.
Если не ясно, значит херово написали.