Polimorfismo de filas

En la teoría de tipos de lenguajes de programación , el polimorfismo de filas es un tipo de polimorfismo que permite escribir programas que son estructuralmente ^{[ 1 ]} (en lugar de nominalmente) polimórficos en tipos de registros y/o variantes . ^{[ 2 ]}

Mitchell Wand introdujo un sistema de tipos polimórfico por filas y una prueba de inferencia de tipos para registros . ^{[ 3 ] [ 4 ]}

El tratamiento teórico del polimorfismo de filas se complica un tanto por la necesidad de tener etiquetas distintas en un registro. Un enfoque, adoptado por Rémy y sus colegas (e implícitamente presente en la presentación que sigue, la cual está fuertemente inspirada en la de Wand), consiste en considerar diferentes tipos de filas, dependiendo de sus etiquetas. ^{[ 2 ]}

Gaster y Jones extendieron formalmente el enfoque también a las variantes, haciendo que tanto el constructor de tipo de registro como el de tipo de variante mapeen de tipos de fila a tipos. ^{[ 5 ]}

Blume et al. propusieron llevar el enfoque un paso más allá en el ámbito de las extensiones componibles agregando "casos de primera clase" manejados por una LetCCconstrucción para componer continuaciones en el código de coincidencia de casos. ^{[ 6 ]} Luego, un par de proyectos (Links , Koka) han utilizado el polimorfismo de filas como base de tipos de un sistema de efectos algebraicos , apuntando a la "composición libre" de efectos definidos por el usuario. ^{[ 7 ] [ 8 ]}

Otro enfoque para el problema de las etiquetas únicas es extender el sistema F con un operador de "fusión coherente", lo que da como resultado cálculos con los llamados tipos de intersección disjuntos . ^{[ 9 ]}

Morris y McKinna generalizaron los tipos de filas a teorías de filas para manejar uniformemente nociones variables de extensión (de registros) en un único marco teórico: por ejemplo, una aplicación puede desear que la operación de extensión sobrescriba los campos existentes en caso de nombres coincidentes, otra puede querer mantener ambos accesibles, posiblemente algún esquema de direccionamiento basado en rutas, etc. ^{[ 10 ]}

El tipo de registro polimórfico por filas define una lista de campos con sus tipos correspondientes, una lista de campos faltantes y una variable que indica la ausencia o presencia de campos adicionales arbitrarios. Ambas listas son opcionales y la variable puede estar restringida. Específicamente, la variable puede estar "vacía", lo que indica que no puede haber campos adicionales para el registro.

Puede escribirse como${\displaystyle \{\ell _{1}:T_{1},\dots ,\ell _{n}:T_{n},{\text{ausente}}(f_{1}),\dots ,{\text{ausente}}(f_{m}),\rho \}}$. Esto indica un tipo de registro que tiene campos${\displaystyle \ell _{i}}$con sus respectivos tipos de${\displaystyle T_{i}}$(para${\displaystyle i=1\dots n}$), y no tiene ninguno de los campos${\displaystyle f_{j}}$(para${\displaystyle j=1\dots m}$), mientras${\displaystyle \rho }$expresa el hecho de que el registro puede contener otros campos que${\displaystyle \ell _{i}}$.

Los tipos de registro polimórficos por filas nos permiten escribir programas que operan solo en una sección de un registro. Por ejemplo, se puede definir una función que realice una transformación bidimensional que acepte un registro con dos o más coordenadas y devuelva un tipo idéntico:

$${\displaystyle {\text{transform2d}}:\{x:{\text{Número}},y:{\text{Número}},\rho \}\to \{x:{\text{Número}},y:{\text{Número}},\rho \}}$$

Gracias al polimorfismo de filas, la función puede realizar una transformación bidimensional en un punto tridimensional (de hecho, n- dimensional), dejando intacta la coordenada z (o cualquier otra coordenada). En un sentido más general, la función puede realizarse en cualquier registro que contenga los campos x e y con tipo${\displaystyle {\text{Número}}}$No hay pérdida de información: el tipo garantiza que todos los campos representados por la variable${\displaystyle \rho }$están presentes en el tipo de retorno. En contraste, la definición de tipo${\displaystyle \{x:{\text{Número}},y:{\text{Número}},\mathbf {vacío} \}}$expresa que un registro de ese tipo tiene exactamente los campos x e y y nada más. En este caso, se obtiene un tipo de registro clásico.

Las operaciones de registro de selección de un campo${\displaystyle r.\ell }$, agregando un campo${\displaystyle r[\ell$ :=e]} , y eliminando un campo${\displaystyle r\backslash \ell }$Se les pueden asignar tipos polimórficos por filas.

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

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

$${\displaystyle \mathrm {eliminar_{\ell }} =\lambda rr\backslash \ell \;:\;\{\ell :T,\rho \}\rightarrow \{\mathrm {ausente} (\ell ),\rho \}}$$

El polimorfismo de filas no es compatible con Standard ML , pero sí lo es con algunas extensiones o derivados como SML# ^{[ 11 ]} y Ocaml .

La existencia misma de la primera versión de SML# fue motivada ^{[ 12 ]} por la adición de polimorfismo de filas, basado en un artículo de SIGMOD '89 de Ohori et al., ^{[ 13 ]} que introdujo la extensión "Machiavelli" a SML, aunque su nombre fue cambiado posteriormente a "SML# de Kansai", antes de adoptar el nombre más corto. El '#' en el nombre no tiene relación con F# , sino que se debe al #operador utilizado para definir implícitamente los tipos polimórficos de filas en el acceso a campos.

En OCaml, el polimorfismo de filas es utilizado por objectlos tipos de OCaml y también por sus variantes polimórficas. Los tipos de registro ordinarios no son polimórficos de filas en OCaml. ^{[ 14 ]} Castagna et al. han criticado a OCaml por carecer de tipado sensible al flujo , lo cual es particularmente notorio en la inferencia de tipos para variantes polimórficas. También señalan que, dado que OCaml carece de tipos de unión verdaderos y sin etiquetar , algunos de los tipos inferidos para variantes polimórficas son demasiado restrictivos, en particular cuando se utilizan tipos de producto en combinación con variantes polimórficas. ^{[ 15 ]}

F# puede simular el polimorfismo de filas utilizando su mecanismo de "Parámetros de tipo resueltos estáticamente" (SRTP), ^{[ 16 ]} que también se ha denominado informalmente " tipado pato estático ". ^{[ 17 ]} Sin embargo, esto se limita a las funciones F# en línea, por lo que no se exportan al sistema de tipos .NET , que a su vez no admite dicha característica.

PureScript también admite el polimorfismo de filas . ^{[ 18 ]}