O que é o formalismo para provar afirmações sobre a exclusividade de funções, determinadas assinaturas

Question

Suponha que eu quero uma função como

f: ((A, B) -> C) -> A -> B -> C

Uma declaração já vi muitas vezes feita é que f tem apenas uma implementação, a saber, "curry função', i.é. g => a => b => g(a, b)

Tomado pelo valor de face este não parece ser realmente verdadeira, eu sempre pode definir f como agir de maneira diferente deste em casos especiais, e.g.O que posso dizer é g => a => b => g(a, b) exceto quando A = B e então eu defini-la como g => a => b => g(b, a).

No entanto, é intuitivamente claro o suficiente o que se entende por "foi apenas uma implementação'.

Gostaria de saber o correto formalismo em que afirmações como a acima pode ser provado.

Em um palpite, eu suspeito que é a categoria de teoria?Acima sente um pouco como a noção de um natural de transformação, mas eu realmente não vejo os detalhes.

Answer 1

Tenho certeza de que existe uma ligação à categoria de teoria, mas você pode realmente fazer com ele (o que eu considero ser ) uma ferramenta mais simples:parametricity.

Eles ideia básica é que, quando uma língua tem a propriedade de que tipos polimórficos fazer exatamente a mesma coisa para cada tipo eles são instanciados para (i.e.não há typecase construção), podemos provar muito poderosas propriedades sobre a linguagem, na forma de uma relação lógica.

Isso impede exatamente o "caso especial" implementação que você descreva-nos a sua questão.Vale ressaltar também que estas implementações são todos extensionally igual:eles podem parecer um pouco diferentes, mas produzir resultados iguais para a igualdade de entradas.exemplo:você pode substituir qualquer termo $t$ com $(\lambda x \ldotp x) t $ e obter uma função equivalente.

As declarações sobre funções apenas do seu tipo geralmente são chamados livre teorema, em homenagem ao papel que introduziu a idéia de: Teoremas de Graça por Phil utilitário de linha de comandos.Se você está interessado nesta área, eu recomendo o papel, já que é uma boa introdução ao assunto.

A ideia subjacente a esta, na verdade, vai muito mais além do que o papel, a John Reynolds de trabalho com Sistema de F e a "abstração teorema", mas demorou um pouco antes de a idéia tornou-se popular.

Você pode realmente gerar livre teoremas em http://free-theorems.nomeata.de/, embora possa levar um pouco de massagem para obter informações úteis a partir da teoremas eles dão lá.

Se você estiver interessado em parametricity usado para provar outras coisas que não a livre teoremas, como o tipo de seguro e, em seguida, Amal Ahmed tese é a melhor apresentação que eu já vi.Ela realmente faz um bom trabalho de descrever a semântica tipos:o tipo de programa é, na verdade, propriedade do como ele é executado e o que ele produz, e o que chamamos de "tipos" são um sintática aproximação mais geral semântica tipos.