Pourquoi une fonction de type polymorphe `forall t: Type, t-> t` doit-elle être la fonction d'identité?

Je suis nouveau dans la théorie des langages de programmation. Je regardais des conférences en ligne dans lesquelles l'instructeur a affirmé qu'une fonction de type polymorphe forall t: Type, t->tétait l'identité, mais n'a pas expliqué pourquoi. Quelqu'un peut-il m'expliquer pourquoi? Peut-être une preuve de la revendication des premiers principes.

La première chose à noter est que ce n'est pas nécessairement vrai. Par exemple, selon la langue, une fonction de ce type, en plus d'être la fonction d'identité, pourrait: 1) boucler pour toujours, 2) muter un état, 3) retourner null, 4) lever une exception, 5) effectuer des E / S, 6) bifurquer un thread pour faire autre chose, 7) faire des call/ccmanigances, 8) utiliser quelque chose comme Java Object.hashCode, 9) utiliser la réflexion pour déterminer si le type est un entier et l'incrémenter si c'est le cas, 10) utiliser la réflexion pour analyser la pile d'appels et faire quelque chose en fonction du contexte dans lequel il est appelé, 11) probablement beaucoup d'autres choses et certainement des combinaisons arbitraires de ce qui précède.

Ainsi, la propriété qui y conduit, la paramétricité, est une propriété du langage dans son ensemble et il existe des variations plus fortes et plus faibles de celui-ci. Pour de nombreux calculs formels étudiés en théorie des types, aucun des comportements ci-dessus ne peut se produire. Par exemple, pour le système F / le calcul lambda polymorphe pur, où la paramétricité a été étudiée pour la première fois, aucun des comportements ci-dessus ne peut se produire. Il n'a tout simplement pas d' exceptions, état mutable, null, call/cc, I / O, la réflexion, et il est fortement normalisant il ne peut pas boucler indéfiniment. Comme Gilles l'a mentionné dans un commentaire, le papier Theorems est gratuit!par Phil Wadler est une bonne introduction à ce sujet et ses références iront plus loin dans la théorie, en particulier la technique des relations logiques. Ce lien répertorie également d'autres articles de Wadler sur le thème de la paramétricité.

La paramétricité étant une propriété du langage, pour le prouver, il faut d'abord articuler formellement le langage puis un argument relativement compliqué. L'argument informel pour ce cas particulier en supposant que nous sommes dans le calcul lambda polymorphe est que, puisque nous ne savons rien, tnous ne pouvons effectuer aucune opération sur l'entrée (par exemple, nous ne pouvons pas l'incrémenter parce que nous ne savons pas si c'est le cas). un nombre) ou créer une valeur de ce type (pour tout ce que nous savons t= Void, un type sans aucune valeur). La seule façon de produire une valeur de type test de renvoyer celle qui nous est donnée. Aucun autre comportement n'est possible. Une façon de voir cela est d'utiliser une normalisation forte et de montrer qu'il n'y a qu'un seul terme de forme normale de ce type.

La preuve de cette affirmation est assez complexe, mais si c'est ce que vous voulez vraiment, vous pouvez consulter l' article original de Reynolds sur le sujet.

L'idée clé est qu'elle vaut pour les fonctions polymorphes paramétriques , où le corps d'une fonction polymorphe est le même pour toutes les instanciations monomorphes de la fonction. Dans un tel système, aucune hypothèse ne peut être faite sur le type d'un paramètre de type polymorphe, et si la seule valeur dans scope a un type générique, il n'y a rien à voir avec cela mais le renvoyer ou le passer à d'autres fonctions que vous '' ve défini, qui à son tour ne peut rien faire mais le retourner ou le passer .. .etc. Donc, à la fin, tout ce que vous pouvez faire est une chaîne de fonctions d'identité avant de retourner le paramètre.

Avec toutes les mises en garde que Derek mentionne, et en ignorant les paradoxes qui résultent de l'utilisation de la théorie des ensembles, permettez-moi d'esquisser une preuve dans l'esprit de Reynolds / Wadler.

Une fonction du type:

f :: forall t . t -> t

est une famille de fonctions indexées par type t .$f_t$$t$

L'idée est que, pour définir formellement des fonctions polymorphes, nous ne devons pas traiter les types comme des ensembles de valeurs, mais plutôt comme des relations. Les types de base, comme Intinduire des relations d'égalité - par exemple, deux Intvaleurs sont liées si elles sont égales. Les fonctions sont liées si elles mappent des valeurs liées à des valeurs liées. Le cas intéressant est celui des fonctions polymorphes. Ils mappent les types associés aux valeurs associées.

$f$$g$

forall t . t -> t

$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

Vous pouvez trouver plus de détails sur mon blog .

EDIT: Un commentaire ci-dessus a fourni la pièce manquante. Certaines personnes jouent délibérément avec des langues qui ne sont pas complètes. Je ne me soucie pas explicitement de ces langues. Un langage vraiment non utilisable et complètement utilisable est une chose difficile à concevoir. Le reste de tout cela se développe sur ce qui se passe en essayant d'appliquer ces théorèmes à un langage complet.

Faux!

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

où l' isopérateur compare deux variables pour l'identité de référence. Autrement dit, ils contiennent la même valeur. Pas une valeur équivalente, même valeur. Les fonctions fet gsont équivalentes par définition mais elles ne sont pas les mêmes.

Si cette fonction est passée elle-même, elle renvoie autre chose; sinon, il renvoie son entrée. Le quelque chose d'autre a le même type que lui, il peut donc être remplacé. En d'autres termes, ce fn'est pas l'identité, car f(f)revient g, alors que l'identité reviendrait f.

Pour que le théorème tienne, il doit assumer la capacité ridicule de réduire

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 vous êtes prêt à supposer que vous pouvez supposer que l'inférence de type beaucoup plus facile peut être gérée.

Si nous essayons de restreindre le domaine jusqu'à ce que le théorème se vérifie, nous finissons par devoir le restreindre terriblement.

• Fonctionnel pur (pas d'état mutable, pas d'E / S). OK je peux vivre avec ça. Beaucoup de temps, nous voulons exécuter des preuves sur les fonctions.
• Bibliothèque standard vide. meh.
• Non raiseet non exit. Maintenant, nous commençons à être contraints.
• Il n'y a pas de type inférieur.
• Le langage a une règle qui permet au compilateur de réduire la récursion infinie en supposant qu'il doit se terminer. Le compilateur est autorisé à rejeter la récursion infinie triviale.
• Le compilateur est autorisé à échouer s'il est présenté avec quelque chose qui ne peut pas être prouvé dans les deux cas.² Maintenant, la bibliothèque standard ne peut pas prendre les fonctions comme arguments. Huer.
• Il n'y en a pas nil. Cela commence à devenir problématique. Nous avons manqué de moyens pour faire face à 1 / 0.³
• Le langage ne peut pas faire d'inférence de type de branche et n'a pas de priorité pour quand le programmeur peut prouver une inférence de type que le langage ne peut pas. C'est assez mauvais.

L'existence des deux dernières contraintes a paralysé la langue. Bien qu'il soit encore complet sur Turing, le seul moyen d'en tirer un travail général est de simuler une plate-forme interne qui interprète un langage avec des exigences plus lâches.

¹ Si vous pensez que le compilateur peut en déduire celui-ci, essayez celui-ci

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 preuve que le compilateur ne peut pas faire cela dépend de l'aveuglement. Nous pouvons utiliser plusieurs bibliothèques pour nous assurer que le compilateur ne peut pas voir la boucle à la fois. De plus, nous pouvons toujours construire quelque chose où le programme fonctionnerait mais ne pourrait pas être compilé car le compilateur ne peut pas effectuer l'induction dans la mémoire disponible.

³ Quelqu'un pense que vous pouvez avoir ce retour nul sans que les types génériques arbitraires retournent nul. Cela paie une pénalité désagréable pour laquelle je n'ai vu aucun langage efficace qui puisse le payer.

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

ne doit pas compiler. Le problème fondamental est que l'indexation des tableaux d'exécution ne fonctionne plus.