Cela implique que les filtrages effectués dans le code sont vérifiés à la compilation, car le formalisme permet de s'assurer que les élements filtrés sont tous disjoint mais aussi que leur union soit égal à l'ensemble filtrés.
En OCaml, le filtrage est aussi vérifié à la compilation : le compilateur affiche un warning si un cas n'est pas traité (ie. si leur union est différente de l'ensemble filtré). En Haskell ce n'est pas le cas par défaut à ma connaissance (pas avec GHC en tout cas), mais le travail de Neil Mitchell sur Catch[0] permet de vérifier qu'il n'y a pas d'erreur de filtrage à l'exécution, c'est à dire qu'un chemin du code ne mène pas à un cas non traité dans un filtrage non exhaustif.
[^] # Re: Anubis et les "catégories bicartésiennes fermées"
Posté par pasSteve pasJobs . En réponse à la dépêche Sortie de la version 2.5 du langage Tom. Évalué à 4.
En OCaml, le filtrage est aussi vérifié à la compilation : le compilateur affiche un warning si un cas n'est pas traité (ie. si leur union est différente de l'ensemble filtré). En Haskell ce n'est pas le cas par défaut à ma connaissance (pas avec GHC en tout cas), mais le travail de Neil Mitchell sur Catch[0] permet de vérifier qu'il n'y a pas d'erreur de filtrage à l'exécution, c'est à dire qu'un chemin du code ne mène pas à un cas non traité dans un filtrage non exhaustif.
[0] : http://www-users.cs.york.ac.uk/~ndm/catch/