Por que uma função com o tipo polimórfico `forall t: Type, t-> t` deve ser a função de identidade?

18

Eu sou novo em teoria da linguagem de programação. Eu estava assistindo algumas palestras on-line nas quais o instrutor alegava que uma função com tipo polimórfico forall t: Type, t->tseria a identidade, mas não explicava o porquê. Alguém pode me explicar por quê? Talvez uma prova da reivindicação dos primeiros princípios.

abhishek
fonte
3
Eu pensei que esta pergunta deveria ser uma duplicata, mas não consigo encontrá-la. cs.stackexchange.com/questions/341/… é um tipo de acompanhamento. A referência padrão é Teoremas de graça! de Phil Wadler.
Gilles 'SO- stop be evil'
1
Tente construir uma função genérica com esse tipo que faça qualquer outra coisa. Você verá que não há.
Bergi 17/10/19
@ Bergi Sim, não consegui encontrar nenhum exemplo de contador, mas ainda não tinha certeza de como provar isso.
Abhishek #
Mas quais foram suas observações quando você tentou encontrar uma? Por que alguma tentativa que você fez não funcionou?
Bergi 18/10/19
@Gilles Talvez você se lembre de cs.stackexchange.com/q/19430/14663 ?
Bergi 18/10/19

Respostas:

32

A primeira coisa a observar é que isso não é necessariamente verdade. Por exemplo, dependendo do idioma, uma função com esse tipo, além de ser a função de identidade, poderia: 1) loop para sempre, 2) alterar algum estado, 3) retornar null, 4) lançar uma exceção, 5) executar alguma E / S, 6) bifurque um thread para fazer outra coisa, 7) faça call/cctravessuras, 8) use algo como Java Object.hashCode, 9) use reflexão para determinar se o tipo é um número inteiro e, se necessário, incremente-o, 10) use reflexão para analisar a pilha de chamadas e faça algo com base no contexto em que é chamado, 11) provavelmente muitas outras coisas e certamente combinações arbitrárias das anteriores.

Portanto, a propriedade que leva a isso, a parametridade, é uma propriedade da linguagem como um todo e existem variações mais fortes e mais fracas dela. Para muitos dos cálculos formais estudados na teoria dos tipos, nenhum dos comportamentos acima pode ocorrer. Por exemplo, para o Sistema F / cálculo lambda polimórfico puro, onde a parametridade foi estudada pela primeira vez, nenhum dos comportamentos acima pode ocorrer. Ele simplesmente não tem exceções, estado mutável, null, call/cc, I / O, reflexão, e é normalizar fortemente para que ele não pode fazer um loop para sempre. Como Gilles mencionou em um comentário, o jornal Theorems for free!por Phil Wadler é uma boa introdução a esse tópico e suas referências serão mais aprofundadas na teoria, especificamente na técnica das relações lógicas. Esse link também lista alguns outros trabalhos de Wadler sobre o tema da parametridade.

Como a parametridade é uma propriedade da linguagem, para provar isso, é necessário primeiro articular formalmente a linguagem e depois um argumento relativamente complicado. O argumento informal para este caso em particular, assumindo que estamos no cálculo lambda polimórfico, é que, como não sabemos nada sobre t, não podemos executar nenhuma operação na entrada (por exemplo, não podemos incrementá-la porque não sabemos se é um número) ou crie um valor desse tipo (pelo que sabemos t= Void, um tipo sem nenhum valor). A única maneira de produzir um valor do tipo té retornar o que é dado a nós. Nenhum outro comportamento é possível. Uma maneira de ver isso é usar forte normalização e mostrar que existe apenas um termo de forma normal desse tipo.

Derek Elkins deixou o SE
fonte
1
Como o Sistema F evitou ciclos infinitos que o sistema de tipos não pode detectar? Isso é classificado como insolúvel no caso geral.
Joshua
2
@ Josué - a prova de impossibilidade padrão para o problema de parada começa com a suposição de que há um loop infinito em primeiro lugar. Portanto, invocá-lo para questionar por que o Sistema F não possui loops infinitos é um raciocínio circular. De maneira mais ampla, o Sistema F não está quase completo de Turing, então duvido que satisfaça qualquer uma das suposições dessa prova. É facilmente fraco o suficiente para um computador provar que todos os seus programas terminam (sem recursão, sem loops de tempo, apenas muito fraco para loops, etc.).
Jonathan fundido
@ Josué: é insolúvel no caso geral , o que não impede a solução em muitos casos especiais. Em particular, provou-se que todo programa que é um termo F de sistema bem digitado é interrompido: há uma prova uniforme que funciona para todos esses programas. Obviamente, isso significa que existem outros programas, que não podem ser digitados no sistema de F ...
Cody
15

A prova da alegação é bastante complexa, mas se é isso que você realmente deseja, pode conferir o artigo original de Reynolds sobre o assunto.

A idéia principal é que ele se aplica a funções parametricamente polimórficas , em que o corpo de uma função polimórfica é o mesmo para todas as instanciações monomórficas da função. Nesse sistema, nenhuma suposição pode ser feita sobre o tipo de parâmetro do tipo polimórfico e, se o único valor no escopo tiver um tipo genérico, não há nada a ver com isso, mas devolvê-lo ou passá-lo para outras funções que você ' definido, que por sua vez não pode fazer nada além de devolvê-lo ou passá-lo ... etc. Portanto, no final, tudo o que você pode fazer é alguma cadeia de funções de identidade antes de retornar o parâmetro.

jmite
fonte
8

Com todas as ressalvas mencionadas por Derek e ignorando os paradoxos resultantes do uso da teoria dos conjuntos, deixe-me esboçar uma prova no espírito de Reynolds / Wadler.

Uma função do tipo:

f :: forall t . t -> t

é uma família de funções indexados por tipo .ftt

A idéia é que, para definir formalmente funções polimórficas, não devemos tratar tipos como conjuntos de valores, mas como relações. Tipos básicos, como Intinduzir relações de igualdade - por exemplo, dois Intvalores são relacionados se forem iguais. As funções são relacionadas se mapearem valores relacionados para valores relacionados. O caso interessante são as funções polimórficas. Eles mapeiam tipos relacionados para valores relacionados.

No nosso caso, queremos estabelecer uma relação entre duas funções polimórficas e do tipo:fg

forall t . t -> t

Suponha que o tipo esteja relacionado ao tipo . A primeira função mapeia os tipos para um valor - aqui, o próprio valor é uma função do tipo . A segunda função mapeia o tipo para outro valor do tipo . Dizemos que está relacionado com se os valores e estão relacionados. Como esses valores são funções, eles são relacionados se mapearem valores relacionados a valores relacionados.stfsfssstgtttfgfsgt

O passo crucial é usar o teorema da parametridade de Reynolds, que diz que qualquer termo está relacionado com ele. No nosso caso, a função festá relacionada a si mesma. Em outras palavras, se sestiver relacionado a t, também estará relacionado a .fsft

Agora podemos escolher qualquer relação entre dois tipos e aplicar esse teorema. Vamos escolher o primeiro tipo como o tipo de unidade (), que possui apenas um valor, também chamado (). Manteremos o segundo tipo tarbitrário, mas não vazio. Vamos escolher uma relação entre ()e tpara ser simplesmente um par ((), c), onde chá algum valor do tipo t(uma relação é apenas um subconjunto do produto cartesiano de conjuntos). O teorema da parametridade nos diz que deve estar relacionado a . Eles devem mapear valores relacionados para valores relacionados. A primeira função não tem muita escolha, deve mapear o único valor para . Portanto, a segunda funçãof()ftf()()()ftdeve mapear cpara c(os únicos valores relacionados a ()). Desde cé completamente arbitrária, concluímos que é e, uma vez que é completamente arbitrária, é .ftEudttfid

Você pode encontrar mais detalhes no meu blog .

Bartosz Milewski
fonte
-2

EDIT: Um comentário acima forneceu a peça que faltava. Algumas pessoas brincam deliberadamente com idiomas completos que não são turing. Eu explicitamente não me importo com esses idiomas. Uma linguagem realmente comum, não turing-complete, é uma coisa louca e difícil de projetar. O resto disso se expande sobre o que acontece tentando aplicar esses teoremas a uma linguagem completa.

Falso!

function f(a): forall t: Type, t->t
    function g(a): forall t: Type, t->t
       return (a is g) ? f : a
    return a is f ? g : a

onde o isoperador compara duas variáveis ​​para a identidade de referência. Ou seja, eles contêm o mesmo valor. Não é um valor equivalente, mesmo valor. Funções fe gsão equivalentes por alguma definição, mas não são iguais.

Se essa função é aprovada, ela retorna outra coisa; caso contrário, ele retorna sua entrada. A outra coisa tem o mesmo tipo que ela mesma, portanto, pode ser substituída. Em outras palavras, fnão é a identidade, porque f(f)retorna g, enquanto a identidade retornaria f.

Para que o teorema se mantenha, ele deve assumir a capacidade ridícula de reduzir

function cantor(n, <z, a>) : forall t: t: Type int, <int, t> -> <int, t>
    return n > 1 ? cantor((n % 2 > 0) ? (n + 1) : n / 2, <z + 1, a>) : <z, a>
return cantor(1000, <0, a>)[1]¹

Se você estiver disposto a assumir que pode assumir a inferência de tipo muito mais fácil, pode ser manipulada.

Se tentarmos restringir o domínio até que o teorema se mantenha, acabamos tendo que restringi-lo terrivelmente.

  • Funcional puro (sem estado mutável, sem IO). OK, eu posso viver com isso. Muito tempo queremos executar provas sobre funções.
  • Biblioteca padrão vazia. meh.
  • Não raisee não exit. Agora estamos começando a ficar constrangidos.
  • Não há tipo de fundo.
  • O idioma possui uma regra que permite ao compilador recolher recursões infinitas, assumindo que ele deve terminar. É permitido ao compilador rejeitar a recursão infinita trivial.
  • É permitido ao compilador falhar se for apresentado algo que não possa ser provado de nenhuma maneira .² Agora a biblioteca padrão não pode aceitar funções como argumentos. Vaia.
  • Não existe nil. Isso está começando a ficar problemático. Ficamos sem maneiras de lidar com 1 / 0.³
  • O idioma não pode fazer inferências de tipo de ramificação e não possui uma substituição para quando o programador puder provar uma inferência de tipo que o idioma não pode. Isso é muito ruim.

A existência das duas últimas restrições prejudicou a linguagem. Enquanto Turing ainda está completo, a única maneira de obter um trabalho de propósito geral é simular uma plataforma interna que interpreta um idioma com requisitos mais flexíveis.

¹ Se você acha que o compilador pode deduzir esse, tente este

function fermat(z) : int -> int
    function pow(x, p)
        return p = 0 ? 1 : x * pow(x, p - 1)
    function f2(x, y, z) : int, int, int -> <int, int>
        left = pow(x, 5) + pow(y, 5)
        right = pow(z, 5)
        return left = right
            ? <x, y>
            : pow(x, 5) < right
                ? f2(x + 1, y, z)
                : pow(y, 5) < right
                    ? f2(2, y + 1, z)
                    : f2(2, 2, z + 1)
    return f2(2, 2, z)
function cantor(n, <z, a>) : forall t: t: Type int, <int, t> -> <int, t>
    return n > 1 ? cantor((n % 2 > 0) ? (n + 1) : n / 2, <z + 1, a>) : <z, a>
return cantor(fermat(3)[0], <0, a>)[1]

² A prova de que o compilador não pode fazer isso depende de ofuscamento. Podemos usar várias bibliotecas para garantir que o compilador não possa ver o loop de uma só vez. Além disso, sempre podemos construir algo em que o programa funcionaria, mas não pôde ser compilado porque o compilador não pode executar a indução na memória disponível.

³ Alguém pensa que você pode ter esse retorno nulo sem que tipos genéricos arbitrários retornem nulo. Isso paga uma penalidade desagradável pela qual não vi uma linguagem eficaz que possa pagá-la.

function f(a, b, c): t: Type: t[],int,int->t
    return a[b/c]

não deve compilar. O problema fundamental é que a indexação de array em tempo de execução não funciona mais.

Joshua
fonte
@ Bergi: Eu construí um contra-exemplo.
Joshua
1
Reserve um momento para refletir sobre a diferença entre sua resposta e as outras duas. A frase de abertura de Derek é "A primeira coisa a se notar é que isso não é necessariamente verdade". E então ele explica quais propriedades de uma linguagem a tornam verdadeira. jmite também explica o que a torna verdadeira. Por outro lado, sua resposta fornece um exemplo em um idioma não especificado (e incomum) com explicação zero. (Qual é o foilquantificador, afinal?) Isso não ajuda em nada.
Gilles 'SO- stop be evil'
1
@ DW: se a é f, então o tipo de a é o tipo de f, que também é o tipo de ge, portanto, a verificação de tipo deve passar. Se um compilador real o expusesse, eu usaria o elenco de tempo de execução que as linguagens reais sempre têm para o sistema de tipo estático errar e nunca falharia no tempo de execução.
18717 Joshua
2
Não é assim que um typechecker estático funciona. Não verifica se os tipos correspondem a uma única entrada específica. Existem regras de tipo específicas, destinadas a garantir que a função verifique tipicamente todas as entradas possíveis. Se você precisar usar um typecast, essa solução será muito menos interessante. Obviamente, se você ignorar o sistema de tipos, o tipo de uma função não garante nada - não há surpresa!
DW
1
@ DW: Você perdeu o ponto. Há informações suficientes para o verificador de tipo estático para provar que o código é do tipo seguro se tiver a inteligência de encontrá-lo.
19717 Joshua