Есть типы предложений? (Какие именно типы?)

25

Я много читал о системах типов и тому подобное, и я примерно понимаю, почему они были введены (чтобы разрешить парадокс Рассела). Я также примерно понимаю их практическую значимость в языках программирования и системах доказательства. Однако я не совсем уверен, что мое интуитивное представление о типе является правильным.

У меня вопрос, действительно ли утверждение, что типы - это предложения?

Другими словами, утверждение «n является натуральным числом» соответствует утверждению «n имеет тип« натуральное число »», означающее, что все алгебраические правила, которые включают натуральные числа, выполняются для n. (То есть, с другой стороны, алгебраические правила - это утверждения. Те утверждения, которые верны для натуральных чисел, верны и для n.)

Значит ли это, что математический объект может иметь более одного типа?

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

Есть ли какая-то связь с теорией категорий?

Рено Линдек
источник
5
Тесно связанный вопрос: Доказательства / Программы и предложения / Типы
Марк Хаманн,
1
Другая связанная с этим дискуссия: классификация лямбда-исчислений
Марк Хаманн,
Нашел еще одну хорошую статью здесь scientopia.org/blogs/goodmath/2009/11/17/…
Рено Линдек,
1
В некотором смысле это сводится к вопросу онтологии. Что такое множество, суждение и т. Д. Кроме того, многие люди думают о типах как о множествах. Если кто-то хочет быть более точным, можно различить маленькие типы (которые являются наборами) и типы вселенных. Для хорошего прочтения, касающегося некоторых вещей, я рекомендую классическую статью Мартина-Лёфса «Интуиционистская теория типов»
Тобиас Раски,
1
Кто-то должен написать ответ с точки зрения теории гомотопического типа.
Робин Грин

Ответы:

20

Ключевая роль типов заключается в разделении объектов, представляющих интерес, на различные вселенные, а не на рассмотрение всего, что существует в одной вселенной. Изначально типы создавались так, чтобы избежать парадоксов, но, как вы знаете, они имеют множество других применений. Типы предоставляют способ классификации или стратификации объектов (см. Запись в блоге ).

Некоторые работают с лозунгом, согласно которому предложения являются типами , поэтому ваша интуиция, безусловно, служит вам хорошо, хотя есть работа, такая как « Предложения как [Типы » »Стива Аводи и Андрея Бауэра, которая утверждает иначе, а именно, что у каждого типа есть ассоциированное предложение. Различие проводится потому, что типы имеют вычислительное содержание, а предложения - нет.

Объект может иметь более одного типа из-за подтипирования и приведения типов .

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

Существует очень сильная связь между типами и теорией категорий. Действительно, Боб Харпер (цитирует Ламбека) говорит, что логика, языки (где находятся типы) и категории образуют святую троицу . Цитирование:

Эти три аспекта порождают три секты поклонения: логика, которая дает первенство доказательствам и суждениям; Языки, которые отдают приоритет программам и типам; Категории, которые отдают приоритет отображениям и структурам.

Чтобы увидеть связь между теорией категорий, вам следует обратиться к переписке Карри-Ховарда, чтобы увидеть связь между языками логики и языков программирования (типы являются предложениями) и декартовыми закрытыми категориями .

Дэйв Кларк
источник
Спасибо, первая ссылка была особенно полезной! В нем Марк сообщает, что существует «общее отношение <» по типам. Значит ли это, что все «предложения» типа должны также включать все «предложения» в типы ниже них? Я ожидал, что это будет, по крайней мере, "частичное отношение <" над типами ....
Рено Линдек,
1
Насколько я понимаю, существует полный порядок по атомам, который был создан только для того, чтобы обеспечить бесконечное количество атомов.
Дейв Кларк,
О, я вижу, я запутался между "Аксиомой Понимания" и "Аксиомой бесконечности" ... Будет ли тип "nat" (тип всех натуральных чисел) быть "типом бесконечного уровня 0"?
Рено Линдек
3
«Святая троица» действительно принадлежит Ламбеку. Ср обсуждение теории типов в Lambek & Scott (1986). Я слышал, что в МакГилле говорят о переписке Карри-Говарда-Ламбека.
Чарльз Стюарт
@Charles: Я согласен, что Ламбек недооценивается за его огромный вклад, даже если, по иронии судьбы, именно чтение книги Ламбека и Скотта убедило меня в том, что «святая троица» является фиктивной: она разрушается в присутствии потенциальных -termination.
Марк Хаманн