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

49

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.

GregRos
la source
2
@SargeBorsch: êtes-vous sûr de cela? Bien sûr, on ne peut pas définir explicitement une voiddonnée en C ...
Basile Starynkevitch
3
@BasileStarynkevitch, il n'y a pas de valeur de type voidet le type d'unité ne doit avoir qu'une seule valeur. En outre, comme vous l'avez fait remarquer, vous ne pouvez même pas déclarer une valeur de type void, ce qui signifie que ce n'est même pas un type, mais un cas particulier dans la langue.
Sarge Borsch
2
Oui, le C est bizarre à cet égard, en particulier dans la façon dont les types de pointeur et de pointeur de fonction sont écrits. Mais voiden Java, c'est presque pareil: pas vraiment un type et on ne peut pas avoir de valeurs.
Sarge Borsch
3
Dans la sémantique des langages avec un type de fond, le type de fond n'est pas considéré comme n'ayant pas de valeur, mais plutôt une valeur, la valeur du bas, représentant un calcul qui ne se termine jamais (normalement). Comme la valeur inférieure est une valeur de chaque type, le type inférieur peut être un sous-type de chaque type.
Theodore Norvell
4
@BasileStarynkevitch Common Lisp a le type nil qui n'a pas de valeur. Il a également le type null qui n'a qu'une seule valeur, le symbole nil(aka, ()), qui est un type d'unité.
Joshua Taylor

Réponses:

33

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)
Matthieu M.
la source
6
voiddans votre exemple C ++ définit (une partie de) le type de la fonction - pas le type de retour. Cela limite la valeur autorisée pour la fonction return; tout ce qui peut convertir en vide (ce qui n'est rien). Si la fonction returnest, elle ne doit pas être suivie d’une valeur. Le type complet de la fonction est void () (char const*, char const*, int, char const *). + 1 pour utiliser char constau lieu de const char:-)
Clearer
4
Cela ne signifie pas pour autant qu'il soit plus logique de définir un type de fond, il suffit simplement de noter les fonctions si elles reviennent ou non dans le langage. En fait, étant donné que les fonctions peuvent échouer pour différentes raisons, il semble préférable de coder la raison plutôt que d'utiliser un terme fourre-tout, un peu comme le concept relativement récent d'annoter les fonctions en fonction de leurs effets secondaires.
GregRos
2
En fait, il y a une raison pour que "ne retourne pas" et "a le type de retour X" indépendants: Compatibilité avec votre code précédent, car la convention d'appel peut dépendre du type de retour.
Déduplicateur
est le [[noreturn]] par de la syntaxe ou un ajout de fonctionnalité?
Zaibis
1
[suite] Globalement, je dirais simplement qu'une discussion sur les avantages de ⊥ doit définir ce qui constitue une implémentation de; et je ne pense pas qu'un système de types qui n'a pas ( a → ⊥) ≤ ( ab ) soit une implémentation utile de. Donc, dans ce sens, l’ABI SysV x86-64 C (entre autres) ne permet tout simplement pas de mettre en œuvre.
Alex Shpilkin
26

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.

Theodore Norvell
la source
Quelle est la différence entre le type forall a . [a]et le type [a]dans Haskell? Les variables de type ne sont-elles pas déjà universellement quantifiées dans les expressions de type Haskell?
Giorgio
@Giorgio Dans Haskell, la quantification universelle est implicite s'il est clair que vous regardez un schéma de type. Vous ne pouvez même pas écrire forallen standard dans Haskell 2010. J'ai écrit la quantification de manière explicite, car il ne s'agit pas d'un forum Haskell et certaines personnes peuvent ne pas être familiarisées avec les conventions de Haskell. Donc, il n'y a pas de différence sauf que ce forall a . [a]n'est pas standard alors que l' [a]est.
Theodore Norvell
19

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é.

à gauche autour de
la source
"Le type du bas (je l'appellerai Void)", qui ne doit pas être confondu avec la valeur bottom , qui est un membre de n'importe quel type dans Haskell .
mb21
18

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.

Karl Bielefeldt
la source
12
«La liste vide de Haskell est un constructeur de types»: la chose la plus pertinente ici est certainement le fait qu’elle est polymorphe ou surchargée - c’est-à-dire que les listes vides de différents types sont des valeurs distinctes, mais les []représentent toutes et le type spécifique si nécessaire.
Peter LeFanu Lumsdaine
Fait intéressant: Si vous essayez de créer un tableau vide dans l'interpréteur Haskell, vous obtenez une valeur très précise avec un type très indéfini: [a]. De même, les :t Left 1rendements Num a => Either a b. En fait, l'évaluation de l'expression force le type de a, mais pas celui de b:Either Integer b
John Dvorak
5
La liste vide est un constructeur de valeur . Un peu déroutant, le constructeur de type impliqué a le même nom mais la liste vide elle-même est une valeur, pas un type (enfin, il existe des listes de niveaux de type aussi, mais c'est un tout autre sujet). La partie qui fait fonctionner la liste vide pour tout type de liste est implicite foralldans son type forall a. [a],. Il y a de bonnes façons de penser forall, mais il faut un certain temps pour vraiment comprendre.
David
@PeterLeFanuLumsdaine C'est exactement ce que signifie constructeur de type. Cela signifie simplement que c'est un type avec un type différent de *.
GregRos
2
En Haskell []est un constructeur de type et []est une expression représentant une liste vide. Mais cela ne signifie pas que "la liste vide de Haskell est un constructeur de type". Le contexte indique clairement si []est utilisé comme type ou comme expression. Supposons que vous déclariez data Foo x = Foo | Bar x (Foo x); vous pouvez maintenant utiliser Foocomme constructeur de type ou comme valeur, mais il est fort probable que vous ayez choisi le même nom pour les deux.
Theodore Norvell
3

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.

usr
la source
2

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.

Telastyn
la source
11
Non, un type de fond n'est pas le type d'unité. Un type de fond n'a aucune valeur, donc une fonction renvoyant un type de fond ne devrait pas être
renvoyée
@BasileStarynkevitch - Je ne parle pas du type d'unité. Le type d'unité est mappé voiddans les langues communes (bien qu'avec une sémantique légèrement différente pour le même usage), pas null. Bien que vous ayez également raison, la plupart des langages ne modélisent pas null comme type de fond.
Telastyn
3
@TheodoreNorvell - les premières versions de Tangent l'ont fait - bien que je sois son auteur, c'est peut-être de la triche. Je n'ai pas enregistré les liens pour d'autres, et cela fait longtemps que je n'ai pas fait cette recherche.
Telastyn
1
@Martijn Mais vous pouvez utiliser null, par exemple, vous comparez un pointeur à nullun résultat booléen. Je pense que les réponses montrent qu'il existe deux types de fonds distincts. (a) Langues (par exemple Scala) où le type qui est un sous-type de chaque type représente des calculs qui ne donnent aucun résultat. Il s'agit essentiellement d'un type vide, bien que techniquement souvent peuplé par une valeur inférieure inutile représentant non-fin. (b) Des langues telles que Tangent, dans lesquelles le type du bas est un sous-ensemble de tous les autres types, car il contient une valeur utile qui se trouve également dans tous les autres types: null.
Theodore Norvell
4
Il est intéressant de noter que certaines langues ont une valeur avec un type que vous ne pouvez pas déclarer (commun pour le littéral nul), tandis que d'autres ont un type que vous pouvez déclarer mais n'a pas de valeurs (un type de fond traditionnel) et qu'elles remplissent des rôles assez comparables. .
Martijn
1

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.

Marc van Leeuwen
la source
Donc , l'idée que var foo = someCondition() ? functionReturningBar() : functionThatAlwaysThrows()pourrait en déduire le type de fooque Bar, puisque l'expression ne pourrait jamais céder quoi que ce soit d' autre?
Supercat
1
Vous venez de décrire le type d'unité, du moins dans la première partie de votre réponse. Une fonction qui renvoie le type d'unité est le même que celui qui est déclaré que le retour voiden C. La deuxième partie de votre réponse, vous parlez d'un type pour une fonction qui ne retourne jamais, ou une liste sans Elements- qui est en effet le type bas! (C'est souvent écrit _|_plutôt que *. Pas sûr de savoir pourquoi. Peut-être parce que ça ressemble à un fond (humain) :)
andrewf
2
Pour éviter tout doute: «ne retourne rien d’utile» est différent de «ne retourne pas»; le premier est représenté par le type d'unité; la seconde par le type Bottom.
Andrewf
@andrewf: Oui, je comprends la distinction. Ma réponse est un peu longue, mais ce que je voulais dire, c'est que le type d'unité et le type de fond jouent tous deux (des rôles différents mais comparables) en permettant à certaines expressions d'être utilisées de manière plus flexible (mais en toute sécurité).
Marc van Leeuwen
@supercat: Oui, c'est l'idée. Actuellement en C ++ qui est illégal, bien qu'il serait valable que si functionThatAlwaysThrows()ont été remplacées par un explicite throw, en raison de la langue spéciale dans la norme. Avoir un type qui fait cela serait une amélioration.
Marc van Leeuwen
0

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).

gnasher729
la source