¿Cuál es el formalismo para probar afirmaciones sobre la unicidad de funciones con ciertas firmas?

Question

Supongamos que quiero una función como

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

Una afirmación que he visto a menudo es que f tiene sólo una implementación, a saber, la 'función curry', es decir g => a => b => g(a, b)

Tomado al pie de la letra, esto no parece ser cierto, siempre puedo definir f como actuar de manera diferente a esto en casos especiales, p.puedo decir que es g => a => b => g(a, b) excepto cuando A = B y luego lo defino como g => a => b => g(b, a).

No obstante, es bastante claro lo que se entiende por "tiene una sola implementación".

Me gustaría saber el formalismo correcto en el que se pueden probar afirmaciones como las anteriores.

Supongo que sospecharía que es teoría de categorías.Lo anterior se parece un poco a la noción de una transformación natural, pero realmente no veo los detalles.

Answer 1

Estoy seguro de que existe una conexión con la teoría de categorías, pero en realidad puedes hacerlo con (lo que considero) una herramienta más simple:parametricidad.

La idea básica es que, cuando un lenguaje tiene la propiedad de que los tipos polimórficos hagan exactamente lo mismo para cada tipo del que se crean instancias (es decir,no hay una construcción tipográfica), podemos probar propiedades muy poderosas sobre el lenguaje, en forma de una relación lógica.

Esto evita exactamente la implementación del "caso especial" que usted describe en su pregunta.También vale la pena mencionar que estas implementaciones son todas extensivamente igual:pueden verse diferentes pero producir resultados iguales para insumos iguales.p.ej.puedes reemplazar cualquier término $t$ con $(\lambda x \ldotp x) t $ y obtener una función equivalente.

Las declaraciones sobre funciones sólo por su tipo generalmente se llaman teorema libre, llamado así por el artículo que presentó la idea: Teoremas gratis por Phil Wadler.Si está interesado en esta área, le recomiendo encarecidamente el artículo, ya que es una buena introducción al tema.

La idea detrás de esto en realidad se remonta mucho más atrás que ese artículo, hasta el trabajo de John Reynolds con el Sistema F y el "teorema de la abstracción", pero pasó un tiempo antes de que la idea se volviera popular.

De hecho, puedes generar teoremas libres en http://free-theorems.nomeata.de/, aunque puede que sea necesario un poco de manipulación para obtener información útil de los teoremas que ofrecen allí.

Si está interesado en la parametricidad utilizada para demostrar cosas distintas a los teoremas libres, como la seguridad de tipos, entonces La tesis de Amal Ahmed Es la mejor introducción que he visto.Realmente hace un buen trabajo al describir tipos semánticos:el tipo de un programa es en realidad una propiedad de cómo se ejecuta y qué produce, y lo que llamamos "tipos" son una aproximación sintáctica de estos tipos semánticos más generales.