Posté par neil .
En réponse au journal Ada, langage et ressources.
Évalué à 8.
Dernière modification le 24 juin 2013 à 22:39.
C’était principalement de l’humour pour dire qu’il y a toujours des systèmes de type plus puissant, c’est à dire permettant de détailler encore plus finement ce que fait un élément d’un programme (une fonction par exemple). L’exemple de l’OP avec un alias de type pour les heures par exemple, permet de définir des fonctions typées comme :
-- Date de Pâques pour une année donnée
easter : Int -> Day_of_year
et le compilateur va se charger de vérifier qu’on ne retourne pas une erreur (un entier négatif, ou supérieur à 366).
En Haskell et OCaml, par exemple, il y a tout un tas d’autres apports du système de type. Par exemple, avec les GADTs, on peut vérifier à la compilation que tous les arbres binaires que l’on va construire sont bien balancés, ou qu’une liste passée en paramètre est toujours non-vide. Ça permet d’avoir une sorte de pattern matching mais à la compilation plutôt qu’à l’exécution. On peut aussi utiliser le système de type pour faire des calculs à la compilation (un peu comme le template meta-programming en C++, mais de façon propre :p).
Les GADTs viennent des systèmes de types dépendants, dans lesquels on peut par exemple typer le fait qu’un programme prenne en entrée une liste de n éléments, et sorte une liste de (n+1) éléments :
-- Ajoute un élément à une liste de taille n contenant des a
addElem : List n a -> L (n+1) a
Et c’est le système de types du compilateur qui va se charger de vérifier ça à la compilation (en fait écrire un programme bien typé est la même chose qu’écrire une preuve, que le compilateur va vérifier). Les types dépendants sont classiquement utilisés dans les systèmes de vérification de programmes comme Coq ou Agda, mais les fonctionnalités commencent à arriver dans OCaml et Haskell. Il y a aussi des expériences de langages généralistes entièrement dépendants tels que Idris ou F*.
Pour les systèmes de types homotopes, il va encore falloir attendre un moment avant d’avoir des jolies applications. En gros, en plus d’unifier de nouvelles branches des mathématiques, ça permet d’avoir des types beaucoup plus jolis, ou de transférer une preuve sur un algorithme naïf, à une preuve sur un algorithme optimisé.
[^] # Re: langage fonctionnel
Posté par neil . En réponse au journal Ada, langage et ressources. Évalué à 8. Dernière modification le 24 juin 2013 à 22:39.
C’était principalement de l’humour pour dire qu’il y a toujours des systèmes de type plus puissant, c’est à dire permettant de détailler encore plus finement ce que fait un élément d’un programme (une fonction par exemple). L’exemple de l’OP avec un alias de type pour les heures par exemple, permet de définir des fonctions typées comme :
et le compilateur va se charger de vérifier qu’on ne retourne pas une erreur (un entier négatif, ou supérieur à 366).
En Haskell et OCaml, par exemple, il y a tout un tas d’autres apports du système de type. Par exemple, avec les GADTs, on peut vérifier à la compilation que tous les arbres binaires que l’on va construire sont bien balancés, ou qu’une liste passée en paramètre est toujours non-vide. Ça permet d’avoir une sorte de pattern matching mais à la compilation plutôt qu’à l’exécution. On peut aussi utiliser le système de type pour faire des calculs à la compilation (un peu comme le template meta-programming en C++, mais de façon propre :p).
Les GADTs viennent des systèmes de types dépendants, dans lesquels on peut par exemple typer le fait qu’un programme prenne en entrée une liste de n éléments, et sorte une liste de (n+1) éléments :
Et c’est le système de types du compilateur qui va se charger de vérifier ça à la compilation (en fait écrire un programme bien typé est la même chose qu’écrire une preuve, que le compilateur va vérifier). Les types dépendants sont classiquement utilisés dans les systèmes de vérification de programmes comme Coq ou Agda, mais les fonctionnalités commencent à arriver dans OCaml et Haskell. Il y a aussi des expériences de langages généralistes entièrement dépendants tels que Idris ou F*.
Pour les systèmes de types homotopes, il va encore falloir attendre un moment avant d’avoir des jolies applications. En gros, en plus d’unifier de nouvelles branches des mathématiques, ça permet d’avoir des types beaucoup plus jolis, ou de transférer une preuve sur un algorithme naïf, à une preuve sur un algorithme optimisé.