¿Cuál es la diferencia entre polimorfismo de filas y tipificación estructural?

Question

Las definiciones con las que me he topado parecen indicar que expresan la misma idea.Es decir, la relación entre tipos de registros está determinada por sus campos (o propiedades) en lugar de sus nombres.Sus páginas de Wikipedia también parecen indicar la misma idea:

A sistema de tipo estructural (o sistema de tipos basado en propiedades) es una clase importante de sistema de tipos en el que la compatibilidad y equivalencia de tipos están determinadas por la estructura o definición real del tipo y no por otras características como su nombre o lugar de declaración.

En la teoría de tipos de lenguajes de programación, polimorfismo de fila es un tipo de polimorfismo que permite escribir programas que son polimórficos en tipos de campos de registro (también conocidos como filas, de ahí polimorfismo de filas).

¿Hay alguna diferencia entre ellos?

Answer 1

Los sistemas de tipo estructural no necesariamente tienen nada que ver con los registros.Por ejemplo, podría tener un sistema donde:

data Bool = False | True
data Two = Zero | One

son en realidad del mismo tipo, porque ambos son tipos con dos constructores nulos.Tampoco necesariamente dice mucho sobre los registros, porque aunque los tipos están determinados por su estructura, los dos registros:

{s : S ; t : T}
{s : S ; t : T ; u : U}

no son la misma estructura, por lo que podría tener tipificación estructural sin que haya nada conveniente en estos dos tipos.

De manera similar, el polimorfismo de filas de forma aislada no dice mucho, solo que puede cuantificar filas y probablemente usarlas, por ejemplo.un tipo de registro parametrizado por una fila.Pero hay todo tipo de variaciones sobre lo que se puede hacer con las filas que realmente especifican las capacidades del sistema.

Por lo general, con los registros estructurales la gente al menos quiere subtipificar.Eso le permite decir que mi segundo tipo de registro anterior es un subtipo del primero, de modo que puede pasar el último a cualquier cosa que espere el primero.Una forma típica de hacer esto con el polimorfismo de filas es cuantificar los campos adicionales que puedan estar presentes y utilizar algún tipo de concatenación de filas.

Entonces, quizás una pregunta más específica sea cuál es la diferencia entre subtipificación y cuantificadores.La respuesta a esto es generalmente que la subtipificación no puede expresar tipos cuantificados a menos que la variable cuantificada solo ocurra exclusivamente de manera covariante o contravariante.Entonces podríamos decir:

(forall a. a -> T) ~= Top -> T
(forall a. T -> a) ~= T -> Bot

Pero para un tipo como forall a. a -> a, no hay un tipo para elegir a sin perder información.

Esto se extiende a sistemas con justo subtipificación de registros vs.Polimorfismo de fila (apropiado).Sin embargo, si tiene un sistema con subtipos y cuantificadores, y los subtipos pueden aplicarse a tipos cuantificados, entonces las diferencias podrían ser mucho más sutiles.Sin embargo, tener cuantificadores y subtipos puede resultar bastante complicado (tampoco es que el polimorfismo de filas sea fácil de acertar).