Je sais que Haskell a déjà la possibilité de paramétrer un type sur un autre type (similaire à la programmation de modèles en C ++), mais je me demande si Haskell peut également paramétrer un type sur des valeurs - s'il prend en charge les types dépendants. Avec les types dépendants, vous pouvez avoir un type paramétré sur des entiers, par exemple des vecteurs de taille n, des matrices de taille n × m, etc.
Sinon, pourquoi pas? Et y a-t-il une possibilité qu'il soit soutenu à l'avenir?
Haskell n'a pas tout à fait les types dépendants, bien qu'il puisse être très proche avec des extensions comme DataKindset TypeFamilies. Pour le moment, le problème, c'est que Haskell au niveau de la valeur a des fonds explicites, mais pas au niveau du type Haskell.
Cela ne vous empêche pas de paramétrer des types sur d'autres types, y compris le DataKind-lifting de valeurs . À partir de GHC 7.6, et avec DataKindsactivé, vous pouvez utiliser des éléments naturels et des chaînes au niveau du type, ainsi que des tuples au niveau du type, des listes au niveau du type et les élévations au niveau du type de tout élément (de type non supérieur, non généralisé) , non contraints) des types de données algébriques, qui est similaire (mais beaucoup plus général que) à la capacité de C ++ à utiliser des entiers dans les modèles.
Pour développer un peu ce que la flamme de Ptharien a bien expliqué sur l'état actuel - et GHC Haskell semble aller plus loin dans la direction des types dépendants (tout en préservant la séparation de phases) avec chaque version.
Ainsi, par exemple, lors de l'ICFP 2013 de septembre, un document sur la prochaine phase de ce processus devrait être présenté, "Vers un Haskell typé de manière dépendante: System FC avec une égalité genre" , sur la réduction des types et des niveaux. Comme cela a été annoncé il y a environ 3 ans .
Et il mentionne même la prochaine étape: "Nous sommes également conscients que la dissertation à venir d'Adam Gundry inclura des types Π dans une version de System FC et nous voudrons également rendre cette fonctionnalité disponible dans la langue source. (Communication personnelle)"
la source
Haskell a traditionnellement essayé de le simuler, mais le résultat final est un système de type beaucoup plus grand et apparemment répétitif. Mais cela pourrait bientôt changer! Voir:
la source