https://nokomprendo.gitlab.io/posts/tuto_fonctionnel_53/2021-02-08-fr-README.html

Le 23 septembre 1999, la sonde Mars Climate Orbiter a été perdue. La cause de cet échec est l’utilisation d’unités de mesure différentes entre deux logiciels de la sonde. D’une façon plus générale, les types de base des langages de programmation portent assez peu d’information. Il est donc facile de confondre, par exemple, des Newton et des Livre-force si on les représente tous les deux par des Double.

Haskell possède un système de types évolué, qui permet de programmer “au niveau des types” (type-level). Ainsi, on profite automatiquement des vérifications du compilateur, ce qui évite de nombreuses erreurs potentielles, comme par exemple mélanger des unités de mesure.

Cet article présente quelques fonctionnalités de programmation type-level, comme les types fantômes et les datakinds, à partir d’une problématique initiale.