Полиморфизм строк

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

Определение типа записи с полиморфной строкой

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

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

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

    ${\text{transform2d}}:\{x:{\text{Number}},y:{\text{Number}},\rho \}\to \{x:{\text{Number}},y:{\text{Number}},\rho \}$

Благодаря полиморфизму строк функция может выполнять двумерное преобразование трехмерной (фактически n -мерной) точки, оставляя координату z (или любые другие координаты) нетронутой. В более общем смысле функция может выполняться с любой записью, содержащей поля $x$ и $y$ с типом ${\text{Number}}$ . Потери информации нет: тип гарантирует, что все поля, представленные переменной $\rho$ присутствуют в возвращаемом типе. Напротив, определение типа $\{x:{\text{Number}},y:{\text{Number}},\mathbf {empty} \}$ выражает тот факт, что запись этого типа имеет именно $x$ и $y$ поля и ничего более. В этом случае получается классический тип записи.

Ввод операций над записями

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

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

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

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

Примечания

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

[1] «OCaml — Полиморфные варианты» . v2.ocaml.org . Проверено 3 декабря 2022 г.

[2] Ванд, Митчелл (июнь 1989 г.). «Вывод типа для конкатенации записей и множественного наследования». Слушания. Четвертый ежегодный симпозиум по логике в информатике . стр. 92–97. дои : 10.1109/LICS.1989.39162 .

[3] Ванд, Митчелл (1991). «Вывод типа для конкатенации записей и множественного наследования». Информация и вычисления . 93 (Избранное с симпозиума IEEE по логике в информатике 1989 г.): 1–15. дои : 10.1016/0890-5401(91)90050-C . ISSN 0890-5401 .

[1]

[2]

[3]