Oui, il existe des langages/techniques de modélisation/spécification largement utilisés pour Haskell. Ils ne sont pas visuels.
En Haskell, les types donnent un partiel spécification. Parfois, cette spécification détermine entièrement le sens/résultat tout en laissant plusieurs choix de mise en œuvre. Au-delà de Haskell, dans les langages avec des types dépendants, comme Agda et Coq (parmi d'autres), les types sont beaucoup plus souvent utiles en tant qu'outil de gestion de l'information. complet spécification.
Lorsque les types ne suffisent pas, ajoutez des spécifications formelles, qui prennent souvent une forme fonctionnelle simple. (D'où, je crois, les réponses que le langage de modélisation de choix pour Haskell est Haskell lui-même ou "math"). Dans une telle forme, vous donnez une définition fonctionnelle qui est optimisée pour la clarté et la simplicité et pas seulement pour l'efficacité. La définition peut même impliquer des opérations non calculables telles que l'égalité des fonctions sur des domaines infinis. Ensuite, étape par étape, vous transformez la spécification sous la forme d'un programme fonctionnel efficacement calculable. Chaque étape préserve la sémantique (dénotation), et ainsi la forme finale ("implémentation") est garantie d'être sémantiquement équivalente à la forme originale ("spécification"). Vous verrez que ce processus est désigné par différents noms, notamment "transformation de programme", "dérivation de programme" et "calcul de programme".
Les étapes d'une dérivation typique sont principalement des applications du "raisonnement équationnel", complétées par quelques applications de l'induction (et de la co-induction) mathématique. La possibilité d'effectuer un raisonnement aussi simple et utile a été l'une des principales motivations des langages de programmation fonctionnelle à l'origine, et ils doivent leur validité à la nature "dénotative" de la "programmation véritablement fonctionnelle". (Les termes "dénotatif" et "véritablement fonctionnel" sont tirés de l'article fondateur de Peter Landin, intitulé Les 700 prochains langages de programmation .) Ainsi, le cri de ralliement pour la programmation fonctionnelle pure était autrefois "bon pour le raisonnement équationnel", bien que je n'entende pas cette description aussi souvent ces jours-ci. En Haskell, le dénotatif correspond aux types autres que IO et les types qui s'appuient sur IO (par exemple STM ). Tandis que le rapport dénotatif/non- IO sont bons pour un raisonnement équationnel correct, le IO /Les types non dénotatifs sont conçus pour être mauvais pour le raisonnement équationnel incorrect.
Une version spécifique de la dérivation à partir de la spécification que j'utilise aussi souvent que possible dans mon travail en Haskell est ce que j'appelle les "morphismes de classe de type sémantique" (TCM). L'idée est de donner une sémantique/interprétation pour un type de données, puis d'utiliser le principe des TCM pour déterminer (souvent de manière unique) la signification de la plupart ou de toutes les fonctionnalités du type via les instances de classe de type. Par exemple, je dis que la signification d'une classe de type Image est une fonction de l'espace 2D. Le principe de la MTC me dit alors la signification de la Monoid , Functor , Applicative , Monad , Contrafunctor y Comonad comme correspondant à ces instances pour les fonctions. C'est un lot de fonctionnalités utiles sur des images aux spécifications très succinctes et convaincantes ! (La spécification est la fonction sémantique plus une liste de classes de types standard pour lesquelles le principe de MCT sémantique doit tenir). Et pourtant, j'ai une énorme liberté quant à la manière de représenter et le principe de la MCT sémantique élimine les fuites d'abstraction. Si vous êtes curieux de voir quelques exemples de ce principe en action, consultez l'article suivant Conception dénotationnelle avec morphismes de classe de type .
