Subtipagem

Na teoria da linguagem de programação , a subtipagem (também chamada de polimorfismo de subtipo ou polimorfismo de inclusão ) é uma forma de polimorfismo de tipo . Um subtipo é um tipo de dados 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), escritos 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 (escrita como S <: T ,   ST , [1] ou   S ≤: T  ) significa que qualquer termo do tipo S pode ser usado com segurança em qualquer contexto onde um termo de tipo T é esperado. A semântica precisa da subtipagem aqui depende crucialmente dos detalhes de como "ser usado com segurança" e "qualquer contexto" são definidos por um determinado tipo de formalismo ou 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 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 de polimorfismo , enquanto as técnicas de polimorfismo paramétrico seriam consideradas programação genérica .

As 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. [2] 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 funcional, 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 funcional também fornecem alguma forma, geralmente restrita, de polimorfismo paramétrico. Num cenário teórico, é desejável estudar a interação dos dois recursos; 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 na lógica matemática (ver Lógica ordenada por ordem ). A subtipagem não deve ser confundida com a noção de herança (de classe ou objeto) de linguagens orientadas a objetos; [3] subtipagem é uma relação entre tipos (interfaces na linguagem orientada a objetos), enquanto 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 a 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). [4]

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 é frequentemente chamado de princípio de 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. 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 tipo . (Consulte § Tipos de funções 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. 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<: 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:

a função max ( x como número , y como número ) é se x < y , então retorne y, caso contrário , retorne x final        
        
         
    
         

Se inteiro e real forem subtipos de Numbere um operador de comparação com um número arbitrário for definido para ambos os tipos, então valores de qualquer tipo poderão ser passados ​​para esta função. No entanto, a própria possibilidade de implementar tal operador restringe fortemente o tipo Number (por exemplo, não se pode comparar um número inteiro com um número complexo) e, na verdade, apenas comparar números inteiros com números 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 [5] é 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 pertença ao 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 listando valores. Tipos definidos pelo usuário, como registros (estruturas, interfaces) ou classes, são definidos intencionalmente por uma declaração de tipo explícita ou pelo uso de 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 é um superconjunto do conjunto S , de modo que todo membro de S também é membro de T .
  • Um tipo pode ser incluído em mais de um tipo: os supertipos de S se cruzam em S .
  • Se S <: T (e portanto ST ), então T , o predicado que circunscreve o conjunto T , deve fazer parte do predicado S (no 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 o mesmo tipo se o sistema de tipos distinguir os tipos pelo nome).

Em termos de especificidade de informação, um subtipo é considerado mais específico do que qualquer um dos seus supertipos, porque contém pelo menos tanta informação quanto cada um deles. Isto pode aumentar a aplicabilidade ou relevância do subtipo (o número de situações em que pode ser aceite ou introduzido), em comparação com os seus supertipos "mais gerais". A desvantagem de ter esta informação mais detalhada é que ela representa escolhas incorporadas que reduzem a prevalência do subtipo (o número de situações que podem gerá-lo ou produzi-lo).

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 em 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 aplicam critérios de seleção para o tipo T e que aplicam critérios adicionais para o tipo S , então conjuntos para os dois tipos podem ser definidos:

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

Por exemplo: existe uma subfamília de espécies de felinos 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 através 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 subsume S ( T :> S ), então um procedimento, função ou expressão dado um valor como um operando (valor de parâmetro ou termo) será, portanto, capaz de operar sobre esse valor como um do tipo T , porque . No exemplo acima, poderíamos esperar que a função ofSubfamily 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 poderia dizer que se objetos do tipo A podem manipular todas as mensagens que 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 de tipo dinâmico. Regras sólidas de subtipagem estrutural para outros tipos além dos tipos de objeto também são bem conhecidas. [ carece de fontes ]

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 automaticamente convertido em um do tipo B . A subtipagem induzida pela subclasse 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 o torna 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 . Expressam duas maneiras diferentes de obter um novo tipo de registro que permite as mesmas operações que o 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 largura aparecerá no subtipo largura. Assim, qualquer operação viável no supertipo será suportada pelo subtipo.

O segundo método, denominado 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 suportada por um campo no supertipo é suportada pelo 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 ao campo 'x' de um ponto real. um ponto inteiro (que, no entanto, é um subtipo profundo do tipo de ponto real) porque 1,5 não é um número inteiro (consulte Variância ).

A subtipagem de registros pode ser definida no Sistema 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 subtipagem de tipos de união disjunta rotulados (como tipos de dados algébricos ). A regra para subtipagem de largura é invertida: cada tag que aparece no subtipo de largura deve aparecer no supertipo de largura.

Tipos de função

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 de 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 S 1S 2 é considerado contravariante porque a relação de subtipagem é invertida para ele, enquanto o tipo de retorno é covariante . Informalmente, esta inversão ocorre porque o tipo refinado é “mais liberal” nos tipos que aceita e “mais conservador” no tipo que devolve. Isso é 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 do tipo Java ), onde estão os tipos de parâmetros, e é 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 nesta área focou na subtipagem comportamental , que além da segurança do sistema de tipos discutida neste artigo também exige que os subtipos preservem todos os invariantes garantidos pelos supertipos em algum contrato . [6] 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 valores de parâmetros e valores de retorno. Referências somente de gravação (ou sinks ) são contravariantes, como valores de parâmetros; referências somente leitura (ou fontes ) são covariantes, como valores de retorno. 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). 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 há relação por herança com Int32. No entanto, Int32pode ser considerado um subtipo, Int64pois qualquer valor inteiro de 32 bits pode ser promovido para um valor inteiro de 64 bits.

O terceiro caso é uma consequência da subtipagem da função contravariância de entrada . 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 . [ carece de fontes ] Para que S seja um subtipo de T o tipo de m em S deve ser um subtipo do tipo de m em T [ carece de fontes ] , ou seja: SS ≤: TT . Pela aplicação bottom-up da regra de subtipagem de 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 .

Subtipagem e 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. [3]

Coerções

Em sistemas de subtipagem coercitiva, os subtipos são definidos por funções implícitas de conversão de tipo 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 s pode ser considerado como um objeto do tipo u sob a coerção composta ( coerce TUcoerce ST ). A coerção de tipo de um tipo para si mesmo coagir TT é a função de identidade id T .

Funções de coerção para registros e subtipos de união disjunta podem ser definidas em componentes; no caso de registros com largura estendida, 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' ( t ) = coerce S 2T 2 ( f ( coerce 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 de acordo com o subtipo e o 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 número 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 coerce floatfloat dado por coerce intfloatcoerce floatint seria então distinto da coerção de identidade id float .

Veja também

Notas

  1. ^ Copestake, Ann. Implementando gramáticas de estrutura de recursos digitadas. Vol. 110. Stanford: publicações CSLI, 2002.
  2. ^ 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 Information and Computation, 76(2/3):138–164, 1988.
  3. ^ ab Cook, Hill & Canning 1990.
  4. ^ Pierce, cap. 15 notas
  5. ^ Benjamin C. Pierce, Tipos e linguagens de programação , MIT Press, 2002, 15.1 "Subsunção", p. 181-182
  6. ^ Barbara Liskov, Jeannette Wing, Uma noção comportamental de subtipagem , ACM Transactions on Programming Languages ​​and Systems, Volume 16, Edição 6 (novembro de 1994), pp. Uma versão atualizada apareceu como relatório técnico da CMU: Liskov, Barbara ; Asa, Jeannette (julho de 1999). "Subtipagem comportamental usando invariantes e restrições" ( PS ) . Recuperado em 05/10/2006 .

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, Component software: Beyond Object-Oriented Programming , 2ª ed., Pearson Education, 2002, ISBN 0-201-74572-0 , pp. destinado a usuários de linguagem de programação) 

Papéis

Cozinheiro, William R.; Colina, Walter; Canning, Peter S. (1990). Herança não é subtipagem . Processo. 17º Simpl. ACM SIGPLAN-SIGACT. sobre 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

Obtido em "https://en.wikipedia.org/w/index.php?title=Subtyping&oldid=1204020914"