haskell - tipos - ¿Cómo se demuestra que una función es única para su tipo?

imprimir en haskell

Question

id es la única función de tipo a -> a , y fst la única función de tipo (a,b) -> a . En estos casos simples, esto es bastante sencillo de ver. Pero, en general, ¿cómo harías para probar esto? ¿Qué pasa si hay múltiples funciones posibles del mismo tipo?

Alternativamente, dado el tipo de función, ¿cómo se deriva la función única (si es verdadera) de ese tipo?

Editar: estoy particularmente interesado en lo que sucede cuando comenzamos a agregar restricciones en los tipos.

Answer 1

El resultado que está buscando deriva de la parametricidad de Reynolds, y Wadler lo mostró de forma más famosa en teoremas de forma gratuita .

La forma más elegante de probar los resultados básicos de parametricidad. He visto utilizar la noción de "Tipo Singleton". Esencialmente, dado cualquier ADT

data Nat = Zero | Succ Nat

existe una familia indexada (también conocida como GADT)

data SNat n where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)

y podemos darle una semántica a nuestro lenguaje "borrando" todos los tipos a un lenguaje sin tipo, de modo que Nat y SNat borren a la misma cosa. Entonces, según las reglas de tipeo del lenguaje

id (x :: SNat n) :: SNat n

SNat n tiene solo un habitante (su singleton), ya que la semántica está dada por borrado, las funciones no pueden usar el tipo de sus argumentos, por lo que el único valor retornable de id en cualquier Nat es el número que le asignó. Este argumento básico puede extenderse para demostrar la mayoría de los resultados de parametricidad y fue utilizado por Karl Crary en A Simple Proof Technique for Parametricity Results, aunque la presentación que tengo aquí está inspirada en Stone y Harper.