Как можно мотивировать реляционную параметричность?

Есть ли какой-то естественный способ понять сущность реляционной семантики для параметрического полиморфизма?

Я только начал читать о понятии реляционной параметричности, а именно «Типах, абстракциях и параметрическом полиморфизме» Джона Рейнольдса, и у меня возникают проблемы с пониманием мотивации реляционной семантики. Семантика множеств имеет смысл для меня, и я понимаю, что семантика множеств недостаточна для описания параметрического полиморфизма, но скачок к реляционной семантике кажется волшебным, совершенно неисследованным.

Есть ли способ объяснить это следующим образом: «Предположим, отношения на базовых типах и терминах, и тогда интерпретация производных терминов - это просто естественные отношения между ... такой и такой естественной вещью ... в вашем языке программирования». «? Или какое-то другое естественное объяснение?

Что ж, реляционная параметричность - одна из самых важных идей, представленных Джоном Рейнольдсом, поэтому не стоит удивляться, что она выглядит как волшебство. Вот сказка о том, как он мог ее изобрести.

Предположим, вы пытаетесь формализовать идею о том, что определенные функции (идентичность, отображение, свертывание, обращение списков) действуют «одинаково для многих типов», т. Е. У вас есть некоторые интуитивные представления о параметрическом полиморфизме, и вы сформулировали некоторые правила для создания таких карт, т. е. полиморфного $\lambda$ исчисления или некоторого его раннего варианта. Вы замечаете, что наивная теоретико-множественная семантика не работает.

Например, мы смотрим на тип

$$\forall X : \mathsf{Type} . X \to X,$$ который должен содержать только единичное отображение, но наивная теоретико-множественная семантика допускает нежелательные функции, такие как $$\lambda X : \mathsf{Type} . \lambda a : X . \mathsf{if}\ (X = \lbrace 0, 1 \rbrace) \ \mathsf{then} \ 0 \ \mathsf{else}\ a.$$ Чтобы устранить подобные вещи, нам нужно наложить некоторые дополнительные условия на функции. Например, мы могли бы попробовать некоторую теорию предметной области: снабдить каждое множество $X$ частичным порядком $\leq_X$ и потребовать, чтобы все функции были монотонными. Но это не совсем так, потому что вышеупомянутая нежелательная функция является либо постоянной, либо тождественной, в зависимости от $X$ , и это монотонные карты.

Частичный порядок $\leq$ является рефлексивным, транзитивным и антисимметричным. Мы можем попытаться изменить структуру, например, мы могли бы попытаться использовать строгий частичный порядок, или линейный порядок, или отношение эквивалентности, или просто симметричное отношение. Однако в каждом случае появляются некоторые нежелательные примеры. Например, симметричные отношения исключают нашу нежелательную функцию, но допускают другие нежелательные функции (упражнение).

И тогда вы заметите две вещи:

1. В требуемых примеров никогда не устранены, независимо от отношения вы используете вместо частичных порядков $\leq$ .
2. Для каждого конкретного нежелательного примера, который вы просматриваете, вы можете найти отношение, которое устраняет его, но не существует единственного отношения, которое устраняет их все.

Итак, у вас есть блестящая мысль, что искомые функции - это те, которые сохраняют все отношения , и реляционная модель рождается.

Ответ на ваш вопрос действительно есть в басне Рейнольдса (Раздел 1). Позвольте мне попытаться истолковать это для вас.

В языке или формализме, в которых типы рассматриваются как абстракции , переменная типа может обозначать любую абстрактную концепцию. Мы не предполагаем, что типы генерируются с помощью некоторого синтаксиса терминов типа, или некоторого фиксированного набора операторов типа, или что мы можем проверять два типа на равенство и т. Д. В таком языке, если функция включает переменную типа, тогда единственным что функция может сделать со значениями этого типа, так это перетасовать значения, которые ей были заданы. Он не может придумать новые значения этого типа, потому что он не «знает», что это за тип! Это интуитивная идея параметричности .

Затем Рейнольдс подумал о том, как математически уловить эту интуитивную идею, и заметил следующий принцип. Предположим, что мы создаем экземпляр переменной типа, скажем, , для двух разных конкретных типов, скажем, A и A ′ , в отдельных случаях и помним некоторое соответствие R : A ↔ A ′ между двумя конкретными типами. Тогда мы можем представить, что в одном случае мы предоставляем значение x ∈ A для функции, а в другом случае соответствующее значение x ′ ∈ A ′ (где «соответствующий» означает, что x и$t$$A$$A'$$R : A \leftrightarrow A'$$x \in A$$x' \in A'$$x$ связаны с R ). Затем, поскольку функция ничего не знает о типах, которые мы предоставляем для t или значениях этого типа, она должна обрабатывать x и x ' точно так же. Таким образом, результаты, которые мы получаем из функции, должны снова соответствовать соотношению R, которое мы запомнили, т. Е. Везде, где элемент x появляется в результате одного экземпляра, элемент x ′ должен появляться в другом экземпляре. Таким образом,параметрически полиморфная функция должна сохранять все возможные реляционные соответствия между возможными экземплярами переменных типа.$x'$$R$$t$$x$$x'$$R$$x$$x'$

Эта идея сохранения соответствий не нова. Математики знали об этом давно. Во-первых, они думали, что полиморфные функции должны сохранять изоморфизмы между экземплярами типов. Обратите внимание, что изоморфизм означает некоторую идею взаимно-однозначного соответствия . По-видимому, изоморфизмы первоначально назывались «гомоморфизмами». Затем они поняли, что то, что мы сейчас называем «гомоморфизмами», т. Е. Некоторое представление о соотношениях « многие к одному» , также будет сохранено. Такое сохранение носит название естественной трансформации в теории категорий. Но, если мы думаем об этом остро, мы понимаем, что сохранение гомоморфизмов совершенно неудовлетворительно. Типы и A $A$$A'$мы упомянули совершенно произвольно. Если мы выберем качестве A ′ и A ′ в качестве A , мы должны получить то же свойство. Итак, почему «соответствие многим к одному», асимметричное понятие, должно играть роль в формулировании симметричного свойства? Таким образом, Рейнольдс сделал большой шаг в обобщении от гомоморфизмов к логическим отношениям, которые представляют собой соответствия « многие ко многим» . Полное влияние этого обобщения еще не полностью понято. Но основная интуиция довольно ясна.$A$$A'$$A'$$A$

Здесь есть еще одна тонкость. В то время как экземпляры переменных типов могут произвольно варьироваться, константные типы должны оставаться фиксированными. Таким образом, когда мы формулируем реляционную корреспонденцию для выражения типа с обоими типами переменных и постоянных типов, мы должны использовать выбранное соотношение везде , где появляется переменная типа и тождественное соотношение I K везде , где константа типа K появляется. Например, выражение отношения для типа t × I n t → I n t × t будет иметь вид R × I I n t → I $R$$I_K$$K$$t \times Int \to Int \times t$. Таким образом, еслиfявляется функцией этого типа, она должна отобразить пару(x,n)и связанный( x ′ ,n)с некоторой парой(m,x)и связанным(m, x ′$R \times I_{Int} \to I_{Int} \times R$$f$$(x,n)$$(x',n)$$(m,x)$$(m,x')$, Обратите внимание, что мы обязаны проверить функцию, поместив одинаковые значения для константных типов в обоих случаях, и мы гарантированно получим одинаковые значения для константных типов в выходных данных. Таким образом, при формулировании реляционных соответствий для выражений типов мы должны убедиться, что, подключив идентичные отношения (представляющие идею, что эти типы будут согласованными), мы получим обратно идентичные отношения, то есть . Это важнейшее расширение личности$F(I_{A_1},\ldots,I_{A_n}) = I_{F(A_1,\ldots,A_n)}$ свойство.

Чтобы понять параметричность интуитивно, все, что вам нужно сделать, - это выбрать некоторые типы функций семплов, подумать о том, какие функции могут быть выражены для этих типов, и подумать о том, как эти функции ведут себя, если вы подключаете различные экземпляры переменных типа и разные значения этих функций. типы экземпляров. Позвольте мне предложить несколько типов функций для начала работы: , t → I n t , I n t → t , t × t → t × t , ( t → t ) → t , ( $t \to t$$t \to Int$$Int \to t$$t \times t \to t \times t$$(t \to t) \to t$ .$(t \to t) \to (t \to t)$

$\omega$

Кроме того, заманчиво отождествлять функции с одинаковым экстенсиональным поведением, что приводит к отношению эквивалентности. Отношение является частичным, если мы исключаем «неопределенные» функции, то есть функции, которые «зацикливаются» для некоторого правильно сформированного ввода.

Модели PER являются обобщением этого.

Другой способ увидеть эти модели как (очень) особый случай моделей симплициальных множеств в теории гомотопического типа . В этой структуре типы интерпретируются как (обобщение) наборов с отношениями и отношений между этими отношениями и т. Д. На самом низком уровне у нас просто есть модели PER.

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