¿Por qué una función con tipo polimórfico `forall t: Type, t-> t` debe ser la función de identidad?

Soy nuevo en la teoría del lenguaje de programación. Estaba viendo algunas conferencias en línea en las que el instructor afirmó que una función con tipo polimórfico forall t: Type, t->tsería la identidad, pero no explicó por qué. ¿Alguien puede explicarme por qué? Tal vez una prueba de la afirmación de los primeros principios.

Lo primero a tener en cuenta es que esto no es necesariamente cierto. Por ejemplo, dependiendo del idioma, una función con ese tipo, además de ser la función de identidad, podría: 1) hacer un bucle para siempre, 2) mutar algún estado, 3) devolver null, 4) lanzar una excepción, 5) realizar alguna E / S, 6) bifurcar un hilo para hacer otra cosa, 7) hacer call/cctravesuras, 8) usar algo como el de Java Object.hashCode, 9) usar la reflexión para determinar si el tipo es un número entero e incrementarlo si es así, 10) usar la reflexión para analizar la pila de llamadas y hacer algo basado en el contexto dentro del cual se llama, 11) probablemente muchas otras cosas y ciertamente combinaciones arbitrarias de lo anterior.

Entonces, la propiedad que conduce a esto, la parametricidad, es una propiedad del lenguaje en su conjunto y hay variaciones más fuertes y más débiles. Para muchos de los cálculos formales estudiados en la teoría de tipos, ninguno de los comportamientos anteriores puede ocurrir. Por ejemplo, para el Sistema F / el cálculo lambda polimórfico puro, donde se estudió por primera vez la parametricidad, ninguno de los comportamientos anteriores puede ocurrir. Simplemente no tiene excepciones, el estado mutable, null, call/cc, E / S, la reflexión, y está fuertemente normalizando por lo que no puede reproducirse en bucle para siempre. Como Gilles mencionó en un comentario, ¡ Theorems de papel gratis!por Phil Wadler es una buena introducción a este tema y sus referencias irán más allá en la teoría, específicamente en la técnica de las relaciones lógicas. Ese enlace también enumera algunos otros documentos de Wadler sobre el tema de la parametricidad.

Dado que la parametricidad es una propiedad del lenguaje, para probarlo se requiere primero articular formalmente el lenguaje y luego un argumento relativamente complicado. El argumento informal para este caso particular, suponiendo que estamos en el cálculo lambda polimórfico es que, dado que no sabemos nada, tno podemos realizar ninguna operación en la entrada (por ejemplo, no podemos incrementarla porque no sabemos si es un número) o cree un valor de ese tipo (por lo que sabemos t= Void, un tipo sin ningún valor). La única forma de producir un valor de tipo tes devolver el que se nos da. No hay otros comportamientos posibles. Una forma de ver eso es usar una fuerte normalización y demostrar que solo hay un término de forma normal de este tipo.

La prueba del reclamo es bastante compleja, pero si eso es lo que realmente desea, puede consultar el documento original de Reynolds sobre el tema.

La idea clave es que se cumple para las funciones polimórficas paramétricas , donde el cuerpo de una función polimórfica es el mismo para todas las instancias monomórficas de la función. En dicho sistema, no se pueden hacer suposiciones sobre el tipo de un parámetro de tipo polimórfico, y si el único valor en el alcance tiene un tipo genérico, no hay nada que ver con él, sino devolverlo o pasarlo a otras funciones que usted ' he definido, que a su vez no puede hacer nada más que devolverlo o pasarlo .. .etc. Entonces, al final, todo lo que puede hacer es una cadena de funciones de identidad antes de devolver el parámetro.

Con todas las advertencias que menciona Derek, e ignorando las paradojas que resultan del uso de la teoría de conjuntos, permítanme esbozar una prueba en el espíritu de Reynolds / Wadler.

Una función del tipo:

f :: forall t . t -> t

es una familia de funciones indexadas por tipo t .$f_t$$t$

La idea es que, para definir formalmente funciones polimórficas, no deberíamos tratar los tipos como conjuntos de valores, sino más bien como relaciones. Tipos básicos, como Intinducir relaciones de igualdad, por ejemplo, dos Intvalores están relacionados si son iguales. Las funciones están relacionadas si asignan valores relacionados a valores relacionados. El caso interesante son las funciones polimórficas. Asignan tipos relacionados a valores relacionados.

En nuestro caso, queremos establecer una relación entre dos funciones polimórficas y g del tipo:$f$$g$

forall t . t -> t

Suponga que el tipo está relacionado con el tipo t . La primera función f asigna el tipo s a un valor: aquí, el valor en sí es una función f s del tipo s → s . La segunda función asigna el tipo t a otro valor g t del tipo t → t . Decimos que f está relacionado con g si los valores f $s$$t$$f$$s$$f_s$$s \to s$$t$$g_t$$t \to t$$f$$g$$f_s$$g_t$

fst$f_s$$f_t$

()()t()t((), c)ct$f_{(\,)}$$f_t$$f_{(\,)}$()()$f_t$cc()c$f_t$$id_t$tfid

Puedes encontrar más detalles en mi blog .

EDITAR: Un comentario anterior ha proporcionado la pieza que falta. Algunas personas están jugando deliberadamente con idiomas menos completos. Explícitamente no me importan esos lenguajes. Un lenguaje realmente útil que no sea completo es una locura difícil de diseñar. Todo lo demás se expande sobre lo que sucede tratando de aplicar estos teoremas a un lenguaje completo.

¡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

donde el is operador compara dos variables para la identidad de referencia. Es decir, contienen el mismo valor. No es un valor equivalente, el mismo valor. Funciones fy gson equivalentes por alguna definición, pero no son lo mismo.

Si esta función se pasa a sí misma, devuelve algo más; de lo contrario, devuelve su entrada. El algo más tiene el mismo tipo que sí mismo, por lo tanto, puede ser sustituido. En otras palabras, fno es la identidad, porquef(f) regresa g, mientras que la identidad volvería f.

Para que el teorema se mantenga tiene que asumir la capacidad ridícula de reducir

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]¹

Si está dispuesto a asumir que puede asumir que se puede manejar la inferencia de tipos mucho más fácil.

Si tratamos de restringir el dominio hasta que se mantenga el teorema, terminamos teniendo que restringirlo terriblemente lejos.

• Funcional puro (sin estado mutable, sin IO). OK, puedo vivir con eso. Muchas veces queremos ejecutar pruebas sobre funciones.
• Biblioteca estándar vacía. meh
• No raisey no exit. Ahora estamos empezando a estar limitados.
• No hay tipo de fondo.
• El lenguaje tiene una regla que permite al compilador colapsar la recursión infinita suponiendo que debe terminar. El compilador puede rechazar la recursividad trivial infinita.
• El compilador puede fallar si se le presenta algo que no se puede probar de ninguna manera .² Ahora la biblioteca estándar no puede tomar funciones como argumentos. Abucheo.
• No existe nil. Esto está empezando a ser problemático. Nos hemos quedado sin formas de lidiar con 1 / 0.³
• El lenguaje no puede hacer inferencias de tipo de rama y no tiene una anulación para cuando el programador puede probar una inferencia de tipo que el idioma no puede. Esto es muy malo

La existencia de las dos últimas restricciones ha paralizado el lenguaje. Si bien aún está completando Turing, la única forma de obtener un trabajo de propósito general es simular una plataforma interna que interprete un lenguaje con requisitos más flexibles.

¹ Si crees que el compilador puede deducir ese, prueba 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]

² La prueba de que el compilador no puede hacer esto depende del cegamiento. Podemos usar varias bibliotecas para asegurarnos de que el compilador no pueda ver el ciclo a la vez. Además, siempre podemos construir algo donde el programa funcionaría pero no podría compilarse porque el compilador no puede realizar la inducción en la memoria disponible.

³ Alguien piensa que puede devolver este valor nulo sin que los tipos genéricos arbitrarios devuelvan nulo. Esto paga una penalidad desagradable por la cual no he visto un lenguaje efectivo que pueda pagarlo.

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

No debe compilar. El problema fundamental es que la indexación de la matriz en tiempo de ejecución ya no funciona.