Polimorfismo paramétrico

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

Em linguagens de programação e teoria de tipos , o polimorfismo paramétrico é uma maneira de tornar uma linguagem mais expressiva, mantendo a segurança de tipo estática completa . Usando 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. [1] Tais 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, 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 type a denotar o tipo de elementos nas listas. Então appendpode ser digitado

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

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

Seguindo Christopher Strachey , [2] 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 em linguagens de programação em ML em 1975. [3] Hoje existe em Standard ML , OCaml , F# , Ada , Haskell , Mercury , Visual Prolog , Scala , Julia , Python , TypeScript , C++ e outros. Java , C# , Visual Basic .NET e Delphicada um introduziu "genéricos" para polimorfismo paramétrico. Algumas implementações de polimorfismo de tipo são superficialmente semelhantes ao polimorfismo paramétrico, ao mesmo tempo em que introduzem aspectos ad hoc. Um exemplo é a especialização de modelo C++ .

A forma mais geral de polimorfismo é " polimorfismo impredicativo de nível superior ". Duas restrições populares desta forma são polimorfismo de posto restrito (por exemplo, polimorfismo de posto-1 ou prenex ) e polimorfismo predicativo. Juntas, essas restrições fornecem "polimorfismo prenex predicativo", que é essencialmente a forma de polimorfismo encontrada no ML e nas primeiras versões do Haskell.

Polimorfismo de classificação mais alta

Polimorfismo Rank-1 (prenex)

Em um sistema polimórfico prenex , as variáveis ​​de tipo não podem ser instanciadas com tipos polimórficos. [4] 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 muito importante a distinção entre tipos polimórficos e não polimórficos; assim, em sistemas predicativos, os tipos polimórficos às vezes são chamados de esquemas de tipos para distingui-los dos tipos comuns (monomórficos), que às vezes são chamados de monotipos . Uma consequência é que todos os tipos podem ser escritos em uma forma que coloca todos os quantificadores na posição mais externa (prenex). Por exemplo, considere aappendfunção descrita acima, que tem o tipo

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

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

Como exemplo prático, OCaml (um descendente ou dialeto de ML ) realiza inferência de tipo e suporta polimorfismo impredicativo, mas em alguns casos quando 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). [1]

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

Polimorfismo Rank - n ("ranking superior")

O polimorfismo Rank - n é um polimorfismo no qual os quantificadores podem aparecer à esquerda de um número arbitrário de setas.

Predicatividade e impredicatividade

Polimorfismo predicativo

Em um sistema polimórfico paramétrico predicativo, um tipocontendo uma variável de tiponão pode ser usado de tal forma queé instanciado para um tipo polimórfico. As teorias de tipo predicativo incluem a teoria de tipo de Martin-Löf e NuPRL .

Polimorfismo impredicativo

O polimorfismo impredicativo (também chamado de polimorfismo de primeira classe ) é a forma mais poderosa de polimorfismo paramétrico. [6] Diz-se que uma definição é impredicativa se for auto-referencial; na teoria de tipos isso permite a instanciação de uma variável em um tipocom qualquer tipo, incluindo tipos polimórficos, comoem si. Um exemplo disso é o System F com a variável de tipo X no tipo, onde X poderia até se referir ao próprio T.

Na teoria dos tipos , os λ-cálculos impredicativos mais freqüentemente estudados são baseados naqueles do cubo lambda , especialmente no Sistema F. [1]

Polimorfismo paramétrico limitado

Em 1985, Luca Cardelli e Peter Wegner reconheceram as vantagens de permitir limites nos parâmetros de tipo. [7] Muitas operações requerem algum conhecimento dos tipos de dados, mas podem funcionar de forma paramétrica. Por exemplo, para verificar se um item está incluído em uma lista, precisamos comparar os itens para igualdade. No Standard ML , os parâmetros de tipo do formulário ''a são restritos para que a operação de igualdade esteja disponível, assim a função teria o tipo ''a × ''a lista → bool e ''a só pode ser um tipo com igualdade. Em Haskell, a delimitação é obtida exigindo que os tipos pertençam a uma classe de tipos ; assim a mesma função tem o tipoem Haskel. Na maioria das linguagens de programação orientadas a objetos que suportam 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 ).

Veja também

Notas

  1. ^ a b c Perfurar 2002 .
  2. ^ Strachey 1967 .
  3. ^ Milner, R., Morris, L., Newey, M. "A Logic for Computable Functions com tipos reflexivos e polimórficos", Proc. Conferência sobre Programas de Prova e Melhoria , Arc-et-Senans (1975)
  4. ^ Benjamin C. Pierce; Benjamin C. (Professor Pierce, Universidade da Pensilvânia) (2002). Tipos e Linguagens de Programação . Imprensa do MIT. ISBN 978-0-262-16209-8.
  5. ^ Pierce 2002 , p. 359.
  6. ^ Pierce 2002 , p. 340.
  7. ^ Cardelli & Wegner 1985 .

Referências