Полиморфизм строк - Row polymorphism

В язык программирования теория типов, полиморфизм строк - это разновидность полиморфизм что позволяет писать программы, полиморфные на записывать типы полей (также известные как строки, отсюда полиморфизм строк). Строка-полиморфная система типов и доказательство вывода типов были введены Митчелл Палочка.^[1][2]

Записи и типы записей

Значение записи записывается как ${\displaystyle \{\ell _{1}=e_{1},\dots ,\ell _{n}=e_{n}\}}$, где запись содержит ${\displaystyle n}$ поля (столбцы), ${\displaystyle \ell _{i}}$ - поля записи, и ${\displaystyle e_{i}}$ - значения поля. Например, запись, содержащая трехмерную декартовую точку, может быть записана как ${\displaystyle Point3d=\{x=1,y=2,z=3\}}$.

Строчный полиморфный тип записи записывается как ${\displaystyle \{\ell _{1}:T_{1},\dots ,\ell _{n}:T_{n},{\text{absent}}(f_{1}),\dots ,{\text{absent}}(f_{m}),\rho \}}$, где возможно ${\displaystyle n=0}$ или же ${\displaystyle m=0}$. Запись ${\displaystyle r}$ имеет строковый полиморфный тип записи всякий раз, когда поле записи ${\displaystyle \ell _{i}}$ имеет тип ${\displaystyle T_{i}}$ (за ${\displaystyle i=1\dots n}$) и не имеет ни одного из полей ${\displaystyle f_{j}}$ (за ${\displaystyle j=1\dots m}$). Строка-полиморфная переменная ${\displaystyle \rho }$ выражает тот факт, что запись может содержать другие поля, кроме ${\displaystyle \ell _{i}}$.

Строковые полиморфные типы записей позволяют нам писать программы, которые работают только с частью записи. Например,${\displaystyle {\text{transform2d}}:\{x:{\text{Float}},y:{\text{Float}},\rho \}\to \{x:{\text{Float}},y:{\text{Float}},\rho \}}$ функция, выполняющая какое-то двумерное преобразование. Из-за полиморфизма строк функция может выполнять двумерное преобразование трехмерного (фактически, п-мерной) точки, оставляя z координаты целы. Более того, функция может работать с любой записью, содержащей поля ${\displaystyle x}$ и ${\displaystyle y}$ с типом ${\displaystyle {\text{Float}}}$. Обратите внимание, что не было потери информации: тип гарантирует, что все поля, представленные переменной ${\displaystyle \rho }$ присутствуют в возвращаемом типе.

Полиморфизмы строк могут быть ограничены. Тип ${\displaystyle \{x:{\text{Float}},y:{\text{Float}},\mathbf {empty} \}}$ выражает тот факт, что запись этого типа имеет точно ${\displaystyle x}$ и ${\displaystyle y}$ поля и больше ничего. Таким образом, получается классический тип записи.

Операции ввода с записями

Запись операций выбора поля ${\displaystyle r.\ell }$, добавив поле, ${\displaystyle r[\ell :=e]}$ и удаление поля ${\displaystyle r\backslash \ell }$ могут быть заданы строково-полиморфные типы.

${\displaystyle \mathrm {select_{\ell }} =\lambda r.(r.\ell )\;:\;\{\ell :T,\rho \}\rightarrow T}$

${\displaystyle \mathrm {add_{\ell }} =\lambda r.\lambda e.r[\ell :=e]\;:\;\{\mathrm {absent} (\ell ),\rho \}\rightarrow T\rightarrow \{\ell :T,\rho \}}$

${\displaystyle \mathrm {remove_{\ell }} =\lambda r.r\backslash \ell \;:\;\{\ell :T,\rho \}\rightarrow \{\mathrm {absent} (\ell ),\rho \}}$

Примечания

1. Палочка, Митчелл (июнь 1989 г.). «Вывод типа для объединения записей и множественного наследования». Ход работы. Четвертый ежегодный симпозиум по логике в компьютерных науках. С. 92–97. Дои:10.1109 / LICS.1989.39162.
2. Палочка, Митчелл (1991). «Вывод типа для объединения записей и множественного наследования». Информация и вычисления. 93 (Выборка из симпозиума IEEE 1989 г. по логике в компьютерных науках): 1–15. Дои:10.1016 / 0890-5401 (91) 90050-С. ISSN  0890-5401.