Je me permets de concentrer dans ce commentaire ma réponse à celui-ci ainsi qu'à cet autre commentaire, étant donné que tu y reprends les mêmes idées. Tu as été clair malgré l'heure tardive, j'espère pouvoir faire de même en cette heure plus matinale.
Il me semble que dans ton approche de la question, tu mélanges plusieurs problématiques. Dans l'exemple que tu donnes ici, tu montres surtout comment un système de type avancé (ici une forme restreinte de type dépendant) permet d'être plus précis sur la spécification d'un code et comment un compilateur peut en tirer partie pour générer un code optimisé (ici en supprimant un test de comparaison à l'exécution rendu inutile par ton type amount). Cela rejoint un exemple que j'avais donné dans la dernière dépêche sur Haskell, où je montrais comment utiliser les GADT (types de données algébriques généralisés) pour exprimer la proposition : « tout arbre binaire parfait non vide a une racine ». Ce qui permettait de coder la fonction qui extrait cette racine sans que le code généré par le compilateur ait à vérifier à l'exécution que l'arbre était non vide (c'était déjà spécifié dans le type de la fonction).
Revenons à présent au sujet précis du journal : le décalage à droite bit à bit. Dans un autre commentaire, tu précises à bon droit que l'arithmétique modulaire est la base de tous les processeurs courants et dans le cas présent on fait de l'arithmétique dans l'anneau Z/nZ avec n = 2^64. Se pose alors la question que doit faire cette fonction de décalage à droite ? et tu réponds toi même : « [elle] ne devrait répondre qu'au seul problème du quotient d'un entier machine entre 0 et 2n - 1 par une puissance positive quelconque de 2 ». Ce à quoi je te répondrai : l'architecture X86 fait cela en restant dans le cadre de l'arithmétique modulaire, et ne la mélange pas avec de l'arithmétique sur les entiers. En effet prenons le type de cette fonction : function my_shr (u : unsigned_64; a : natural) return unsigned_64. Elle prend en paramètre un entier non signé sur 64 bits, un entier naturel et renvoie un entier non signé sur 64 bits. Or pour opérer au sein de l'anneau sus-mentionné, elle doit donc associer un élément de cette anneau au paramètre a : natural, puis renvoyer ensuite le quotient d'une division euclidienne effectuée au sein de l'anneau. Les processeurs X86 on fait le choix de prendre l'élément 2 ^ (a % 64), ce qui peut sembler assez « naturel » lorsque l'on pratique l'arithmétique modulaire. Exemple en OCaml sur mon X86 :
En revanche, de ce que j'ai compris, l'architecture ARM ne voit pas cela du tout comme une opération d'arithmétique modulaire, mais semble considérer une telle donnée (un entier non signé sur 64 bit) comme un suite finie de 0 et de 1 ou plutôt comme une suite stationnaire de valeur nulle à partir du rang 64 et si tu lui donne la suite u(n) elle te renvoie la suite u(n+a). Ce qui semble être le comportement que tu souhaiterais, mais ce n'est pas du tout le point de vue de l'arithmétique modulaire. Autrement dit, elle voit un entier de 64 bit comme un entier naturel compris entre 0 et 2^64 - 1 représenté en base 2, effectue une division euclidienne par une puissance de 2 et opère donc sur l'ensemble des entiers naturels.
Viens maintenant le problème des langages compilés et de la spécification qu'ils donnent à une telle primitive. Ils pourraient tout à fait faire un choix strict et défini en optant pour la vision modulaire à la X86 ou la vision entière à la ARM. La plupart on choisit d'utiliser pour chaque architecture la primitive correspondante du processeur et elle n'est donc spécifiée et définie que sur le domaine où elles coïncident, à savoir 0≤ a < 64. Si le programmeur veut une fonction plus fortement spécifiée, alors il n'a qu'à la coder lui-même.
Tu concluais ton commentaire réponse par : « c'est pour ça que j'adore l'Ada, vous l'aurez remarqué :) », je terminerai le mien par j'adore le lamba-calcul typé et rien de plus normal pour le mathématicien et logicien que je suis :) Le lamba-calcul typé (dont font partie les langages comme Haskell, OCaml ou Coq) a pour principe fondamental la correspondance preuve-programme : une programme est la preuve d'un théorème dont l'énoncé est le type ! \o/
Si l'on prend le langage qui a le système de type le plus sophistiqué (Coq), je te laisse deviner ce que fait une fonction dont le type est « pour tout (n: nat), il existe (p:nat) tel n ≤ p et p soit premier » si on lui passe un entier en entrée. En Coq, cela pourrait se définir ainsi :
Definitiongreater_prime(n:nat):={p:nat|n<=p/\primep}.Theoremma_fonctionn:greater_primen.Proof.(* la preuve *)Qed.
Pas besoin d'aller lire la doc pour savoir ce que fait la fonction, la lecture de son type suffit à cela. ;-)
Au final si j'étais un peu taquin, en se basant sur la popularité des langages de programmation je dirais qu'à l'heure actuelle la programmation consiste, la plupart du temps, dans l'art de faire des mathématiques comme un goret dans des langages atrophiés. En conséquence, la seule chose à faire si l'on veut savoir ce que fait une fonction, c'est d'aller lire la doc : on ne peut pas se fier uniquement à son type ni à ses attentes. Et le seul moyen de vérifier qu'elle se comporte exactement comme le spécifie la doc, c'est d'aller lire le code d'où la condition sine qua non que celui-ci soit publiquement accessible. Voilà une leçon que pourront retenir tes étudiants de cet exercice.
Comme tu enseignes les mathématiques, si le sujet t'intéresse il y a un dossier sympa sur le sujet dans la gazette des mathématiciens d'octobre 2014 : théories des types et mathématiques certifiées, et la théorie homotopique des types pousse encore plus loin la correspondance que j'ai signalée plus haut et fournit des fondements élégants à l'ensemble de l'édifice mathématique.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Du haut niveau pour gérer correctement du bas niveau
Posté par kantien . En réponse au journal Un décalage de 64 bits, ça vous inspire comment ?. Évalué à 7.
Je me permets de concentrer dans ce commentaire ma réponse à celui-ci ainsi qu'à cet autre commentaire, étant donné que tu y reprends les mêmes idées. Tu as été clair malgré l'heure tardive, j'espère pouvoir faire de même en cette heure plus matinale.
Il me semble que dans ton approche de la question, tu mélanges plusieurs problématiques. Dans l'exemple que tu donnes ici, tu montres surtout comment un système de type avancé (ici une forme restreinte de type dépendant) permet d'être plus précis sur la spécification d'un code et comment un compilateur peut en tirer partie pour générer un code optimisé (ici en supprimant un test de comparaison à l'exécution rendu inutile par ton type
amount). Cela rejoint un exemple que j'avais donné dans la dernière dépêche sur Haskell, où je montrais comment utiliser les GADT (types de données algébriques généralisés) pour exprimer la proposition : « tout arbre binaire parfait non vide a une racine ». Ce qui permettait de coder la fonction qui extrait cette racine sans que le code généré par le compilateur ait à vérifier à l'exécution que l'arbre était non vide (c'était déjà spécifié dans le type de la fonction).Revenons à présent au sujet précis du journal : le décalage à droite bit à bit. Dans un autre commentaire, tu précises à bon droit que l'arithmétique modulaire est la base de tous les processeurs courants et dans le cas présent on fait de l'arithmétique dans l'anneau
Z/nZavecn = 2^64. Se pose alors la question que doit faire cette fonction de décalage à droite ? et tu réponds toi même : « [elle] ne devrait répondre qu'au seul problème du quotient d'un entier machine entre 0 et 2n - 1 par une puissance positive quelconque de 2 ». Ce à quoi je te répondrai : l'architecture X86 fait cela en restant dans le cadre de l'arithmétique modulaire, et ne la mélange pas avec de l'arithmétique sur les entiers. En effet prenons le type de cette fonction :function my_shr (u : unsigned_64; a : natural) return unsigned_64. Elle prend en paramètre un entier non signé sur 64 bits, un entier naturel et renvoie un entier non signé sur 64 bits. Or pour opérer au sein de l'anneau sus-mentionné, elle doit donc associer un élément de cette anneau au paramètrea : natural, puis renvoyer ensuite le quotient d'une division euclidienne effectuée au sein de l'anneau. Les processeurs X86 on fait le choix de prendre l'élément2 ^ (a % 64), ce qui peut sembler assez « naturel » lorsque l'on pratique l'arithmétique modulaire. Exemple en OCaml sur mon X86 :En revanche, de ce que j'ai compris, l'architecture ARM ne voit pas cela du tout comme une opération d'arithmétique modulaire, mais semble considérer une telle donnée (un entier non signé sur 64 bit) comme un suite finie de
0et de1ou plutôt comme une suite stationnaire de valeur nulle à partir du rang64et si tu lui donne la suiteu(n)elle te renvoie la suiteu(n+a). Ce qui semble être le comportement que tu souhaiterais, mais ce n'est pas du tout le point de vue de l'arithmétique modulaire. Autrement dit, elle voit un entier de 64 bit comme un entier naturel compris entre0et2^64 - 1représenté en base 2, effectue une division euclidienne par une puissance de2et opère donc sur l'ensemble des entiers naturels.Viens maintenant le problème des langages compilés et de la spécification qu'ils donnent à une telle primitive. Ils pourraient tout à fait faire un choix strict et défini en optant pour la vision modulaire à la X86 ou la vision entière à la ARM. La plupart on choisit d'utiliser pour chaque architecture la primitive correspondante du processeur et elle n'est donc spécifiée et définie que sur le domaine où elles coïncident, à savoir
0≤ a < 64. Si le programmeur veut une fonction plus fortement spécifiée, alors il n'a qu'à la coder lui-même.Tu concluais ton commentaire réponse par : « c'est pour ça que j'adore l'Ada, vous l'aurez remarqué :) », je terminerai le mien par j'adore le lamba-calcul typé et rien de plus normal pour le mathématicien et logicien que je suis :) Le lamba-calcul typé (dont font partie les langages comme Haskell, OCaml ou Coq) a pour principe fondamental la correspondance preuve-programme : une programme est la preuve d'un théorème dont l'énoncé est le type ! \o/
Ce qui donne le tableau suivant :
Si l'on prend le langage qui a le système de type le plus sophistiqué (Coq), je te laisse deviner ce que fait une fonction dont le type est « pour tout (n: nat), il existe (p:nat) tel
n ≤ pet p soit premier » si on lui passe un entier en entrée. En Coq, cela pourrait se définir ainsi :Pas besoin d'aller lire la doc pour savoir ce que fait la fonction, la lecture de son type suffit à cela. ;-)
Au final si j'étais un peu taquin, en se basant sur la popularité des langages de programmation je dirais qu'à l'heure actuelle la programmation consiste, la plupart du temps, dans l'art de faire des mathématiques comme un goret dans des langages atrophiés. En conséquence, la seule chose à faire si l'on veut savoir ce que fait une fonction, c'est d'aller lire la doc : on ne peut pas se fier uniquement à son type ni à ses attentes. Et le seul moyen de vérifier qu'elle se comporte exactement comme le spécifie la doc, c'est d'aller lire le code d'où la condition sine qua non que celui-ci soit publiquement accessible. Voilà une leçon que pourront retenir tes étudiants de cet exercice.
Comme tu enseignes les mathématiques, si le sujet t'intéresse il y a un dossier sympa sur le sujet dans la gazette des mathématiciens d'octobre 2014 : théories des types et mathématiques certifiées, et la théorie homotopique des types pousse encore plus loin la correspondance que j'ai signalée plus haut et fournit des fondements élégants à l'ensemble de l'édifice mathématique.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.