Qual é a diferença entre polimorfismo de linha e digitação estrutural?

Question

As definições que encontrei parecem indicar que expressam a mesma ideia.Isso significa que o relacionamento entre os tipos de registro é determinado pelos seus campos (ou propriedades) e não pelos seus nomes.Suas páginas da Wikipedia também parecem indicar a mesma ideia:

A sistema de tipo estrutural (ou sistema de tipos baseado em propriedades) é uma classe principal de sistema de tipos em que a compatibilidade e a equivalência de tipos são determinadas pela estrutura ou definição real do tipo e não por outras características, como seu nome ou local de declaração.

Na teoria dos tipos de linguagem de programação, polimorfismo de linha é um tipo de polimorfismo que permite escrever programas que são polimórficos em tipos de campo de registro (também conhecidos como linhas, daí polimorfismo de linha).

Existem diferenças entre eles?

Answer 1

Os sistemas de tipo estrutural não têm necessariamente nada a ver com registros.Por exemplo, você poderia ter um sistema onde:

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

são na verdade do mesmo tipo, porque ambos são tipos com dois construtores nulos.Também não diz necessariamente muito sobre os registros, porque embora os tipos sejam determinados por sua estrutura, os dois registros:

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

não são a mesma estrutura, então você poderia ter tipagem estrutural sem que houvesse nada de conveniente nesses dois tipos.

Da mesma forma, o polimorfismo de linha isoladamente não diz muito - apenas que você pode quantificar as linhas e provavelmente usá-las, por exemplo.um tipo de registro parametrizado por uma linha.Mas existem todos os tipos de variações sobre o que você pode fazer com linhas que realmente especificam os recursos do sistema.

Geralmente, com registros estruturais, as pessoas desejam pelo menos subtipagem.Isso permite dizer que meu segundo tipo de registro acima é um subtipo do primeiro, para que você possa passar o último para qualquer coisa que espere o primeiro.Uma maneira típica de fazer isso com o polimorfismo de linha é quantificar os campos extras que podem estar presentes e usar algum tipo de concatenação de linha.

Então, talvez uma questão mais direcionada seja qual é a diferença entre subtipagem e quantificadores.A resposta para isso é geralmente que a subtipagem não pode expressar tipos quantificados, a menos que a variável quantificada ocorra apenas de forma exclusivamente covariante ou contravariante.Então poderíamos dizer:

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

Mas para um tipo como forall a. a -> a, não há um tipo para escolher a sem perder informações.

Isto se estende a sistemas com apenas subtipagem de registros vs.polimorfismo de linha (apropriado).No entanto, se você tiver um sistema com subtipagem e quantificadores, e a subtipagem puder ser aplicada a tipos quantificados, as diferenças poderão ser muito mais sutis.Porém, ter quantificadores e subtipos pode ser bastante complicado (não que o polimorfismo de linha seja fácil de acertar).