Bonjour à tous!
Malgré la bizarrerie et une certaine abstraction du sujet considéré aujourd'hui - nous espérons qu'il pourra diversifier votre week-end. À la fin de l'article, nous plaçons trois liens de l'auteur, vous permettant de vous familiariser avec la saisie dépendante dans Idris, F * et JavaScript
Parfois, il semble que les langages de programmation n'aient pas beaucoup changé depuis les années 60. Quand ils me parlent de cela, je me souviens souvent du nombre d'outils et de fonctionnalités sympas que nous avons maintenant à notre disposition, et comment ils simplifient nos vies. Offhand: ce sont des débogueurs intégrés, des tests unitaires, des analyseurs statiques et des IDE sympas, ainsi que des tableaux typés et bien plus encore. Le développement des langues est un processus long et progressif, et il n'y a pas de telles «balles d'argent» avec lesquelles le développement des langues changerait une fois pour toutes.
Aujourd'hui, je veux vous parler d'une des dernières étapes de ce processus en cours. La technologie dont nous parlons est encore activement explorée, mais tout indique qu'elle prendra bientôt racine dans les langues dominantes. Et notre histoire commence par l'un des concepts les plus fondamentaux de l'informatique: les
types .
Monde des types
La dactylographie est l'une de ces choses qui sont tellement inséparables de notre pensée que nous ne pensons même pas au concept de types en tant que tels? Pourquoi 1 est-il un
int , mais si vous mettez simplement cette valeur entre guillemets - et qu'elle se transforme en
string ? Qu'est-ce qu'un «type» par essence? Comme c'est souvent le cas en programmation, la réponse dépend du libellé de la question.
Les types sont divers. Dans certains systèmes de types, il existe des frontières très claires entre les types et les valeurs. Ainsi, 3, 2 et 1 sont
integer valeurs
integer , mais l'
integer n'est pas une valeur. Cette construction est «intégrée» dans le langage et fondamentalement différente du sens. Mais, en fait, une telle différence n'est pas nécessaire et ne peut que nous limiter.
Si vous libérez les types et les transformez en une autre catégorie de valeurs, un certain nombre de possibilités incroyables s'ouvrent. Les valeurs peuvent être stockées, converties et transmises aux fonctions. Ainsi, il serait possible de faire une fonction qui prend un type en paramètre, en créant des fonctions généralisées: celles qui peuvent fonctionner avec de nombreux types sans surcharge. Vous pouvez avoir un tableau de valeurs d'un type donné, plutôt que de faire une arithmétique et une conversion de caractères de pointeurs étranges, comme vous devez le faire en C. Vous pouvez également collecter de nouveaux types pendant l'exécution du programme et fournir des fonctionnalités telles que la désérialisation JSON automatique. Mais, même si vous traitez les types comme des valeurs, vous ne pouvez toujours pas faire tout ce que les types peuvent faire avec des valeurs. Ainsi, en opérant avec des instances d'utilisateurs, vous pouvez, par exemple, comparer leurs noms, vérifier leur âge ou leur identifiant, etc.
if user.name == "Marin" && user.age < 65 { print("You can't retire yet!") }
Toutefois, lorsque vous essayez de faire de même avec le type d'
User , vous ne pouvez comparer que les noms de type et éventuellement les noms de propriété. Comme il s'agit d'un type et non d'une instance, vous ne pouvez pas vérifier les valeurs de ses propriétés.
if typeof(user) == User { print("Well, it's a user. That's all I know") }
Serait-ce cool si nous avions une fonction capable de recevoir uniquement une liste d'utilisateurs non vide? Ou une fonction qui n'accepterait une adresse e-mail que si elle est enregistrée au format correct? À ces fins, vous aurez besoin des types «tableau non vide» ou «adresse e-mail». Dans ce cas, il s'agit d'un type dépendant de la valeur, c'est-à-dire sur le
type dépendant . Dans les langues traditionnelles, ce n'est pas possible.
Pour que les types puissent être utilisés, le compilateur doit les vérifier. Si vous prétendez que la variable contient un entier, il serait préférable qu'il n'y ait pas de
string , sinon le compilateur jurera. En principe, c'est bien, car cela ne nous permet pas de courtiser. La vérification des types est assez simple: si une fonction retourne un
integer et que nous essayons d'y retourner
"Marin" , alors c'est une erreur.
Cependant, avec les types dépendants, les choses deviennent plus compliquées. Le problème est quand exactement le compilateur vérifie les types. Comment peut-il s'assurer qu'il y a exactement trois valeurs dans le tableau, si le programme n'est pas encore en cours d'exécution? Comment s'assurer qu'un entier est supérieur à 3, s'il n'est même pas encore attribué? Il y a de la
magie là-
dedans ... ou, en d'autres termes, des
mathématiques . S'il peut être prouvé mathématiquement que l'ensemble de nombres est toujours supérieur à 3, alors le compilateur peut le vérifier.
Les maths en studio!
L'induction mathématique est utilisée pour formuler des preuves. L'induction nous permet de confirmer sans condition la véracité d'une déclaration. Par exemple, nous voulons prouver que la formule mathématique suivante est valable pour tout nombre positif:
1 + 2 + 3 + ... + x = x * (x + 1) / 2
Il existe un nombre infini de x possibles, il nous faudrait donc très longtemps pour vérifier tous les nombres manuellement. Heureusement, ce n'est pas nécessaire. Nous devons simplement prouver deux choses:
- Cette déclaration est observée pour le premier jour. (Habituellement, c'est 0 ou 1)
- Si cette affirmation est vraie pour le nombre
n , alors elle sera vraie pour le nombre suivant n + 1
Puisque l'énoncé est observé à la fois pour le premier nombre et pour tous les nombres suivants, nous savons qu'il est vrai pour tous les nombres possibles.
Pour prouver que ce n'est pas difficile:
1 = 1 * (1 + 1) / 2 1 = 1
Maintenant, nous devons également prouver que la déclaration est valable pour tous les autres nombres. Pour ce faire, supposons que cela fonctionne pour un certain nombre n, puis assurez-vous qu'il fonctionne également pour n + 1.
En supposant que l'expression suivante est vraie:
1 + 2 + 3 + ... + n = n * (n + 1) / 2
Découvrez-le pour
n + 1 :
(1 + 2 + 3 + ... + n) + (n + 1) = (n + 1) * ((n + 1) + 1) / 2
Ainsi, nous pouvons remplacer
"(1 + 2 + 3 + ... + n)" égalité ci
"(1 + 2 + 3 + ... + n)" dessus:
(n * (n + 1) / 2) + (n + 1) = (n + 1) * ((n + 2) / 2)
et simplifier
(n + 1) * (n/2 + 1) = (n + 1) * (n/2 + 1)
Puisque les deux parties de l'expression sont égales, nous nous sommes assurés que cette affirmation est vraie. C'est l'une des façons dont vous pouvez vérifier la véracité des déclarations sans calculer manuellement chaque cas, et c'est sur la base de ce principe que les types dépendants fonctionnent. Vous écrivez une déclaration mathématique pour vous assurer que la thèse de type est vraie.
La beauté de cette approche réside dans le fait que toute preuve mathématique peut être délivrée sous la forme d'un programme informatique - et c'est ce dont nous avons besoin!
Retour à la programmation
Nous avons donc constaté que certaines choses peuvent être prouvées en premier, puis passer à des valeurs spécifiques. Pour ce faire dans un langage de programmation, vous avez besoin d'un moyen d'exprimer ces instructions dans du code qui sera écrit dans le système de types lui-même, c'est-à-dire que le système de types doit être amélioré.
Prenons un exemple. Ici, nous avons une fonction d'ajout qui prend deux tableaux et les combine. En règle générale, la signature d'une telle fonction ressemblera à ceci:
append: (arr1: Array, arr2: Array) -> Array
Cependant, juste en regardant la signature, nous ne pouvons pas être sûrs de la bonne mise en œuvre. Le fait que la fonction renvoie un tableau ne signifie pas qu'elle a fait quelque chose. Une façon de vérifier le résultat consiste à s'assurer que la longueur du tableau résultant est égale à la somme des longueurs des tableaux de paramètres.
newArray = append([1], [2, 3]) assert(length(newArray) == 3)
Mais pourquoi vérifier cela au moment de l'exécution si vous pouvez créer une contrainte qui sera vérifiée au moment de la compilation:
append: (arr1: Array, arr2: Array) -> newArray: Array where length(newArray) == length(arr1) + length(arr2)
Nous déclarons que
append est une fonction qui prend deux arguments
Array et renvoie un nouvel argument
Array , que nous avons appelé
newArray . Seulement cette fois, nous ajoutons une mise en garde que la longueur du nouveau tableau doit être égale à la somme des longueurs de tous les arguments de la fonction. L'instruction que nous avions ci-dessus à l'exécution est convertie en type au moment de la compilation.
Le code ci-dessus fait référence au monde des types, pas des valeurs, c'est-à-dire que le signe
== indique une comparaison de la
length type retournée et non de sa valeur. Pour qu'un tel mécanisme fonctionne, la longueur de type retournée doit nous donner des informations sur le nombre réel.
Pour garantir le fonctionnement d'un tel mécanisme, vous devez vous assurer que chaque numéro est d'un type distinct. Un type ne peut contenir qu'une seule valeur: 1. Il en va de même pour Deux, Trois et tous les autres nombres. Naturellement, un tel travail est très fatigant, mais c'est pour un tel travail que nous avons une programmation. Vous pouvez écrire un compilateur qui le fera pour nous.
Cela fait, vous pouvez créer des types distincts pour les tableaux contenant 1, 2, 3 et un nombre différent d'éléments.
ArrayOfOne ,
ArrayOfTwo , etc.
Ainsi, vous pouvez définir la fonction de longueur, qui prendra l'un des types de tableau ci-dessus et aura un type de retour dépendant de
One pour
ArrayOfOne ,
Two pour
ArrayOfTwo , etc. pour chaque numéro.
Maintenant que nous avons un type distinct pour toute longueur spécifique du tableau, nous pouvons vérifier (au moment de la compilation) que les deux tableaux sont de longueur égale. Pour ce faire, comparez leurs types. Et comme les types ont les mêmes valeurs que les autres, vous pouvez leur affecter des opérations. Vous pouvez déterminer l'ajout de deux types spécifiques en spécifiant que la somme de
ArrayOfOne et
ArrayOfTwo est égale à
ArrayOfThree .
C'est toute l'information dont le compilateur a besoin pour s'assurer que le code que vous avez écrit est correct.
Supposons que nous voulons créer une variable de type
ArrayOfThree :
result: ArrayOfThree = append([1], [2, 3])
Le compilateur peut déterminer que [1] n'a qu'une seule valeur, vous pouvez donc affecter le type
ArrayOfOne . Il peut également affecter
ArrayOfTwo à [2, 3].
Le compilateur sait que le type de résultat doit être égal à la somme des types des premier et deuxième arguments. Il sait également que ArrayOfOne + ArrayOfTwo est égal à ArrayOfThree, c'est-à-dire qu'il sait que l'expression entière sur le côté droit de l'identité est de type ArrayOfThree. Il correspond à l'expression de gauche et le compilateur est satisfait.
Si nous écrivions ce qui suit:
result: ArrayOfTwo = append([1], [2, 3])
alors le compilateur serait complètement insatisfait, car il saurait que le type est incorrect.
La saisie dépendante est très cool
Dans ce cas, un grand nombre de bogues est tout simplement impossible à autoriser. Avec le typage dépendant, les erreurs par unité, les accès aux index de tableau inexistants, les exceptions de pointeur nul, les boucles infinies et le code cassé peuvent être évités.
En utilisant des types dépendants, vous pouvez exprimer presque tout. La fonction factorielle n'acceptera que les nombres naturels, la fonction de
login n'acceptera pas les lignes vides, la fonction
removeLast n'acceptera que les tableaux non vides. De plus, tout cela est vérifié avant de démarrer le programme.
Le problème avec les vérifications d'exécution est qu'elles échouent si le programme est déjà en cours d'exécution. Ceci est normal si le programme est exécuté uniquement par vous, mais pas par l'utilisateur. Les types dépendants vous permettent de prendre ces vérifications au niveau des types, de sorte qu'une défaillance de ce type pendant l'exécution du programme devient impossible.
Je pense que la dactylographie dépendante est l'avenir des langages de programmation traditionnels, et j'ai hâte de l'attendre!
→
Idris→
F *→
Ajout de types dépendants à JavaScript