Normalmente, você usa a parametridade binária para provar as equivalências do programa. Não é natural fazer isso com um modelo unário, pois ele fala apenas de um programa por vez.
Normalmente, você usa um modelo unário se tudo o que lhe interessa é uma propriedade unária. Por exemplo, veja nosso rascunho recente, Tipos superficialmente subestruturais , no qual provamos um resultado de solidez de tipo usando um modelo unário. Como a solidez fala sobre o comportamento de um programa (se então diverge ou reduz a um valor v : A ), um modelo unário é suficiente. Se quiséssemos provar as equivalências do programa além disso, precisaríamos de um modelo binário.e:Av:A
Edição: Acabei de perceber que, se você olhar para o nosso artigo, ele se parece com um modelo antigo de relações lógicas / realizabilidade. Eu deveria dizer um pouco mais sobre o que o torna (e outros modelos) paramétrico. Basicamente, um modelo é paramétrico quando você pode provar o lema de extensão de identidade para ele: ou seja, para qualquer expressão de tipo, se todas as variáveis de tipo livres estiverem ligadas a relações de identidade, a expressão de tipo será a relação de identidade. Nós não o provamos explicitamente como um lema (não sei por que, mas você raramente precisa fazer modelos operacionais), mas essa propriedade é essencial para a solidez de nossa linguagem.
A definição de "relação" e "relação de identidade" na parametridade é realmente um pouco em disputa, e essa liberdade é realmente essencial se você deseja suportar tipos sofisticados, como tipos superiores ou tipos dependentes, ou deseja trabalhar com estruturas semânticas mais sofisticadas. A explicação mais acessível sobre isso que conheço está no rascunho de Bob Atkey, Parametridade relacional para tipos superiores .
Se você tem um bom apetite pela teoria das categorias, ela foi formulada de maneira abstrata por Rosolini em seu artigo Gráficos reflexivos e polimorfismo paramétrico . Desde então, foi desenvolvido ainda mais por Dunphy e Reddy em seu artigo Parametric Limits , e também por Birkedal, Møgelberg e Petersen em modelos teóricos de domínio do polimorfismo paramétrico .