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

18

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.

abhishek
la source
3
Je pensais que cette question devait être en double, mais je ne la trouve pas. cs.stackexchange.com/questions/341/… est une sorte de suivi. La référence standard est Theorems gratuitement! par Phil Wadler.
Gilles 'SO- arrête d'être méchant'
1
Essayez de construire une fonction générique avec ce type qui fait autre chose. Vous constaterez qu'il n'y en a pas.
Bergi
@Bergi Oui, je n'ai pas pu trouver de contre-exemple, mais je ne savais toujours pas comment le prouver.
abhishek
Mais quelles ont été vos observations lorsque vous avez essayé d'en trouver une? Pourquoi les tentatives que vous avez faites n'ont-elles pas fonctionné?
Bergi
@Gilles Vous vous souvenez peut-être de cs.stackexchange.com/q/19430/14663 ?
Bergi

Réponses:

32

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.

Derek Elkins a quitté SE
la source
1
Comment le système F a-t-il évité les boucles infinies que le système de type ne peut pas détecter? C'est classé comme insoluble dans le cas général.
Joshua
2
@Joshua - la preuve d'impossibilité standard pour le problème d'arrêt commence avec l'hypothèse qu'il existe une boucle infinie en premier lieu. Donc, l'invoquer pour se demander pourquoi le système F n'a pas de boucles infinies est un raisonnement circulaire. Plus largement, le système F n'est pas presque complet de Turing, donc je doute qu'il satisfasse l'une des hypothèses de cette preuve. Il est facilement assez faible pour qu'un ordinateur prouve que tous ses programmes se terminent (pas de récursivité, pas de boucles while, seulement très faible pour les boucles, etc.).
Jonathan Cast
@Joshua: c'est insoluble dans le cas général , ce qui n'empêche pas de le résoudre dans de nombreux cas particuliers. En particulier, il a été prouvé que chaque programme qui se trouve être un système bien typé F s'arrête: il existe une preuve uniforme qui fonctionne pour tous ces programmes. Évidemment, cela signifie qu'il existe d' autres programmes, qui ne peuvent pas être saisis dans le système F ...
cody
15

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.

jmite
la source
8

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 .ftt

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.

fg

forall t . t -> t

stfsfssstgtttfgfsgt

fstfsft

()()t()t((), c)ctf()ftf()()()Ftcc()cFtjettfid

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

Bartosz Milewski
la source
-2

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.

Joshua
la source
@Bergi: J'ai construit un contre-exemple.
Joshua
1
Veuillez prendre un moment pour réfléchir à la différence entre votre réponse et les deux autres. La première phrase de Derek est «La première chose à noter est que ce n'est pas nécessairement vrai». Et puis il explique quelles propriétés d'une langue la rendent vraie. jmite explique également ce qui le rend vrai. En revanche, votre réponse donne un exemple dans un langage non spécifié (et peu commun) sans aucune explication. (Quel est le foilquantificateur de toute façon?) Ce n'est pas du tout utile.
Gilles 'SO- arrête d'être méchant'
1
@DW: si a est f alors le type de a est le type de f qui est aussi le type de g et donc le contrôle de type devrait passer. Si un vrai compilateur le supprimait, j'utiliserais le cast d'exécution que les vraies langues ont toujours pour que le système de type statique se trompe et il n'échouerait jamais au moment de l'exécution.
Joshua
2
Ce n'est pas ainsi que fonctionne un vérificateur de caractères statique. Il ne vérifie pas que les types correspondent pour une seule entrée spécifique. Il existe des règles de type spécifiques, qui visent à garantir que la fonction vérifie typiquement toutes les entrées possibles. Si vous avez besoin d'utiliser un transtypage, cette solution est beaucoup moins intéressante. Bien sûr, si vous contournez le système de type, le type de fonction ne garantit rien - pas de surprise là-bas!
DW
1
@DW: Vous manquez le point. Il y a suffisamment d'informations pour que le vérificateur de type statique prouve que le code est sûr pour le type s'il avait l'esprit de le trouver.
Joshua