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

This article provides insufficient context for those unfamiliar with the subject. Please help improve the article by providing more context for the reader. (October 2018) (Learn how and when to remove this message)

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

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

Может быть записано как . Это указывает на тип записи, который имеет поля с соответствующими типами (для ), и не имеет ни одного из полей (для ), при этом выражает тот факт, что запись может содержать другие поля, кроме . ${\displaystyle \{\ell _{1}:T_{1},\dots ,\ell _{n}:T_{n},{\text{absent}}(f_{1}),\dots ,{\text{absent}}(f_{m}),\rho \}}$${\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{Number}},y:{\text{Number}},\rho \}\to \{x:{\text{Number}},y:{\text{Number}},\rho \}}$

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