Como a parametridade relacional pode ser motivada?

Existe alguma maneira natural de entender a essência da semântica relacional do polimorfismo paramétrico?

Acabei de começar a ler sobre a noção de parametridade relacional, como "Tipos, abstração e polimorfismo paramétrico" de John Reynolds, e estou tendo problemas para entender como a semântica relacional é motivada. A semântica de conjuntos faz todo o sentido para mim, e percebo que a semântica de conjuntos é insuficiente para descrever o polimorfismo paramétrico, mas o salto para a semântica relacional parece mágico, saindo completamente do nada.

Existe alguma maneira de explicá-lo ao longo das linhas "Assuma relações nos tipos e termos básicos, e então a interpretação dos termos derivados é apenas a relação natural entre ... uma coisa tão natural ... em sua linguagem de programação "? Ou alguma outra explicação natural?

Bem, a parametridade relacional é uma das idéias mais importantes introduzidas por John Reynolds; portanto, não deve ser surpresa que pareça mágica. Aqui está um conto de fadas sobre como ele pode ter inventado.

Suponha que você esteja tentando formalizar a ideia de que certas funções (identidade, mapa, dobra, reversão de listas) agem "da mesma maneira em muitos tipos", ou seja, você tem algumas idéias intuitivas sobre polimorfismo paramétrico e formulou algumas regras para criar tais mapas, isto é, o $\lambda$ cálcio polimórfico ou alguma variante inicial. Você percebe que a semântica ingênua da teoria dos conjuntos não está funcionando.

Por exemplo, podemos encarar o tipo

$$\forall X : \mathsf{Type} . X \to X,$$ que deve conter apenas o mapa de identidade, mas a semântica ingênua da teoria dos conjuntos permite funções indesejadas como $$\lambda X : \mathsf{Type} . \lambda a : X . \mathsf{if}\ (X = \lbrace 0, 1 \rbrace) \ \mathsf{then} \ 0 \ \mathsf{else}\ a.$$ Para eliminar esse tipo de coisa, precisamos impor algumas condições adicionais às funções. Por exemplo, poderíamos tentar alguma teoria de domínio: equipar cada conjunto $X$ com uma ordem parcial $\leq_X$ e exigir que todas as funções sejam monótonas. Mas isso não ajuda muito porque a função indesejada acima é constante ou identidade, dependendo do $X$ , e esses são mapas monótonos.

Uma ordem parcial $\leq$ é relfexiva, transitiva e anti-simétrica. Podemos tentar alterar a estrutura, por exemplo, podemos tentar usar uma ordem parcial estrita, uma ordem linear, uma relação de equivalência ou apenas uma relação simétrica. No entanto, em cada caso, alguns exemplos indesejados aparecem. Por exemplo, relações simétricas eliminam nossa função indesejada, mas permitem outras funções indesejadas (exercício).

E então você percebe duas coisas:

1. Os exemplos desejados nunca são eliminados, quaisquer que sejam as relações usadas no lugar de ordens parciais $\leq$ .
2. Para cada exemplo indesejado em particular que você olha, você pode encontrar uma relação que a elimine, mas não há uma única relação que elimine todas elas.

Então, você tem o brilhante pensamento de que as funções desejadas são aquelas que preservam todas as relações , e o modelo relacional nasce.

A resposta para sua pergunta está realmente na fábula de Reynolds (Seção 1). Deixe-me tentar interpretá-lo para você.

Em uma linguagem ou formalismo em que os tipos são tratados como abstrações , uma variável de tipo pode representar qualquer conceito abstrato. Não assumimos que os tipos sejam gerados por meio de alguma sintaxe dos termos de tipo, ou de uma coleção fixa de operadores de tipo, ou que possamos testar dois tipos quanto à igualdade, etc. Nesse idioma, se uma função envolver uma variável de tipo, o único a coisa que a função pode fazer com valores desse tipo é embaralhar os valores que ela recebeu. Ele não pode inventar novos valores desse tipo, porque não "sabe" o que é esse tipo! Essa é a ideia intuitiva da parametridade .

Então Reynolds pensou em como capturar matematicamente essa ideia intuitiva e percebeu o seguinte princípio. Suponha que instanciar a variável do tipo, digamos , a dois tipos de concreto diferentes, dizem A e A ' , em instâncias separadas, e se manter em nossa mente alguma correspondência R : A ↔ A ' entre os dois tipos de concreto. Então, podemos imaginar que, em um caso, forneçamos um valor x ∈ A à função e, no outro caso, um valor correspondente x ′ ∈ A ′ (onde "correspondente" significa que x e$t$$A$$A'$$R : A \leftrightarrow A'$$x \in A$$x' \in A'$$x$ são relacionados por R ). Então, como a função não sabe nada sobre os tipos que estamos fornecendo para t ou os valores desse tipo, ela deve tratar x e x ' exatamente da mesma maneira. Portanto, os resultados que obtemos da função devem corresponder novamente à relação R que mantemos em nossa mente, ou seja, sempre que o elemento x aparece no resultado de uma instância, o elemento x ' deve aparecer na outra instância. Assim,uma função parametricamente polimórfica deve preservar todas as correspondências relacionais possíveis entre instâncias possíveis de variáveis ​​de tipo.$x'$$R$$t$$x$$x'$$R$$x$$x'$

Essa ideia de preservação de correspondências não é nova. Os matemáticos sabem disso há muito tempo. Em um primeiro momento, eles pensaram que funções polimórficas deveriam preservar isomorfismos entre instanciações de tipo. Observe que isomorfismo significa alguma idéia de uma correspondência individual . Aparentemente, os isomorfismos foram originalmente chamados de "homomorfismos". Então eles perceberam que o que agora chamamos de "homomorfismos", isto é, alguma idéia de correspondências muitos-para-um , também seria preservado. Essa preservação tem o nome de transformação natural na teoria das categorias. Mas, se pensarmos profundamente, perceberemos que a preservação de homomorfismos é totalmente insatisfatória. Os tipos e A $A$$A'$nós mencionamos são completamente arbitrários. Se escolhermos como A ' e A ' como A , devemos obter a mesma propriedade. Então, por que a "correspondência muitos-para-um", um conceito assimétrico, deve desempenhar um papel na formulação de uma propriedade simétrica? Assim, Reynolds deu o grande passo de generalizar dos homomorfismos para as relações lógicas, que são correspondências muitos para muitos . O impacto total dessa generalização ainda não está totalmente esclarecido. Mas a intuição subjacente é bastante clara.$A$$A'$$A'$$A$

Há mais uma sutileza aqui. Enquanto as instanciações das variáveis ​​de tipo podem ser arbitrariamente variadas, os tipos constantes devem permanecer fixos. Portanto, quando formulamos a correspondência relacional para uma expressão de tipo com tipos de variáveis ​​e tipos constantes, devemos usar a relação escolhida sempre que a variável de tipo aparecer e a relação de identidade I K sempre que um tipo constante de K aparecer. Por exemplo, a expressão de relação para o tipo t × I n t → I n t × t seria R × I I n t → I $R$$I_K$$K$$t \times Int \to Int \times t$$R \times I_{Int} \to I_{Int} \times R$$f$$(x,n)$$(x',n)$$(m,x)$$(m,x')$. Observe que somos obrigados a testar a função colocando os mesmos valores para tipos constantes nos dois casos, e garantimos que obtemos os mesmos valores para tipos constantes nas saídas. Portanto, ao formular correspondências relacionais para expressões de tipo, devemos garantir que, inserindo relações de identidade (representando a ideia de que esses tipos serão consentidos), recuperemos relações de identidade, ou seja, . Esta é a extensão de identidade crucial$F(I_{A_1},\ldots,I_{A_n}) = I_{F(A_1,\ldots,A_n)}$ propriedade.

Para entender a parametridade intuitivamente, tudo o que você precisa fazer é escolher alguns tipos de funções da amostra, pensar em quais funções podem ser expressas desses tipos e pensar em como essas funções se comportam se você conectar instâncias diferentes de variáveis ​​de tipo e valores diferentes daquelas tipos de instanciação. Deixe-me sugerir alguns tipos de funções para você começar: , t → I n t , i n t → t , t × t → t × t , ( t → t ) → t , ( $t \to t$$t \to Int$$Int \to t$$t \times t \to t \times t$$(t \to t) \to t$ .$(t \to t) \to (t \to t)$

$\omega$

Além disso, é tentador identificar funções com o mesmo comportamento extensional, levando a uma relação de equivalência. A relação é parcial se excluirmos as funções "indefinidas", ou seja, as funções que "fazem loop" para alguma entrada bem formada.

Os modelos PER são uma generalização disso.

Outra maneira de ver esses modelos é como um caso (muito) especial dos modelos de conjuntos simples da Teoria dos Tipos de Homotopia . Nessa estrutura, os tipos são interpretados como (uma generalização de), conjuntos com relações e relações entre essas relações, etc. No nível mais baixo, simplesmente temos os modelos PER.

Finalmente, o campo da matemática construtiva viu o surgimento de noções relacionadas, em particular a Teoria dos Conjuntos de Bispo envolve a descrição de um conjunto, fornecendo elementos e uma relação explícita de igualdade, que deve ser uma equivalência. É natural esperar que alguns princípios da matemática construtiva entrem na teoria dos tipos.