Y a-t-il une raison d'avoir un type de fond dans un langage de programmation?

Un type de fond est une construction apparaissant principalement dans la théorie des types mathématiques. On l'appelle aussi le type vide. C'est un type qui n'a pas de valeur, mais qui est un sous-type de tous les types.

Si le type de retour d'une fonction est le type du bas, cela signifie qu'il ne retourne pas. Période. Peut-être que ça tourne en boucle pour toujours, ou peut-être une exception.

Quel est l'intérêt d'avoir ce type étrange dans un langage de programmation? Ce n'est pas si commun, mais il est présent dans certains, tels que Scala et Lisp.

Je prendrai un exemple simple: C ++ vs Rust.

Voici une fonction utilisée pour lever une exception en C ++ 11:

[[noreturn]] void ThrowException(char const* message,
                                 char const* file,
                                 int line,
                                 char const* function);

Et voici l'équivalent en rouille:

fn formatted_panic(message: &str, file: &str, line: isize, function: &str) -> !;

Sur une question purement syntaxique, la construction de Rust est plus sensible. Notez que la construction C ++ spécifie un type de retour, même si elle spécifie également qu'il ne sera pas renvoyé. C'est un peu bizarre.

Sur une note standard, la syntaxe C ++ n’apparaissait qu’avec C ++ 11 (c’était un clou au dessus), mais divers compilateurs fournissaient diverses extensions depuis un certain temps, de sorte que des outils d’analyse tiers devaient être programmés pour reconnaître les différentes manières. cet attribut pourrait être écrit. L’avoir normalisé est évidemment nettement supérieur.

Maintenant, comme pour le bénéfice?

Le fait qu'une fonction ne retourne pas peut être utile pour:

• optimisation: on peut supprimer n'importe quel code après celui-ci (il ne reviendra pas), il n'est pas nécessaire de sauvegarder les registres (car il ne sera pas nécessaire de les restaurer), ...
• analyse statique: élimine un certain nombre de chemins d'exécution potentiels
• maintenabilité: (voir l'analyse statique, mais par l'homme)

La réponse de Karl est bonne. Voici une utilisation supplémentaire que personne, à mon avis, n’a mentionnée. Le type de

if E then A else B

devrait être un type qui inclut toutes les valeurs du type Aet toutes les valeurs du type B. Si le type Best Nothing, alors le type de l' ifexpression peut être le type de A. Je déclare souvent une routine

def unreachable( s:String ) : Nothing = throw new AssertionError("Unreachable "+s) 

dire que le code ne devrait pas être atteint. Comme son type est Nothing, unreachable(s)peut maintenant être utilisé dans n’importe quel ifou (plus souvent) switchsans affecter le type de résultat. Par exemple

 val colour : Colour := switch state of
         BLACK_TO_MOVE: BLACK
         WHITE_TO_MOVE: WHITE
         default: unreachable("Bad state")

Scala a un tel type rien.

Un autre cas d'utilisation Nothing(comme mentionné dans la réponse de Karl) est List [Nothing] est le type de listes dont chacun des membres a le type Nothing. Cela peut donc être le type de la liste vide.

La propriété de clé Nothingqui fait fonctionner ces cas d'utilisation n'est pas qu'elle n'a pas de valeur - bien que dans Scala, par exemple, elle n'a pas de valeur - c'est qu'il s'agit d'un sous-type de tous les autres types.

Supposons que vous ayez une langue où chaque type contient la même valeur - appelons-le (). Dans un tel langage, le type d'unité, qui a ()pour seule valeur, pourrait être un sous-type de chaque type. Cela n'en fait pas un type de fond au sens où l'entend l'OP; le PO était clair qu'un type de fond ne contient aucune valeur. Cependant, comme il s'agit d'un type qui est un sous-type de chaque type, il peut jouer à peu près le même rôle qu'un type inférieur.

Haskell fait les choses un peu différemment. En Haskell, une expression qui ne produit jamais de valeur peut avoir le schéma de type forall a.a. Une instance de ce schéma de type s'unira avec tout autre type, de sorte qu'elle agit effectivement comme un type de fond, même si Haskell (standard) ne possède aucune notion de sous-typage. Par exemple, la errorfonction du prélude standard a un schéma de types forall a. [Char] -> a. Donc tu peux écrire

if E then A else error ""

et le type de l'expression sera le même que le type de A, pour toute expression A.

La liste vide dans Haskell a le schéma de type forall a. [a]. Si Aest une expression dont le type est un type de liste, alors

if E then A else []

est une expression du même type que A.

Les types forment un monoïde de deux manières, formant ensemble un semiring . C'est ce qu'on appelle les types de données algébriques . Pour les types finis, ce semiring est directement lié au semiring de nombres naturels (y compris zéro), ce qui signifie que vous comptez le nombre de valeurs possibles du type (à l’exclusion des «valeurs non finales»).

• Le type du bas (je l'appellerai Vacuous) a une valeur nulle ^† .
• Le type d'unité a une valeur. J'appellerai à la fois le type et sa valeur unique ().
• La composition (que la plupart des langages de programmation prennent en charge assez directement, via des enregistrements / structures / classes avec des champs publics) est une opération produit . Par exemple, (Bool, Bool)a quatre valeurs possibles, à savoir (False,False), (False,True), (True,False)et (True,True).
  Le type d'unité est l'élément d'identité de l'opération de composition. Par exemple, ((), False)et ((), True)sont les seules valeurs de type ((), Bool), ce type est donc isomorphe à Boollui-même.
• Les types alternatifs sont quelque peu négligés dans la plupart des langues (les langues OO supportent en quelque sorte leur héritage), mais ils ne sont pas moins utiles. Une alternative entre deux types Aet a Bfondamentalement toutes les valeurs de A, plus toutes les valeurs de B, donc le type de somme . Par exemple, Either () Boola trois valeurs, je les appellerai Left (), Right Falseet Right True.
  Le type du bas est l'élément d'identité de la somme: Either Vacuous An'a que des valeurs de la forme Right a, car cela Left ...n'a pas de sens ( Vacuousn'a pas de valeurs).

Ce qui est intéressant à propos de ces monoïdes, c’est que, lorsque vous introduisez des fonctions dans votre langue, la catégorie de ces types avec les fonctions de morphismes est une catégorie monoïdale . Cela vous permet entre autres de définir des foncteurs et des monades applicatifs , ce qui s'avère être une excellente abstraction pour les calculs généraux (impliquant éventuellement des effets secondaires, etc.) dans des termes autrement purement fonctionnels.

Maintenant, en fait, vous pouvez aller assez loin en vous inquiétant d'un seul côté de la question (le monoïde de composition), vous n'avez donc pas vraiment besoin du type de fond explicitement. Par exemple, même Haskell n’avait pas pendant longtemps un type de fond standard. Maintenant, ça s'appelle Void.

Mais si vous considérez la situation dans son ensemble, en tant que catégorie fermée bicartesienne , le système de typage est en réalité équivalent au calcul lambda complet. Vous disposez donc d’une abstraction parfaite pour tout ce qui est possible dans un langage complet de Turing. Idéal pour les langues embarquées spécifiques à un domaine. Par exemple, il existe un projet sur le codage direct des circuits électroniques de cette manière .

Bien sûr, vous pouvez bien dire que tout cela est un non-sens général des théoriciens . Vous n'avez pas besoin de connaître la théorie des catégories pour être un bon programmeur, mais lorsque vous le faites, cela vous donne des moyens puissants et ridiculement généraux de raisonner sur le code et de prouver les invariants.

^† _{mb21 me rappelle de noter que cela ne doit pas être confondu avec les valeurs inférieures . Dans des langages paresseux comme Haskell, chaque type contient une «valeur» inférieure, notée ⊥. Ce n'est pas quelque chose de concret que vous pourriez explicitement transmettre, mais plutôt ce qui est «retourné», par exemple, lorsqu'une fonction est en boucle pour toujours. Même le Voidtype de Haskell "contient" la valeur inférieure, donc le nom. Dans cette optique, le type de fond de Haskell a vraiment une valeur et son type d'unité a deux valeurs, mais dans les discussions sur la théorie des catégories, ceci est généralement ignoré.}

Peut-être que ça tourne en boucle pour toujours, ou peut-être une exception.

Cela semble être un type utile à avoir dans ces situations, aussi rares soient-elles.

De même, même si Nothing(le nom de Scala pour le type du bas) ne peut avoir aucune valeur, il List[Nothing]n’a pas cette restriction, ce qui le rend utile comme type de liste vide. La plupart des langues contournent cela en faisant d'une liste vide de chaînes un type différent de celui d'une liste vide d'entiers, ce qui a du sens, mais rend une liste vide plus verbeuse à écrire, ce qui est un gros inconvénient dans un langage orienté liste.

Il est utile pour une analyse statique de documenter le fait qu’un chemin de code particulier n’est pas accessible. Par exemple, si vous écrivez ce qui suit en C #:

int F(int arg) {
 if (arg != 0)
  return arg + 1; //some computation
 else
  Assert(false); //this throws but the compiler does not know that
}
void Assert(bool cond) { if (!cond) throw ...; }

Le compilateur se plaindra de Fne rien renvoyer dans au moins un chemin de code. Si Assertdevaient être marqués comme non-retour, le compilateur n'aurait pas besoin d'avertir.

Dans certaines langues, nulla le type du bas, car le sous-type de tous les types définit bien le langage utilisé par null (malgré la légère contradiction entre nullêtre lui-même et une fonction qui se retourne, en évitant les arguments usuels sur la raison de l’inexistence de pourquoi bot).

Il peut également être utilisé comme une fourre-tout dans les types de fonctions ( any -> bot) pour gérer une distribution qui a mal tourné.

Et certaines langues vous permettent de résoudre botle problème en tant qu’erreur, ce qui peut être utilisé pour fournir des erreurs de compilation personnalisées.

Oui, c'est un type très utile. Bien que son rôle soit essentiellement interne au système de types, il existe des cas où le type de fond apparaît ouvertement.

Considérons un langage à typage statique dans lequel les conditions sont des expressions (la construction if-then-else fait donc double emploi en tant qu'opérateur ternaire de C et de ses amis, et il pourrait y avoir une déclaration de cas similaire à plusieurs entrées). Les langages de programmation fonctionnels ont cela, mais cela se produit également dans certains langages impératifs (depuis ALGOL 60). Ensuite, toutes les expressions de branche doivent finalement produire le type de l'expression conditionnelle entière. On pourrait simplement exiger que leurs types soient égaux (et je pense que c'est le cas de l'opérateur ternaire en C), mais cela est excessivement restrictif, en particulier lorsque le conditionnel peut également être utilisé en tant qu'instruction conditionnelle (ne renvoyant aucune valeur utile). En général, on veut que chaque expression de branche soit (implicitement) convertible à un type commun qui sera le type de l'expression complète (éventuellement avec des restrictions plus ou moins compliquées pour permettre à ce type commun d'être effectivement trouvé par le compliant, voir C ++, mais je n'entrerai pas dans ces détails ici).

Il existe deux types de situations où un type général de conversion permettra la flexibilité nécessaire de telles expressions conditionnelles. On est déjà mentionné, où le type de résultat est le type d'unitévoid; c'est naturellement un super-type de tous les autres types, et permettre à n'importe quel type d'y être converti (de manière triviale) permet d'utiliser l'expression conditionnelle en tant qu'instruction conditionnelle. L'autre concerne les cas où l'expression renvoie une valeur utile mais où une ou plusieurs branches sont incapables d'en produire une. Ils lèveront généralement une exception ou impliqueront un saut, et leur demander de produire (également) une valeur du type de l'expression entière (à partir d'un point inaccessible) serait alors inutile. C'est ce genre de situation qui peut être gérée avec élégance en donnant des clauses d'exception, des sauts et des appels qui auront un tel effet, le type du bas, le type qui peut être (trivialement) converti en un autre type.

Je suggérerais d'écrire un type de fond *qui suggère sa convertibilité en type arbitraire. Il peut servir d’autres objectifs utiles en interne, par exemple, lorsque vous essayez de déduire un type de résultat pour une fonction récursive qui n’en déclare pas, le type inférenceur peut affecter le type *à n’importe quel appel récursif pour éviter une situation poule-œuf; le type réel sera déterminé par des branches non-récursives, et les branches récursives seront converties au type commun des branches non-récursives. S'il n'y a aucune branche non récursive, le type restera *et indiquera correctement que la fonction n'a aucun moyen de revenir de la récursion. Autre que cela et comme type de résultat des fonctions de levée d’exception, on peut utiliser*en tant que type de composant de séquences de longueur 0, par exemple de la liste vide; de nouveau si jamais un élément est sélectionné dans une expression de type [*](liste nécessairement vide), le type résultant *indiquera correctement qu'il ne peut jamais être retourné sans erreur.

Dans certaines langues, vous pouvez annoter une fonction pour indiquer à la fois au compilateur et aux développeurs qu'un appel à cette fonction ne va pas être renvoyé (et si la fonction est écrite de manière à pouvoir être renvoyée, le compilateur ne l'autorisera pas. ). C'est une chose utile à savoir, mais à la fin, vous pouvez appeler une fonction comme celle-là comme une autre. Le compilateur peut utiliser les informations pour l'optimisation, donner des avertissements sur le code mort, etc. Donc, il n'y a pas de raison très convaincante d'avoir ce type, mais pas de raison très convaincante de l'éviter non plus.

Dans de nombreuses langues, une fonction peut retourner "void". Ce que cela signifie exactement dépend de la langue. En C, cela signifie que la fonction ne renvoie rien. En Swift, cela signifie que la fonction retourne un objet avec une seule valeur possible, et comme il n’existe qu’une seule valeur possible, cette valeur ne prend aucun bit et ne nécessite aucun code. Dans les deux cas, ce n'est pas la même chose que "bas".

"bottom" serait un type sans valeur possible. Cela ne peut jamais exister. Si une fonction retourne "bottom", elle ne peut pas réellement retourner car il n'y a pas de valeur de type "bottom" qu'elle pourrait renvoyer.

Si un concepteur de langage en a envie, il n’ya aucune raison de ne pas avoir ce type. L'implémentation n'est pas difficile (vous pouvez l'implémenter exactement comme une fonction retournant vide et marquée "ne retourne pas"). Vous ne pouvez pas mélanger des pointeurs vers des fonctions renvoyant bottom avec des pointeurs vers des fonctions renvoyant void, car ils ne sont pas du même type).