Type vide
Le type vide est en théorie des types un type qui ne comporte pas de valeurs. On l'abrège communément par bot (de bottom type), le symbole ( ⊥ {\displaystyle \bot } ) ou par l'approximation ASCII _|_. On l'appelle aussi parfois type zéro. Il ne faut pas le confondre avec le type top ou le type unité. Le type top comprend toutes les valeurs d'un système. Le type unité a une seule valeur. On utilise souvent le type vide dans les cas suivants : Pour signifier le faux. Il peut être employé pour définir la négation et exprimer l'axiome ex falso sequitur quodlibet : Pour toute proposition P {\displaystyle P} : ⊥ → P {\displaystyle \bot \to P} . Hormis en logique minimale que rejette cet axiome, le type vide désigne donc par voie de conséquence, l'absurdité, l'état d'incohérence du système. Pour signaler qu'une fonction ou un calcul diverge ; en d'autres termes, il ne retourne pas de résultat à l'appelant. Cela ne signifie pas nécessairement que le programme ne se termine pas ; une fonction peut terminer sans retourner à son appelant, ou sortir par un moyen autre qu'un retour normal, par exemple via une continuation. Pour indiquer une erreur ; cela arrive principalement dans des langages théoriques dans lesquels les distinctions entre les erreurs ne sont pas importantes. Les langages de programmation pratiques utilisent une gestion d'exceptions à la place.
Le type vide est en théorie des types un type qui ne comporte pas de valeurs.
On l'abrège communément par bot (de bottom type), le symbole () ou par l'approximation ASCII _|_. On l'appelle aussi parfois type zéro. Il ne faut pas le confondre avec le type top ou le type unité. Le type top comprend toutes les valeurs d'un système. Le type unité a une seule valeur.
On utilise souvent le type vide dans les cas suivants :
- Pour signifier le faux. Il peut être employé pour définir la négation et exprimer l'axiome ex falso sequitur quodlibet : Pour toute proposition : . Hormis en logique minimale que rejette cet axiome, le type vide désigne donc par voie de conséquence, l'absurdité, l'état d'incohérence du système.
- Pour signaler qu'une fonction ou un calcul diverge ; en d'autres termes, il ne retourne pas de résultat à l'appelant. Cela ne signifie pas nécessairement que le programme ne se termine pas ; une fonction peut terminer sans retourner à son appelant, ou sortir par un moyen autre qu'un retour normal, par exemple via une continuation.
- Pour indiquer une erreur ; cela arrive principalement dans des langages théoriques dans lesquels les distinctions entre les erreurs ne sont pas importantes. Les langages de programmation pratiques utilisent une gestion d'exceptions à la place.
Exemples d'utilisation
[modifier | modifier le code]Rocq
[modifier | modifier le code]Le logiciel Rocq définit le type vide dans sa librairie standard par :
Inductive False : Prop :=.
Par opposition, le type unité est
Inductive True : Prop :=
I : True.
Sans entrer dans une description du langage, on voit que I : True est un (le) constructeur pour le type True. A contrario, l'absence de constructeur pour False interdit l'instanciation, autrement dit, on ne peut pas construire un objet de type False ; ce qui est heureux car, selon la correspondance de Curry-Howard, un objet de ce type serait assimilable à une preuve de l'incohérence de la logique.
La définition de False génère automatique l'axiome ex falso sequitur quodlibet :
False_ind
: forall P : Prop, False -> P
La négation est simplement définie par :
Definition not (A:Prop) := A -> False.
Haskell
[modifier | modifier le code]En Haskell, le mot clé undefined représente un calcul dont le résultat a un type vide. Tenter d'évaluer undefined pendant l'exécution arrête le programme.
Articles connexes
[modifier | modifier le code]Source
[modifier | modifier le code]- (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Bottom_type » (voir la liste des auteurs).
Liens externes
[modifier | modifier le code]- (en) Types and Programming Languages par Benjamin Pierce (MIT Press 2002) [1]
