Subtipagem - Subtyping

Na teoria da linguagem de programação , subtipo (também polimorfismo de subtipo ou polimorfismo de inclusão ) é uma forma de polimorfismo de tipo em que um subtipo é um tipo de dados que está relacionado a outro tipo de dados (o supertipo ) por alguma noção de substituibilidade , o que significa que os elementos do programa, normalmente sub-rotinas ou funções, escritas para operar em elementos do supertipo, também podem operar em elementos do subtipo. Se S é um subtipo de T, a relação de subtipagem é freqüentemente escrita S <: T, para significar que qualquer termo do tipo S pode ser usado com segurança em um contexto onde um termo do tipo T é esperado. A semântica precisa de subtipagem depende crucialmente dos detalhes do que "usado com segurança em um contexto onde" significa em uma determinada linguagem de programação . O sistema de tipos de uma linguagem de programação define essencialmente sua própria relação de subtipagem, que pode muito bem ser trivial , caso a linguagem não suporte (ou suporte muito poucos) mecanismos de conversão.

Devido à relação de subtipagem, um termo pode pertencer a mais de um tipo. A subtipagem é, portanto, uma forma de polimorfismo de tipo. Na programação orientada a objetos, o termo 'polimorfismo' é comumente usado para se referir apenas a este polimorfismo de subtipo , enquanto as técnicas de polimorfismo paramétrico seriam consideradas programação genérica .

Linguagens de programação funcional geralmente permitem a subtipagem de registros . Conseqüentemente, o cálculo lambda simplesmente digitado estendido com tipos de registro é talvez o cenário teórico mais simples no qual uma noção útil de subtipagem pode ser definida e estudada. Como o cálculo resultante permite que os termos tenham mais de um tipo, ele não é mais uma teoria de tipo "simples" . Como as linguagens de programação funcional, por definição, oferecem suporte a literais de função , que também podem ser armazenados em registros, os tipos de registros com subtipagem fornecem alguns dos recursos da programação orientada a objetos. Normalmente, as linguagens de programação funcional também fornecem alguma forma, geralmente restrita, de polimorfismo paramétrico. Em um cenário teórico, é desejável estudar a interação dos dois recursos; um cenário teórico comum é sistema de F _<: . Vários cálculos que tentam capturar as propriedades teóricas da programação orientada para o objecto pode ser derivados a partir do sistema de F _<: .

O conceito de subtipagem está relacionado às noções linguísticas de hiponímia e holonímia . Também está relacionado ao conceito de quantificação limitada em lógica matemática (consulte Lógica ordenada por ordem ). A subtipagem não deve ser confundida com a noção de herança (classe ou objeto) de linguagens orientadas a objetos; subtipagem é uma relação entre tipos (interfaces na linguagem orientada a objetos), enquanto herança é uma relação entre implementações originadas de um recurso de linguagem que permite que novos objetos sejam criados a partir dos existentes. Em várias linguagens orientadas a objetos, a subtipagem é chamada de herança de interface , com herança referida como herança de implementação .

Origens

A noção de subtipagem em linguagens de programação remonta à década de 1960; foi introduzido em derivados Simula . Os primeiros tratamentos formais de subtipagem foram dados por John C. Reynolds em 1980, que usou a teoria das categorias para formalizar conversões implícitas , e Luca Cardelli (1985).

O conceito de subtipagem ganhou visibilidade (e sinonímia com polimorfismo em alguns círculos) com a adoção predominante da programação orientada a objetos. Neste contexto, o princípio da substituição segura é frequentemente chamado de princípio da substituição de Liskov , em homenagem a Barbara Liskov que o popularizou em um discurso em uma conferência sobre programação orientada a objetos em 1987. Como deve considerar objetos mutáveis, a noção ideal de subtipagem definido por Liskov e Jeannette Wing , chamado de subtipagem comportamental é consideravelmente mais forte do que o que pode ser implementado em um verificador de tipo . (Consulte § Tipos de função abaixo para obter detalhes.)

Exemplos

Exemplo de subtipos: onde bird é o supertipo e todos os outros são subtipos, conforme indicado pela seta na notação UML

Um exemplo prático simples de subtipos é mostrado no diagrama, à direita. O tipo "pássaro" possui três subtipos "pato", "cuco" e "avestruz". Conceitualmente, cada um deles é uma variedade do tipo básico "pássaro" que herda muitas características de "pássaro", mas possui algumas diferenças específicas. A notação UML é usada neste diagrama, com setas abertas mostrando a direção e o tipo de relacionamento entre o supertipo e seus subtipos.

Como um exemplo mais prático, uma linguagem pode permitir que valores inteiros sejam usados ​​sempre que valores de ponto flutuante são esperados ( Integer< Float:), ou pode definir um tipo genéricoNúmerocomo um supertipo comum de inteiros e reais. Neste segundo caso, temos apenas Integer<: Numbere Float<:, Numbermas Integere Floatnão são subtipos um do outro.

Os programadores podem tirar vantagem da subtipagem para escrever código de uma maneira mais abstrata do que seria possível sem ela. Considere o seguinte exemplo:

function max (x as Number, y as Number) is
    if x < y then
        return y
    else
        return x
end

Se inteiro e real forem ambos subtipos de Number, e um operador de comparação com um número arbitrário for definido para ambos os tipos, então os valores de qualquer tipo podem ser passados ​​para esta função. No entanto, a própria possibilidade de implementar tal operador restringe fortemente o tipo de número (por exemplo, não se pode comparar um inteiro com um número complexo) e, na verdade, apenas comparar inteiros com inteiros e reais com reais faz sentido. Reescrever essa função para que ela aceite apenas 'x' e 'y' do mesmo tipo requer polimorfismo limitado .

Subsumption

Em teoria tipo o conceito de subordinação é utilizado para definir ou avaliar se um tipo S é um subtipo do tipo T .

Um tipo é um conjunto de valores. O conjunto pode ser descrito extensionalmente , listando todos os valores, ou pode ser descrito intensivamente , declarando a associação do conjunto por um predicado sobre um domínio de valores possíveis. Em linguagens de programação comuns, os tipos de enumeração são definidos extensivamente por valores de listagem. Tipos definidos pelo usuário como registros (structs, interfaces) ou classes são definidos intensivamente por uma declaração de tipo explícita ou usando um valor existente, que codifica informações de tipo, como um protótipo a ser copiado ou estendido.

Ao discutir o conceito de subordinação, o conjunto de valores de um tipo é indicado por escrever seu nome em itálico matemáticas: T . O tipo, visto como um predicado sobre um domínio, é indicado por escrever seu nome em negrito: T . O símbolo convencional <: significa "é um subtipo de" e :> significa "é um supertipo de".

• Um tipo T engloba S se o conjunto de valores de T que se define, é um subconjunto do conjunto de S , de modo a que cada membro de S é também um membro do T .
• Um tipo pode ser incluído mais do que um tipo: os supertipos de S se cruzam em S .
• Se S <: T (e, por conseguinte, S ⊆ T ), então T , o predicado que circunscreve o conjunto T , deve fazer parte do predicado S (em relação ao mesmo domínio) que define S .
• Se S inclui T e T inclui S , então os dois tipos são iguais (embora possam não ser do mesmo tipo se o sistema de tipos distinguir os tipos pelo nome).

Uma regra prática a seguir: um subtipo é provavelmente "maior / mais amplo / mais profundo" (seus valores contêm mais informações) e "menos / menor" (o conjunto de valores é menor) do que um de seus supertipos (que tem mais restrições informações e cujo conjunto de valores é um superconjunto daqueles do subtipo).

No contexto de subsunção, as definições de tipo podem ser expressas usando a notação Set-builder , que usa um predicado para definir um conjunto. Predicados pode ser definida ao longo de um domínio (conjunto de valores possíveis) D . Predicados são funções parciais que comparam valores aos critérios de seleção. Por exemplo: "é um valor inteiro maior ou igual a 100 e menor que 200?". Se um valor corresponder aos critérios, a função retornará o valor. Caso contrário, o valor não é selecionado e nada é retornado. (Compreensões de lista são uma forma desse padrão usado em muitas linguagens de programação.)

Se houver dois predicados, que aplicam critérios de seleção para o tipo T , e que aplicam critérios adicionais para o tipo S , então os conjuntos para os dois tipos podem ser definidos: ${\ displaystyle P_ {T}}$${\ displaystyle P_ {s}}$

${\ displaystyle T = \ {v \ in D \ mid \ P_ {T} (v) \}}$

${\ displaystyle S = \ {v \ in D \ mid \ P_ {T} (v) {\ text {e}} P_ {s} (v) \}}$

O predicado é aplicado ao lado de , como parte do predicado composto S definindo S . Os dois predicados são conjugados , portanto, ambos devem ser verdadeiros para que um valor seja selecionado. O predicado subsume o predicado T , de modo S <: T .${\ displaystyle \ mathbf {T} = P_ {T}}$${\ displaystyle P_ {s}}$${\ displaystyle \ mathbf {S} = \ mathbf {T} \ land P_ {s} = P_ {T} \ land P_ {s}}$

Por exemplo: existe uma subfamília de espécies de gatos chamada Felinae , que faz parte da família Felidae . O gênero Felis , ao qual pertence a espécie de gato doméstico Felis catus , faz parte dessa subfamília.

${\ displaystyle {\ mathit {Felinae = \ {cat \ in Felidae \ mid \ ofSubfamily (cat, felinaeSubfamilyName) \}}}}$

${\ displaystyle {\ mathit {Felis = \ {cat \ in Felinae \ mid \ ofGenus (cat, felisGenusName) \}}}}$

A conjunção de predicados foi expressa aqui por meio da aplicação do segundo predicado sobre o domínio de valores em conformidade com o primeiro predicado. Vistos como tipos, Felis <: Felinae <: Felidae .

Se T inclui S ( T:> S ), então um procedimento, função ou expressão dado um valor como um operando (argumento ou termo de entrada) será, portanto, capaz de operar sobre esse valor como um do tipo T , porque . No exemplo acima, poderíamos esperar que a função de Subfamília fosse aplicável a valores de todos os três tipos Felidae , Felinae e Felis . ${\ displaystyle s \ in S}$${\ displaystyle s \ in T}$

Esquemas de subtipagem

Os teóricos de tipo fazem uma distinção entre o subtipo nominal , no qual apenas os tipos declarados de uma certa maneira podem ser subtipos um do outro, e o subtipo estrutural , no qual a estrutura de dois tipos determina se um é ou não um subtipo do outro. O subtipo orientado a objeto baseado em classe descrito acima é nominal; uma regra de subtipagem estrutural para uma linguagem orientada a objetos pode dizer que se os objetos do tipo A podem manipular todas as mensagens que os objetos do tipo B podem manipular (isto é, se eles definem todos os mesmos métodos ), então A é um subtipo de B independentemente de um deles herdar do outro. Essa chamada digitação duck é comum em linguagens orientadas a objetos digitadas dinamicamente. Regras sólidas de subtipagem estrutural para tipos diferentes de tipos de objeto também são bem conhecidas.

Implementações de linguagens de programação com subtipagem se enquadram em duas classes gerais: implementações inclusivas , nas quais a representação de qualquer valor do tipo A também representa o mesmo valor no tipo B se A  <:  B , e implementações coercitivas , nas quais um valor do tipo A podem ser convertidos automaticamente em uma de tipo B . A subtipagem induzida pela subclasse em uma linguagem orientada a objetos é geralmente inclusiva; relações de subtipagem que relacionam números inteiros e números de ponto flutuante, que são representados de forma diferente, geralmente são coercivas.

Em quase todos os sistemas de tipo que definem uma relação de subtipagem, ela é reflexiva (significando A  <:  A para qualquer tipo A ) e transitiva (significando que se A  <:  B e B  <:  C então A  <:  C ). Isso o torna uma encomenda de tipos.

Tipos de registro

Subtipagem de largura e profundidade

Tipos de registros dão origem aos conceitos de subtipagem de largura e profundidade . Expressam duas formas distintas de obtenção de um novo tipo de registro que permite as mesmas operações do tipo de registro original.

Lembre-se de que um registro é uma coleção de campos (nomeados). Visto que um subtipo é um tipo que permite todas as operações permitidas no tipo original, um subtipo de registro deve suportar as mesmas operações nos campos que o tipo original suportado.

Uma forma de obter esse suporte, chamada de subtipagem de largura , adiciona mais campos ao registro. Mais formalmente, cada campo (nomeado) que aparece no supertipo de largura aparecerá no subtipo de largura. Assim, qualquer operação viável no supertipo será suportada pelo subtipo.

O segundo método, chamado de subtipagem de profundidade , substitui os vários campos por seus subtipos. Ou seja, os campos do subtipo são subtipos dos campos do supertipo. Uma vez que qualquer operação suportada para um campo no supertipo é suportada para seu subtipo, qualquer operação viável no supertipo de registro é suportada pelo subtipo de registro. Subtipagem de profundidade só faz sentido para registros imutáveis: por exemplo, você pode atribuir 1,5 ao campo 'x' de um ponto real (um registro com dois campos reais), mas você não pode fazer o mesmo com o campo 'x' de um ponto inteiro (que, no entanto, é um subtipo profundo do tipo de ponto real) porque 1,5 não é um inteiro (consulte Variância ).

A subtipagem de registros pode ser definida no Sistema F _< :, que combina o polimorfismo paramétrico com a subtipagem de tipos de registro e é uma base teórica para muitas linguagens de programação funcionais que oferecem suporte a ambos os recursos.

Alguns sistemas também suportam subtipagem de tipos de união disjunta rotulados (como tipos de dados algébricos ). A regra para subtipo de largura é invertida: cada tag que aparece no subtipo de largura deve aparecer no supertipo de largura.

Tipos de função

Se T ₁ → T ₂ é um tipo de função, então um subtipo dele é qualquer tipo de função S ₁ → S ₂ com a propriedade de que T ₁ <: S ₁ e S ₂ <: T ₂ . Isso pode ser resumido usando a seguinte regra de digitação :

${\ displaystyle T_ {1} \ leq: S_ {1} \ quad S_ {2} \ leq: T_ {2} \ over S_ {1} \ rightarrow S_ {2} \ leq: T_ {1} \ rightarrow T_ { 2}}$

O tipo de argumento de S ₁ → S ₂ é considerado contravariante porque a relação de subtipagem é invertida para ele, enquanto o tipo de retorno é covariante . Informalmente, essa reversão ocorre porque o tipo refinado é "mais liberal" nos tipos que aceita e "mais conservador" no tipo que retorna. Isso é exatamente o que funciona em Scala : uma função n -ary é internamente uma classe que herda o traço (que pode ser visto como uma interface geral em linguagens semelhantes a Java ), onde estão os tipos de parâmetro e B é seu tipo de retorno; " - " antes do tipo significa que o tipo é contravariante, enquanto " + " significa covariante. ${\ displaystyle {\ mathtt {Function_ {N} (- A_ {1}, - A_ {2}, \ dots, -A_ {n}, + B)}}}$ ${\ displaystyle {\ mathtt {A_ {1}, A_ {2}, \ dots A_ {n}}}}$

Em linguagens que permitem efeitos colaterais, como a maioria das linguagens orientadas a objetos, a subtipagem geralmente não é suficiente para garantir que uma função possa ser usada com segurança no contexto de outra. O trabalho de Liskov nesta área se concentrou na subtipagem comportamental , que além da segurança do sistema de tipos discutida neste artigo, também requer que os subtipos preservem todos os invariantes garantidos pelos supertipos em algum contrato . Esta definição de subtipagem é geralmente indecidível , portanto, não pode ser verificada por um verificador de tipo .

A subtipagem de referências mutáveis é semelhante ao tratamento de argumentos de função e valores de retorno. Referências somente de gravação (ou coletores ) são contravariantes, como argumentos de função; referências somente leitura (ou fontes ) são covariantes, como valores de retorno. As referências mutáveis ​​que atuam como fontes e sumidouros são invariantes.

Relação com herança

Subtipagem e herança são relacionamentos independentes (ortogonais). Eles podem coincidir, mas nenhum é um caso especial do outro. Em outras palavras, entre os dois tipos S e T , todas as combinações de subtipagem e herança são possíveis:

1. S não é um subtipo nem um tipo derivado de T
2. S é um subtipo, mas não é um tipo derivado de T
3. S não é um subtipo, mas é um tipo derivado de T
4. S é um subtipo e um tipo derivado de T

O primeiro caso é ilustrado por tipos independentes, como Booleane Float.

O segundo caso pode ser ilustrado pela relação entre Int32e Int64. Na maioria das linguagens de programação orientadas a objetos, Int64não são relacionados por herança a Int32. No entanto, Int32pode ser considerado um subtipo de, Int64uma vez que qualquer valor inteiro de 32 bits pode ser promovido para um valor inteiro de 64 bits.

O terceiro caso é uma consequência da função de subtipagem da contravariância de entrada . Suponha que uma superclasse do tipo T tenha um método m retornando um objeto do mesmo tipo ( ou seja, o tipo de m é T → T , observe também que o primeiro argumento de m é este / self) e uma classe derivada do tipo S de T . Por herança, o tipo de m em S é S → S . A fim de S ser um subtipo de T do tipo de m em S deverá ser um subtipo do tipo de m em T , em outras palavras: S → S ≤: T → T . Pela aplicação ascendente da regra de subtipagem da função, isso significa: S ≤: T e T ≤: S , o que só é possível se S e T forem iguais. Como a herança é uma relação irreflexiva, S não pode ser um subtipo de T .

O subtipo e a herança são compatíveis quando todos os campos e métodos herdados do tipo derivado têm tipos que são subtipos dos campos e métodos correspondentes do tipo herdado.

Coerções

Em sistemas de subtipos coercitivos, os subtipos são definidos por funções implícitas de conversão de tipo de subtipo em supertipo. Para cada relação de subtipagem ( S <: T ), uma função de coerção coerce : S → T é fornecido, e qualquer objeto s do tipo S é considerado como o objecto coerce _{S → t} ( s ) de tipo T . Uma função de coerção pode ser definida por composição: se S <: T e T <: U então s pode ser considerado como um objeto do tipo u sob a coerção composta ( coerção _{T → U} ∘ coerção _{S → T} ). A coerção de tipo de um tipo para si mesmo coagir _{T → T} é a função de identidade id _T

Funções de coerção para registros e subtipos de união disjunta podem ser definidas componente a componente; no caso de registros estendidos por largura, a coerção de tipo simplesmente descarta quaisquer componentes que não estejam definidos no supertipo. A coacção tipo para tipos de função pode ser dada por f' ( s ) = coerce _{S 2 → T 2} ( f ( coerce _{T 1 → S 1} ( t ))), reflectindo a contravariância dos argumentos da função de covariância e de valores de retorno.

A função de coerção é determinada de forma única, dado o subtipo e supertipo . Portanto, quando vários relacionamentos de subtipagem são definidos, deve-se ter cuidado para garantir que todas as coerções de tipo sejam coerentes. Por exemplo, se um inteiro como 2: int pode ser forçado a um número de ponto flutuante (digamos, 2.0: float ), então não é admissível coagir 2.1: float a 2: int , porque a coerção composta coagir _{float → float} dada pelo coerce _{int → flutuador} ∘ coerce _{flutuador → int} seria então distinta da identidade coerção id _flutuador .

Veja também

• Covariância e contravariância
• O problema do círculo-elipse (para os perigos de subtipar tipos de variáveis ​​na mesma base que tipos de valor)
• Programação baseada em aulas
• Tipo de topo
• Tipo de refinamento
• Subtipagem comportamental

Notas

Referências

Livros didáticos

Papéis

Leitura adicional