Subtipagem

Da Wikipédia, a enciclopédia livre
Ir para a navegação Saltar para pesquisar

Na teoria da linguagem de programação , a subtipagem (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, tipicamente 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 é frequentemente escrita S <: T, para significar que qualquer termo do tipo S pode serusado com segurança em um contexto onde um termo do tipo T é esperado. A semântica precisa da subtipagem depende crucialmente das particularidades 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 ser trivial , caso a linguagem suporte nenhum (ou muito pouco) mecanismo 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 subtipo polimorfismo , enquanto as técnicas de polimorfismo paramétrico seriam consideradas programação genérica .

As linguagens de programação funcionais geralmente permitem a subtipagem de registros . Consequentemente, o cálculo lambda simplesmente tipado 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. [1] Como o cálculo resultante permite que os termos tenham mais de um tipo, não é mais uma teoria de tipos "simples" . Como as linguagens de programação funcionais, por definição, suportam 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 funcionais também fornecem alguma forma, geralmente restrita, de polimorfismo paramétrico. Em um cenário teórico, é desejável estudar a interação das duas características; uma configuração teórica comum é o sistema F <: . Vários cálculos que tentam capturar as propriedades teóricas da programação orientada a objetos podem ser derivados do sistema 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; [2] a subtipagem é uma relação entre tipos (interfaces na linguagem orientada a objetos), enquanto a herança é uma relação entre implementações decorrentes de um recurso de linguagem que permite que novos objetos sejam criados a partir de objetos existentes. Em várias linguagens orientadas a objetos, a subtipagem é chamada de herança de interface , com herança referida comoherança de implementação .

Origens

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

O conceito de subtipagem ganhou visibilidade (e sinônimo de polimorfismo em alguns círculos) com a adoção generalizada da programação orientada a objetos. Neste contexto, o princípio da substituição segura é muitas vezes chamado de princípio da substituição de Liskov , em homenagem a Barbara Liskov que o popularizou em uma palestra em uma conferência sobre programação orientada a objetos em 1987. Porque 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 tipos . (Consulte § Tipos de função abaixo para obter detalhes.)

Exemplos

Exemplo de subtipos: onde pássaro é o supertipo e todos os outros são subtipos conforme indicado pela seta em 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 tem algumas diferenças específicas. A notação UML é usada neste diagrama, com setas abertas mostrando a direção e o tipo do relacionamento entre o supertipo e seus subtipos.

Como um exemplo mais prático, uma linguagem pode permitir que valores inteiros sejam usados ​​onde quer que valores de ponto flutuante sejam 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<: Number, mas Integere Floatnão são subtipos um do outro.

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

função  max  ( x  como  número ,  y  como  número )  é 
    se  x  <  y  então 
        retorna  y 
    senão 
        retorna  x 
fim

Se integer e real forem ambos subtipos de Number, e um operador de comparação com um Number arbitrário for definido para ambos os tipos, valores de qualquer tipo poderão ser passados ​​para esta função. No entanto, a própria possibilidade de implementar tal operador restringe muito o tipo Number (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 esta função para que ela aceite apenas 'x' e 'y' do mesmo tipo requer polimorfismo limitado .

Subsunção

Na teoria dos tipos o conceito de subsunção [4] é usado 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 intencionalmente declarando a pertinência 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 extensionalmente por valores de listagem. Tipos definidos pelo usuário como registros (structs, interfaces) ou classes são definidos intencionalmente 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 subsunção, o conjunto de valores de um tipo é indicado escrevendo seu nome em itálico matemático: T . O tipo, visto como um predicado sobre um domínio, é indicado escrevendo seu nome em negrito: T . O símbolo convencional <: significa "é um subtipo de", e :> significa "é um supertipo de".

  • Um tipo T subsume S se o conjunto de valores T que ele define for um superconjunto do conjunto S , de modo que todo membro de S também é membro de T .
  • Um tipo pode ser subsumido por mais de um tipo: os supertipos de S se cruzam em S .
  • Se S <: T (e portanto S ⊆ T ), então T , o predicado que circunscreve o conjunto T , deve fazer parte do predicado S (sobre o mesmo domínio) que define S .
  • Se S subsume T e T subsume 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).

Segue-se uma regra prática: é provável que um subtipo seja "maior/mais largo/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 informação, 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. Os predicados podem ser definidos sobre um domínio (conjunto de valores possíveis) D . Predicados são funções parciais que comparam valores com 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 será selecionado e nada será retornado. (As compreensões de lista são uma forma desse padrão usado em muitas linguagens de programação.)

Se houver dois predicados,que aplica critérios de seleção para o tipo T , eque aplica critérios adicionais para o tipo S , então os conjuntos para os dois tipos podem ser definidos:

O predicadoé aplicado ao ladocomo parte do predicado composto S que define S . Os dois predicados são combinados , portanto, ambos devem ser verdadeiros para que um valor seja selecionado. O predicadosubsume o predicado T , então S <: T .

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.

A conjunção de predicados foi expressa aqui pela aplicação do segundo predicado sobre o domínio de valores conforme o primeiro predicado. Vistos como tipos, Felis <: Felinae <: Felidae .

Se T subsume S ( T :> S ) então um procedimento, função ou expressão dado um valorcomo um operando (valor de parâmetro ou termo) poderá, portanto, 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 .

Esquemas de subtipagem

Os teóricos dos tipos fazem uma distinção entre subtipagem nominal , em que apenas tipos declarados de uma certa maneira podem ser subtipos um do outro, e subtipagem estrutural , em que a estrutura de dois tipos determina se um é ou não um subtipo do outro. A subtipagem orientada a objetos baseada em classe descrita 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 (ou seja, se eles definem todos os mesmos métodos ), então A é um subtipo de B , independentemente de um herdar do outro. Este chamadoa tipagem de pato é comum em linguagens orientadas a objetos tipadas dinamicamente. Regras de subtipagem estruturais sólidas para tipos diferentes de tipos de objetos também são bem conhecidas. [ citação necessária ]

As 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 pode ser convertido automaticamente em um do tipo B . A subtipagem induzida por subclasses em uma linguagem orientada a objetos geralmente é inclusiva; relações de subtipagem que relacionam inteiros e números de ponto flutuante, que são representados de forma diferente, são geralmente coercitivas.

Em quase todos os sistemas de tipos 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 faz com que seja uma pré -encomenda de tipos.

Tipos de registro

Subtipagem de largura e profundidade

Os tipos de registros dão origem aos conceitos de subtipagem de largura e profundidade . Eles expressam duas maneiras diferentes de obter 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). Como 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 subtipagem de profundidade , substitui os vários campos por seus subtipos. Ou seja, os campos do subtipo são subtipos dos campos do supertipo. Como qualquer operação com suporte para um campo no supertipo tem suporte para seu subtipo, qualquer operação viável no supertipo de registro é suportada pelo subtipo de registro. A 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 não pode fazer o mesmo para o campo 'x' de um ponto inteiro (que, no entanto, é um subtipo profundo do tipo ponto real) porque 1,5 não é um inteiro (consulte Variação ).

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

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

Tipos de funções

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

O tipo de parâmetro de S 1S 2 é dito contravariante porque a relação de subtipagem é invertida para ele, enquanto o tipo de retorno é covariante . Informalmente, essa inversão ocorre porque o tipo refinado é "mais liberal" nos tipos que aceita e "mais conservador" no tipo que retorna. Isto é exatamente o que funciona em Scala : uma função n -ary é internamente uma classe que herda o trait (que pode ser visto como uma interface geral em linguagens semelhantes a Java ), ondesão os tipos de parâmetros e B é seu tipo de retorno; " - " antes do tipo significa que o tipo é contravariante enquanto " + " significa covariante.

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 nessa área se concentrou na subtipagem comportamental , que além da segurança do sistema de tipos discutida neste artigo também exige que os subtipos preservem todas as invariantes garantidas pelos supertipos em algum contrato . [5] Esta definição de subtipagem é geralmente indecidível , então não pode ser verificada por um verificador de tipos .

A subtipagem de referências mutáveis ​​é semelhante ao tratamento de valores de parâmetros e valores de retorno. Referências somente de gravação (ou coletores ) são contravariantes, como valores de parâmetro; 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 invariáveis.

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 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 relacionadas por herança a Int32. No entanto Int32, pode ser considerado um subtipo de Int64, pois qualquer valor inteiro de 32 bits pode ser promovido para um valor inteiro de 64 bits.

O terceiro caso é uma consequência da contravariância de entrada de subtipagem de função . Suponha uma superclasse do tipo T tendo um método m retornando um objeto do mesmo tipo ( ou seja, o tipo de m é TT , observe também que o primeiro parâmetro de m é this/self) e uma classe derivada do tipo S de T . Por herança, o tipo de m em S é SS . Para que S seja um subtipo de T , o tipo de m em Sdeve ser um subtipo do tipo de m em T , ou seja: SS ≤: TT . Pela aplicação bottom-up da regra de subtipagem de funções, 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 .

A subtipagem e a herança são compatíveis quando todos os campos e métodos herdados do tipo derivado possuem tipos que são subtipos dos campos e métodos correspondentes do tipo herdado. [2]

Coerções

Em sistemas de subtipagem coercitiva, os subtipos são definidos por funções de conversão de tipo implícitas de subtipo para supertipo. Para cada relacionamento de subtipagem ( S <: T ), uma função de coerção coerce : ST é fornecida, e qualquer objeto s do tipo S é considerado como o objeto coerce ST ( s ) do tipo T . Uma função de coerção pode ser definida por composição: se S <: T e T <: U então spode ser considerado como um objeto do tipo u sob a coação composta ( coação T U coação S T ) . A coerção de tipo de um tipo para ele próprio coagir TT é a função identidade id T .

As funções de coerção para registros e subtipos de união disjunta podem ser definidas por componentes; no caso de registros estendidos por largura, a coerção de tipo simplesmente descarta quaisquer componentes que não estejam definidos no supertipo. A coerção de tipo para tipos de função pode ser dada por f' ( s ) = coagir S 2T 2 ( f ( coagir T 1S 1 ( t ))), refletindo a contravariância dos valores dos parâmetros e a covariância dos valores de retorno.

A função de coerção é determinada exclusivamente com base no subtipo e no supertipo . Assim, 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 coagido para um número de ponto flutuante (digamos, 2.0 : float ), então não é admissível coagir 2.1 : float para 2 : int , porque a coerção composta força floatfloat dado por coercer intfloatcoerce floatint seria então distinto da coerção de identidadeid flutuar .

Veja também

Notas

  1. ^ Cardelli, Lucas. Uma semântica de herança múltipla. Em G. Kahn, D. MacQueen e G. Plotkin, editores, Semantics of Data Types, volume 173 de Lecture Notes in Computer Science, páginas 51–67. Springer-Verlag, 1984. Versão completa em Informação e Computação, 76(2/3):138-164, 1988.
  2. ^ a b Cook, Hill & Canning 1990 .
  3. ^ Pierce, cap. 15 notas
  4. ^ Benjamin C. Pierce, tipos e linguagens de programação , MIT Press, 2002, 15.1 "Subsunção", p. 181-182
  5. ^ Barbara Liskov, Jeannette Wing, uma noção comportamental de subtipagem , ACM Transactions on Programming Languages ​​and Systems, Volume 16, Issue 6 (novembro de 1994), pp. 1811–1841. Uma versão atualizada apareceu como relatório técnico da CMU: Liskov, Barbara ; Wing, Jeannette (julho de 1999). "Subtipagem Comportamental Usando Invariantes e Restrições" ( PS ) . Recuperado em 2006-10-05 .

Referências

Livros didáticos

  • Benjamin C. Pierce, Tipos e linguagens de programação , MIT Press, 2002, ISBN 0-262-16209-1 , capítulo 15 (subtipagem de tipos de registro), 19.3 (tipos nominais vs. estruturais e subtipagem) e 23.2 (variedades de polimorfismo ) 
  • C. Szyperski, D. Gruntz, S. Murer, Software componente: além da programação orientada a objetos , 2ª ed., Pearson Education, 2002, ISBN 0-201-74572-0 , pp. 93–95 (uma apresentação de alto nível destinado a usuários de linguagem de programação) 

Papéis

Cook, William R.; Hill, Walter; Canning, Peter S. (1990). Herança não é subtipagem . Proc. 17º ACM SIGPLAN-SIGACT Symp. em Princípios de Linguagens de Programação (POPL). págs. 125-135. CiteSeerX  10.1.1.102.8635 . doi : 10.1145/96709.96721 . ISBN 0-89791-343-4.
  • Reynolds, John C. Usando a teoria das categorias para projetar conversões implícitas e operadores genéricos. Em ND Jones, editor, Proceedings of the Aarhus Workshop on Semantics-Directed Compiler Generation, número 94 em Lecture Notes in Computer Science. Springer-Verlag, janeiro de 1980. Também em Carl A. Gunter e John C. Mitchell, editores, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994).

Leitura adicional