Polimorfismo paramétrico

Em linguagens de programação e teoria dos tipos, polimorfismo paramétrico é uma forma de se tornar uma linguagem mais expressiva, enquanto continua mantendo toda sua tipagem estática segura. Usando o polimorfismo paramétrico, a função ou tipo de dado pode ser escrita genericamente para que possa suportar valores idênticos sem depender de seu tipo.^[1] Essas funções e tipos de dados são chamados funções genéricas e tipos de dados genéricos respectivamente e formam a base da programação genérica.

Por exemplo, a função append que junta duas listas pode ser construída para que não se preocupe com o tipo dos elementos: ela pode juntar listas de inteiros, listas de números reais, listas de strings, e assim por diante. Suponhamos que o tipo da variável a denota o tipo de elementos da lista. Então append pode ser escrito da forma [a] x [a] -> [a], onde [a] denota o tipo de listas cujos elementos são do tipo a. Dizemos que o tipo de append é parametrizado por a para todos os valores de a. (Note que como há apenas um único tipo de variável, a função não pode ser aplicada para qualquer par de listas: o par, assim como a lista resultante, deve consistir do mesmo tipo de elementos.) Para cada local no qual append é aplicado, o valor é decidido por a.

De acordo com Christopher Strachey,^[2] o polimorfismo paramétrico pode ser posto em contraste com o polimorfismo ad-hoc, no qual uma única função polimórfica pode ter um número distinto e potencialmente heterogêneo de implementações dependendo do tipo do(s) argumento(s) para o(s) qual(is) ela é aplicada. Dessa forma, o polimorfismo ad-hoc pode apenas suportar um número limitados de tipos distintos, desde que seja provida uma implementação separada para cada tipo.

História

O polimorfismo paramétrico foi primeiramente introduzido para linguagens de programação em ML em 1976. Hoje existe em Standard ML, OCaml, F#, Ada, Haskell, Visual Prolog, Scala, e outras. Java, C#, Visual Basic .NET e Delphi inseriram cada uma tipos "genéricos" para o polimorfismo paramétrico. Algumas implementações de tipos de polimorfismo são superficialmente similares ao polimorfismo paralelo por também introduzirem aspectos ad-hoc. Um exemplo é a especialização do template do C++.

A forma mais geral de polimorfismo é o "polimorfismo impredicativo de maior-rank". Duas restrições populares dessa forma são os polimorfismos de rank restrito (por exemplo, rank-1 ou polimorfismo prenex) e polimorfismo predicativos. Juntas, essas restrições formam o "polimorfismo de predicativo prenex", que é essencialmente a forma de polimorfismo encontrada no ML e mais recentemente em versões de Haskell.

Polimorfismo de alto posto

Polimorfismo de posto-1 (prenex)

Em um sistema polimórfico prenex, os tipos de variáveis podem não serem instanciados com tipos polimórficos. Isso é muito similar com o que é chamado "ML-style" ou "polimorfismo via-let" (tecnicamente polimorfismo via-let de ML tem poucas outras restrições de sintaxe). Essa restrição faz com que a distinção entre tipos polimórficos e não polimórficos seja muito importante; dessa forma em sistemas predicativos tipos polimórficos são as vezes referidos como tipos esquemas para distinguir eles de outros tipos (monomórficos), os quais são chamados às vezes de monótipos. Uma consequência é que todos os tipos podem ser escritos de uma forma que coloca todos os quantificadores na posição mais externa (prenex). Por exemplo, considere que a função append descrita acima, cujo tipo é [a] × [a] → [a]; para aplicar essa função para um par de listas, um tipo deve ser substituído pela variável a no tipo da função de forma que argumentos casam com o tipo da função resultante. Em um sistema impredicativo, o tipo sendo substituído pode ser qualquer um, incluindo o tipo que é polimórfico; assim append pode ser aplicada a pares de listas cujos elementos são de qualquer tipo - até mesmo para listas de funções polimórficas como o próprio append. O polimorfismo na linguagem ML e linguagens próximas é predicativo. Isso porque a predicatividade, junto com algumas outras restrições, faz com que o sistema do tipo seja simples o suficiente para a inferência do tipo ser possível. Em linguagens nas quais anotações explícitas do tipo são necessárias quando aplicadas a uma função polimórfica, a restrição da predicatividade é menos importante; dessa forma essas linguagens são geralmente impredicativas. Haskell consegue alcançar a inferência do tipo sem a predicatividade, mas com algumas poucas complicações.

Polimorfismo de posto-k

Para alguns valores fixos de k, o polimorfismo de posto-k é um sistema no qual o quantificador pode não aparecer na esquerda de k ou mais setas (quando o tipo é desenhado como uma árvore)^[1]

O tipo de inferência para polimorfismo de rank-2 é decidível, mas a reconstrução do posto-3 para cima não é.^[3]

Polimorfismo de posto-n (mais alto posto)

Polimorfismo de posto-n é um polimorfismo no qual os quantificadores podem aparecer na esquerda de várias setas arbitrariamente.

Predicatividade e impredicatividade

Polimorfismo predicativo

Em um sistema polimórfico paramétrico predicativo, um tipo ${\displaystyle \tau }$ contendo um tipo de veriável ${\displaystyle \alpha }$ pode não ser usada da mesma maneira que ${\displaystyle \alpha }$ é instanciado no tipo polimórfico. Dentre as teorias de tipos predicativos estão inclusas a Teoria dos Tipos de Martin-Löf e NuPRL.

Polimorfismo impredicativo

Polimorfismo impredicativo (também chamado de polimorfismo de primeira classe) é a mais poderosa forma de polimorfismo paramétrico.^[4] Uma definição é dita ser impredicativa se ela for auto-referenciável; na teoria dos tipos isso permite a instanciação de uma variável do tipo ${\displaystyle \tau }$ com qualquer tipo, incluindo tipos polimórficos, tais como o próprio ${\displaystyle \tau }$. Um exemplo disso é o Sistema F com o tipo de variável X do tipo ${\displaystyle T=\forall X.X\to X}$, onde X pode até referenciar o próprio T.

Na teoria dos tipos, os impredicativos mais frequentemente estudados lambda cálculos são baseados baseado no lambda cubo, especialmente o sistema F.^[1]

Polimorfismo paramétrico limitado

Em 1985, Luca Cardelli e Peter Wegner reconheceram as vantagens de se permitirem limites nos tipos de parâmetros. ^[5] Muitas operações requerem alguns conhecimentos dos tipos de dados, mas por outro lado trabalham parametricamente. Por exemplo, para checar se um item está incluso em uma lista, nós precisamos comparar os itens através da igualdade. Em Standard ML, tipos paramétricos da forma ’’a são restritos para que a operação de igualdade seja possível, assim a função poderia ter o tipo ’’a × ’’a list → bool e ’’a pode apenas ser um tipo com uma igualdade definida. Em Haskell, limites são alcançados através da requisição dos tipos pertencentes a uma classe de tipos; assim a mesma função tem o tipo ${\displaystyle {\scriptstyle Eq\,\alpha \,\Rightarrow \alpha \,\rightarrow \left[\alpha \right]\rightarrow Bool}}$ em Haskell. Na maioria das linguagens de programação orientadas a objeto que suporta polimorfismo paramétrico, os parâmetros podem ser forçados a serem subtipos de um dado tipo (veja polimorfismo de subtipo e o artigo de programação genérica).

Ver também

• Recursão polimórfica

Notas

Referências

• Strachey, Christopher (1967), Fundamental Concepts in Programming Languages (Lecture notes), Copenhagen: International Summer School in Computer Programming . Republished in: Higher-Order and Symbolic Computation. 13: 11–49. 2000. doi:10.1023/A:1010000313106 
• Hindley, J. Roger (1969), «The principal type scheme of an object in combinatory logic», American Mathematical Society, Transactions of the American Mathematical Society, 146: 29–60, JSTOR 1995158, MR 0253905, doi:10.2307/1995158 .
• Girard, Jean-Yves (1971). «Une Extension de l'Interpretation de Gödel à l'Analyse, et son Application à l'Élimination des Coupures dans l'Analyse et la Théorie des Types». Proceedings of the Second Scandinavian Logic Symposium (em French). Amsterdam. pp. 63–92. doi:10.1016/S0049-237X(08)70843-7  !CS1 manut: Língua não reconhecida (link)
• Girard, Jean-Yves (1972), Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur (Ph.D. thesis) (em French), Université Paris 7  !CS1 manut: Língua não reconhecida (link).
• Reynolds, John C. (1974), «Towards a Theory of Type Structure», Paris, Colloque sur la programmation, Lecture Notes in Computer Science, 19: 408–425, doi:10.1007/3-540-06859-7_148 .
• Milner, Robin (1978). «A Theory of Type Polymorphism in Programming». Journal of Computer and System Sciences. 17 (3): 348—375. doi:10.1016/0022-0000(78)90014-4 
• Cardelli, Luca; Wegner, Peter (dezembro de 1985). «On Understanding Types, Data Abstraction, and Polymorphism» (PDF). New York, NY, USA: ACM. ACM Computing Surveys. 17 (4): 471–523. ISSN 0360-0300. doi:10.1145/6041.6042 
• Pierce, Benjamin C. (2002). Types and Programming Languages. [S.l.]: MIT Press. ISBN 978-0-262-16209-8