Parametricidade

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

Ideia

Considere este exemplo, baseado em um conjunto X e no tipo T ( X ) = [ XX ] 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 ) = ff , é intuitivamente independente do conjunto X . A família de todas essas funções duas vezes X , parametrizada 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 ” . Parametricidade é a propriedade abstrata desfrutada pelas famílias que agem uniformemente, como duas vezes , 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 injetáveis ​​com números naturais. A função correspondente ao número natural n é dada pela regra f f n , ou seja, o numeral polimórfico de Church para n . Em contraste, o conjunto de todas as famílias ad hoc seria demasiado grande para ser um conjunto.

História

O teorema da parametricidade foi originalmente formulado 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 de parametricidade para derivar teoremas sobre funções parametricamente polimórficas com base em seus tipos.

Implementação de linguagem de programação

A parametricidade é a base para muitas transformações de programas implementadas em compiladores para a linguagem de programação Haskell . Estas 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 lenta , Haskell suporta certas operações primitivas - como o operador seq- que permitem o chamado "rigor seletivo", permitindo ao programador forçar 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 da parametricidade geral não é válido para programas Haskell; portanto, essas transformações são doentias em geral.

Tipos dependentes

Veja também

Referências

  1. ^ Reynolds, JC (1983). "Tipos, abstração e polimorfismo paramétrico" (PDF) . Processando informação . Holanda do Norte, Amsterdã. páginas 513–523.
  2. ^ Wadler, Philip (setembro de 1989). "Teoremas de graça!". 4ª Conferência Internacional em Programação Funcional e Arquitetura de Computadores . Londres.
  3. ^ Johann, Patrícia; Janis Voigtlaender (janeiro de 2004). “Teoremas livres na presença de seq”. Proc., Princípios de Linguagens de Programação . páginas 99–110. doi :10.1145/964001.964010.

links externos

  • Wadler: Parametricidade
Obtido em "https://en.wikipedia.org/w/index.php?title=Parametricity&oldid=1186887176"