Parametricidade

Na teoria da linguagem de programação , a parametricidade é uma propriedade de uniformidade abstrata desfrutada por funções polimórficas parametricamente , que captura a intuição de que todas as instâncias de uma função polimórfica agem da mesma maneira.

Considere este exemplo, baseado em um conjunto X e o tipo T ( X ) = [ X → X ] de funções de X para si mesmo. A função de ordem superior duas vezes _X  : T ( X ) → T ( X ) dada por duas vezes _X ( f ) = f ∘ f , é intuitivamente independente do conjunto X . A família de todas essas funções duas vezes _X , parametrizadas por conjuntos X , é chamada de " função parametricamente polimórfica ". Simplesmente escrevemos duas vezes para toda a família dessas funções e escrevemos seu tipo como X . T ( X ) → T ( X ). As funções individuais duas vezes _X são chamadas de componentes ou instâncias da função polimórfica. Observe que todas as funções componentes duas vezes _X agem "da mesma maneira" porque são dadas pela mesma regra. Outras famílias de funções obtidas escolhendo uma função arbitrária de cada T ( X ) → T ( X ) não teriam tal uniformidade. Elas são chamadas de " funções polimórficas ad hoc " . Parametricalidade é a propriedade abstrata desfrutada pelas famílias de ação uniforme, como twice , que as distingue das famílias ad hoc . Com uma formalização adequada da parametricidade, é possível provar que as funções parametricamente polimórficas do tipo X . T ( X ) → T ( X ) são um-para-um com números naturais. A função correspondente ao número natural n é dada pela regra f f ⁿ , ou seja, o numeral de Church polimórfico para n . Em contraste, a coleção de todas as famílias ad hoc seria muito grande para ser um conjunto. ${\displaystyle \forall }$${\displaystyle \forall }$ ${\displaystyle \mapsto }$

O teorema da parametricidade foi originalmente declarado por John C. Reynolds , que o chamou de teorema da abstração . ^[1] Em seu artigo "Teoremas de graça!", ^[2] Philip Wadler descreveu uma aplicação da parametricidade para derivar teoremas sobre funções parametricamente polimórficas com base em seus tipos.

A parametricalidade é a base para muitas transformações de programa implementadas em compiladores para a linguagem de programação Haskell . Essas transformações eram tradicionalmente consideradas corretas em Haskell por causa da semântica não estrita de Haskell. Apesar de ser uma linguagem de programação preguiçosa , Haskell suporta certas operações primitivas — como o operador seq— que permitem a chamada "rigidez seletiva", permitindo que o programador force a avaliação de certas expressões. Em seu artigo "Teoremas livres na presença de seq ", ^[3] Patricia Johann e Janis Voigtlaender mostraram que, devido à presença dessas operações, o teorema geral da parametricalidade não é válido para programas Haskell; portanto, essas transformações são insustentáveis ​​em geral.

• Polimorfismo paramétrico
• Linguagem de programação não estrita

• Wadler: Parametricidade