Polimorfismo paramétrico - Parametric polymorphism

Em linguagens de programação e teoria de tipo , o polimorfismo paramétrico é uma maneira de tornar uma linguagem mais expressiva, enquanto ainda mantém a segurança de tipo estática total . Usando o polimorfismo paramétrico , uma função ou um tipo de dados pode ser escrito genericamente para que possa manipular valores de forma idêntica, sem depender de seu tipo. Essas funções e tipos de dados são chamados de funções genéricas e tipos de dados genéricos, respectivamente, e formam a base da programação genérica .

Por exemplo, uma função appendque une duas listas pode ser construída de forma que não se importe com o tipo de elementos: ela pode anexar listas de inteiros , listas de números reais , listas de strings e assim por diante. Deixe a variável de tipo a denotar o tipo de elementos nas listas. Então appendpode ser digitado

forall a. [a] × [a] -> [a]

onde [a]denota o tipo de listas com elementos do tipo a . Dizemos que o tipo de appendé parametrizado por a para todos os valores de a . (Observe que, uma vez que existe apenas um tipo de variável, a função não pode ser aplicada a qualquer par de listas: o par, assim como a lista de resultados, deve consistir no mesmo tipo de elementos) Para cada local onde appendé aplicado, um o valor é decidido por a .

Seguindo Christopher Strachey , o polimorfismo paramétrico pode ser contrastado com o polimorfismo ad hoc , no qual uma única função polimórfica pode ter várias implementações distintas e potencialmente heterogêneas, dependendo do tipo de argumento (s) ao qual é aplicada. Assim, o polimorfismo ad hoc geralmente só pode suportar um número limitado de tais tipos distintos, uma vez que uma implementação separada deve ser fornecida para cada tipo.

História

O polimorfismo paramétrico foi introduzido pela primeira vez nas linguagens de programação em ML em 1975. Hoje ele existe em ML padrão , OCaml , F # , Ada , Haskell , Mercury , Visual Prolog , Scala , Julia , Python , TypeScript , C ++ e outros. Java , C # , Visual Basic .NET e Delphi introduziram "genéricos" para polimorfismo paramétrico. Algumas implementações de polimorfismo de tipo são superficialmente semelhantes ao polimorfismo paramétrico, embora também introduzam aspectos ad hoc. Um exemplo é a especialização de template C ++ .

A forma mais geral de polimorfismo é " polimorfismo impredicativo de classificação superior ". Duas restrições populares desta forma são polimorfismo de classificação restrita (por exemplo, polimorfismo de classificação 1 ou prenex ) e polimorfismo predicativo. Juntas, essas restrições fornecem "polimorfismo prenex predicativo", que é essencialmente a forma de polimorfismo encontrada em ML e nas primeiras versões de Haskell.

Polimorfismo de classificação superior

Polimorfismo Rank-1 (prenex)

Em um sistema polimórfico prenex , as variáveis de tipo não podem ser instanciadas com tipos polimórficos. Isso é muito semelhante ao que é chamado de "estilo ML" ou "polimorfismo Let" (tecnicamente, o polimorfismo Let do ML tem algumas outras restrições sintáticas). Essa restrição torna a distinção entre tipos polimórficos e não polimórficos muito importante; portanto, em sistemas predicativos, os tipos polimórficos às vezes são chamados de esquemas de tipo para distingui-los dos tipos comuns (monomórficos), que às vezes são chamados de monótipos . Uma consequência é que todos os tipos podem ser escritos em uma forma que coloque todos os quantificadores na posição mais externa (prenex). Por exemplo, considere a appendfunção descrita acima, que tem tipo

forall a. [a] × [a] -> [a]

Para aplicar esta função a um par de listas, um tipo deve ser substituído pela variável a no tipo da função de forma que o tipo dos argumentos corresponda ao tipo de função resultante. Em um sistema impredicativo , o tipo a ser substituído pode ser qualquer tipo, incluindo um tipo que é ele próprio polimórfico; assim, appendpode ser aplicado a pares de listas com elementos de qualquer tipo - até mesmo a listas de funções polimórficas, como appendela mesma. Polimorfismo na linguagem ML é predicativo. Isso ocorre porque a predicatividade, junto com outras restrições, torna o sistema de tipos simples o suficiente para que a inferência completa de tipos seja sempre possível.

Como um exemplo prático, OCaml (um descendente ou dialeto de ML ) realiza inferência de tipo e suporta polimorfismo impredicativo, mas em alguns casos quando o polimorfismo impredicativo é usado, a inferência de tipo do sistema é incompleta, a menos que algumas anotações de tipo explícitas sejam fornecidas pelo programador.

Polimorfismo Rank- k

Para algum valor fixo k , o polimorfismo rank- k é um sistema no qual um quantificador pode não aparecer à esquerda de k ou mais setas (quando o tipo é desenhado como uma árvore).

A inferência de tipo para polimorfismo de classificação 2 é decidível, mas a reconstrução para classificação 3 e acima não é.

Polimorfismo Rank- n ("rank superior")

O polimorfismo Rank- n é o polimorfismo no qual os quantificadores podem aparecer à esquerda de muitas setas arbitrariamente.

Predicatividade e impredicatividade

Polimorfismo predicativo

Em um sistema polimórfico paramétrico predicativo, um tipo contendo uma variável de tipo não pode ser usado de forma que seja instanciado para um tipo polimórfico. As teorias de tipo predicativas incluem a teoria de tipo de Martin-Löf e NuPRL . ${\ displaystyle \ tau}$ ${\ displaystyle \ alpha}$ ${\ displaystyle \ alpha}$

Polimorfismo impredicativo

O polimorfismo impredicativo (também chamado de polimorfismo de primeira classe ) é a forma mais poderosa de polimorfismo paramétrico. Uma definição é considerada impredicativa se for autorreferencial; na teoria dos tipos, isso permite a instanciação de uma variável em um tipo com qualquer tipo, incluindo tipos polimórficos, como ele mesmo. Um exemplo disso é o Sistema F com a variável de tipo X no tipo , onde X pode até se referir ao próprio T. ${\ displaystyle \ tau}$ ${\ displaystyle \ tau}$ ${\ displaystyle T = \ forall XX \ to X}$

Em teoria dos tipos , o mais freqüentemente estudada impredicativa digitado λ-cálculos são baseados naqueles do cubo lambda , especialmente Sistema F .

Polimorfismo paramétrico limitado

Em 1985, Luca Cardelli e Peter Wegner reconheceram as vantagens de permitir limites nos parâmetros de tipo. Muitas operações requerem algum conhecimento dos tipos de dados, mas, de outra forma, podem funcionar parametricamente. Por exemplo, para verificar se um item está incluído em uma lista, precisamos comparar os itens para igualdade. No ML padrão , os parâmetros de tipo da forma '' a são restritos para que a operação de igualdade esteja disponível, portanto, a função teria o tipo '' a × '' uma lista → bool e '' a só pode ser um tipo com definido igualdade. Em Haskell , a limitação é obtida exigindo que os tipos pertençam a uma classe de tipos ; portanto, a mesma função tem o tipo em Haskell. Na maioria das linguagens de programação orientadas a objetos que oferecem suporte ao polimorfismo paramétrico, os parâmetros podem ser restritos a subtipos de um determinado tipo (consulte Polimorfismo de subtipo e o artigo sobre programação genérica ). ${\ displaystyle {\ scriptstyle Eq \, \ alpha \, \ Rightarrow \ alpha \, \ rightarrow \ left [\ alpha \ right] \ rightarrow Bool}}$

Veja também

Notas

Referências

Strachey, Christopher (1967), Fundamental Concepts in Programming Languages (notas da aula), Copenhagen: International Summer School in Computer Programming. Republicado em: Strachey, Christopher (2000). Computação Simbólica e de Ordem Superior . 13 : 11–49. doi : 10.1023 / A: 1010000313106 . Ausente ou vazio |title=( ajuda )
Hindley, J. Roger (1969), "The principal type scheme of an object in combinatory logic", Transactions of the American Mathematical Society , 146 : 29-60, doi : 10.2307 / 1995158 , JSTOR 1995158 , MR 0253905.
Girard, Jean-Yves (1971). "Une Extension de l'Interpretation de Gödel à l'Analyse, et son Application à l'Elimination des Coupures dans l'Analyse et la Théorie des Types". Proceedings of the Second Scandinavian Logic Symposium (em francês). Amsterdam. pp. 63–92. doi : 10.1016 / S0049-237X (08) 70843-7 .
Girard, Jean-Yves (1972), Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur (tese de doutorado) (em francês), Université Paris 7.
Reynolds, John C. (1974), "Towards a Theory of Type Structure", Colloque Sur la Programmation , Lecture Notes in Computer Science , Paris, 19 : 408–425, doi : 10.1007 / 3-540-06859-7_148 , ISBN 978-3-540-06859-4.
Milner, Robin (1978). "A Theory of Type Polymorphism in Programming" (PDF) . 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). "Sobre tipos de compreensão, abstração de dados e polimorfismo" (PDF) . Pesquisas de computação ACM . 17 (4): 471–523. CiteSeerX 10.1.1.117.695 . doi : 10.1145 / 6041.6042 . ISSN 0360-0300 .
Pierce, Benjamin C. (2002). Tipos e linguagens de programação . MIT Press. ISBN 978-0-262-16209-8.

Languages

In other projects