Система типов на основе теории наивных множеств

Как я понимаю, в компьютерных науках типы данных не основаны на теории множеств из-за таких вещей, как парадокс Рассела, но, как и в реальных языках программирования, мы не можем выразить такие сложные типы данных, как «множество, которое не содержит себя», можем ли мы Скажите, что на практике тип - это бесконечное множество его членов, в котором членство в экземпляре определяется числом характеристик, свойственных данному типу / набору (наличие определенных свойств, методов)? Если нет, то какой будет контрпример?

type-theory set-theory type-systems Nutel
источник

Парадокс Рассела не имеет к этому никакого отношения.

Андрей Бауэр

Ответы:

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

Чтобы быть более точным, рекурсивно определенное значение типа (где обычно является типом функции) определяется уравнением с фиксированной точкой где может быть любой программой. Если интерпретируется как множество то мы ожидаем, что каждый будет иметь фиксированную точку. Но единственным множеством с этим свойством является синглтон. $v$ $\tau$ $\tau$ $v = \Phi(v)$ $\Phi : \tau \to \tau$ $\tau$ $T$ $f : T \to T$ $T$

Конечно, вы также можете понять, что виновником является классическая логика. Если вы работаете с интуиционистской теорией множеств, то можно предположить, что существует множество множеств со свойством фиксированной точки. Фактически, это использовалось, чтобы дать семантику языка программирования, см., Например,

Алекс Симпсон, Вычислительная адекватность для рекурсивных типов в моделях теории интуиционистских множеств , В летописи чистой и прикладной логики, 130: 207-275, 2004.

Андрей Бауэр
источник

Семантический подтип основан на теоретической интерпретации типов базового множества, где подтип является подмножеством. Я полагаю, что оригинальная работа принадлежит Кастаньи в контексте языка обработки XML CDuce. Типы соответствуют наборам документов XML. Идеи с тех пор были повторно применены к калькулятору и объектам и классам исчисления . $\pi$

Дэйв Кларк
источник

Предвестники Кастаньи есть. Давным-давно люди уже использовали отношение подмножеств для моделирования подтипов в моделях PER. Там тип соответствует отношению частичной эквивалентности (PER), а подтип - это просто включение таких отношений.

Андрей Бауэр

За некоторыми исключениями (которые цитирует Дейв Кларк), простую теоретико-множественную семантику типов трудно использовать. Причина в том, что абстракция данных не очень хорошо сочетается с теоретико-множественной семантикой.

$\forall \alpha.\; \alpha \to \alpha$ $U$

[[\forall α, α \to α]] знак равно Π Икс \in U, Икс \to Икс

$[\![\forall \alpha.\; \alpha \to \alpha]\!] = \Pi X \in \mathrm{U}.\;X \to X$

$U$ $U$ $X \to X$ $X \in U$ $\alpha$

$\forall \alpha.\; \alpha \to \alpha$

Нил Кришнасвами
источник

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

Сэм Тобин-Хохштадт

Сэм, я не понимаю твою точку зрения: это звучит так, будто ты полностью согласен со мной! Стандартная теоретико-множественная семантика не может доказать, что единственным обитателем этого типа является тождество, поэтому вам нужна другая семантика.

Нил Кришнасвами

@Neel: проблема, которую вы описываете, сохраняется, даже когда мы удаляемся от сетов. Решение состоит не в том, чтобы изменить категорию множеств чем-то другим, а в том, чтобы по-другому моделировать параметричность. А именно, нужно использовать реляционную параметричность, как я уверен, вы знаете. Но тогда все складывается в сеты точно так же, если я не ошибаюсь. Единственная проблема с множествами - отсутствие фиксированных точек (как на уровне рекурсивных значений, так и рекурсивных типов).

Андрей Бауэр

Ах, я думаю, я понимаю, почему я путаю тебя и Сэма! Я, конечно, не имею в виду, что использовать наивную теоретико-множественную модель нецелесообразно, просто эта модель часто дает бесполезные ответы - вот почему я сказал «сложно использовать», а не «неправильно». Конечно, вы можете использовать наборы для построения полезной модели (т. Е. Реляционной), но тогда мы больше не будем интерпретировать типы как наборы способом, предложенным в вопросе. (Кроме того, как вы знаете, в случае с непредсказуемым полиморфизмом нет наивной модели, но параметричность все еще имеет смысл предикативно.)

Нил Кришнасвами

Я думаю, что ваша точка зрения касается соответствия между семантикой - теоретико-множественная семантика не очень подходит для полиморфизма в стиле System F, потому что она имеет невыразимые обитатели. Но это не пункт против теоретико-множественной семантики, просто утверждение, что наша семантика должна согласиться. Если наш язык позволяет нам выражать функции, о которых вы говорите (например, Typed Racket), то мы можем захотеть использовать теоретико-множественную семантику.

Сэм Тобин-Хохштадт