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

Эта статья не предоставляет достаточного контекста для тех, кто не знаком с предметом . Пожалуйста, помогите улучшить статью , предоставив читателю больше контекста . ( Октябрь 2018 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения )

Эта статья требует внимания специалиста по математике . Конкретная проблема заключается в следующем: Обозначения неясны, без объяснения того, как n в первой формуле соотносится с n и m во второй формуле, или как они могут быть равны 0, или каковы все эти дополнительные поля. WikiProject Mathematics может чтобы помочь нанять специалиста. ( Октябрь 2018 г. )

В теории типов языков программирования полиморфизм строк - это своего рода полиморфизм, который позволяет писать программы, полиморфные по типам полей записи (также известные как строки, отсюда и полиморфизм строк). Строка-полиморфная система типов и доказательство вывода типов были введены Митчеллом Вандом . ^{[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}}$

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

Заметки [ править ]