Le type Never est le type le plus inhabituel du système de types de FLIN. Il n'a aucune valeur. On ne peut pas créer un Never. On ne peut pas stocker un Never. On ne peut pas passer un Never à une fonction. Son but n'est pas de décrire des données -- c'est de décrire l'impossibilité.
Et pourtant, ce type sans valeurs est l'un des types les plus importants de tout le système. C'est le mécanisme par lequel le compilateur prouve que votre code gère tous les cas. C'est le fondement théorique des types pour la vérification d'exhaustivité.
Ce que signifie Never
En théorie des types, le type Never (aussi appelé type bottom, ou « ! » en Rust, ou « never » en TypeScript) est le type des calculs qui ne produisent pas de valeur. Une fonction qui lève toujours une erreur renvoie Never. Un bras de match que le compilateur prouve inatteignable a le type Never. Une variable qui a été réduite à néant -- parce que toutes les possibilités ont été traitées -- a le type Never.
flin// A function that never returns
fn panic(message: text) -> never {
log_error(message)
abort()
}
// A match arm that is unreachable
match direction {
North -> "north"
South -> "south"
East -> "east"
West -> "west"
// No _ needed -- all variants covered
// Any additional arm would have type never (unreachable)
}Never dans le système de types
Never est représenté comme un variant dans l'enum FlinType :
rustpub enum FlinType {
Int,
Number,
Text,
Bool,
// ...
Never, // The bottom type
Any, // The top type
}Never et Any sont des duaux. Any est le supertype de tout -- chaque type est assignable à Any. Never est le sous-type de tout -- Never est assignable à chaque type.
Cette relation de sous-typage a une conséquence pratique : une fonction retournant Never peut être utilisée n'importe où. Si panic() retourne Never, alors panic() est un int valide, un text valide, un User valide. Parce que panic() ne produit jamais réellement une valeur, il est vacuement compatible avec chaque type.
rustfn types_compatible(&self, expected: &FlinType, actual: &FlinType) -> bool {
match (expected, actual) {
// Never is compatible with everything (subtype of all types)
(_, FlinType::Never) => true,
// Any accepts everything (supertype of all types)
(FlinType::Any, _) => true,
// ...
}
}La première règle -- Never est compatible avec tout -- signifie qu'on peut écrire :
flinfn get_value(id: int) -> int {
user = User.find(id)
if user {
return user.score
}
panic("User not found") // returns never, but int is expected -- OK
}L'appel panic() retourne Never, qui est assignable à int. Le compilateur accepte cela parce qu'il sait que la fonction ne retournera jamais réellement à ce point.
Vérification d'exhaustivité
La vérification d'exhaustivité est la garantie du compilateur que chaque cas possible dans une expression match ou une chaîne if-else est traité. Elle fonctionne en réduisant progressivement le type de la valeur matchée jusqu'à ce qu'il ne reste plus rien -- jusqu'à ce que le type atteigne Never.
Sur les enums
La forme la plus simple de vérification d'exhaustivité porte sur les enums :
flinenum Color { Red, Green, Blue }
match color {
Red -> "#FF0000"
Green -> "#00FF00"
// ERROR: non-exhaustive -- missing Blue
}L'algorithme :
rustfn check_enum_exhaustiveness(
&self,
enum_type: &FlinType,
arms: &[MatchArm],
span: Span,
) {
let FlinType::Enum { variants, .. } = enum_type else { return };
let variant_names: HashSet<String> = variants.iter()
.map(|(name, _)| name.clone())
.collect();
let mut covered: HashSet<String> = HashSet::new();
let mut has_wildcard = false;
for arm in arms {
match &arm.pattern {
Pattern::EnumVariant { variant, .. } => {
covered.insert(variant.clone());
}
Pattern::Wildcard | Pattern::Identifier { .. } => {
has_wildcard = true;
}
Pattern::Or(patterns) => {
for p in patterns {
if let Pattern::EnumVariant { variant, .. } = p {
covered.insert(variant.clone());
}
}
}
_ => {}
}
}
if !has_wildcard {
let uncovered: Vec<&String> = variant_names.difference(&covered).collect();
if !uncovered.is_empty() {
self.report_error(&format!(
"non-exhaustive match on {}: missing variant(s): {}",
enum_type.display_name(),
uncovered.iter().map(|s| s.as_str()).collect::<Vec<_>>().join(", ")
));
}
}
}On commence avec l'ensemble de tous les variants. Pour chaque bras, on marque le variant comme couvert. S'il reste des variants non couverts et qu'il n'y a pas de joker, on signale une erreur.
Sur les booléens
Les booléens ont exactement deux valeurs, donc l'exhaustivité est simple :
flinmatch flag {
true -> "yes"
false -> "no"
}Les deux valeurs sont couvertes. Pas besoin de joker. Le compilateur vérifie :
rustfn check_bool_exhaustiveness(&self, arms: &[MatchArm], span: Span) {
let has_true = arms.iter().any(|a| matches_literal_bool(&a.pattern, true));
let has_false = arms.iter().any(|a| matches_literal_bool(&a.pattern, false));
let has_wildcard = arms.iter().any(|a| is_wildcard(&a.pattern));
if !has_wildcard && (!has_true || !has_false) {
let missing = if !has_true && !has_false {
"true, false"
} else if !has_true {
"true"
} else {
"false"
};
self.report_error(&format!("non-exhaustive match on bool: missing {}", missing));
}
}Sur les types union
L'exhaustivité des types union fonctionne en suivant quels membres ont été traités :
flinvalue: int | text | bool = getData()
match value {
is int -> handle_int(value)
is text -> handle_text(value)
is bool -> handle_bool(value)
}Chaque bras is couvre un membre de l'union. Après les trois, l'union est entièrement couverte. S'il manque un bras :
flinmatch value {
is int -> handle_int(value)
is text -> handle_text(value)
// ERROR: non-exhaustive -- bool is not covered
}Le mécanisme de soustraction de type de l'article sur les gardes de type pilote cela. Après is int et is text, le type restant est bool. Si aucun bras ne traite bool et qu'il n'y a pas de joker, le match est non exhaustif.
Sur les types infinis
Les entiers, les chaînes de caractères et les nombres à virgule flottante ont une infinité de valeurs possibles. La vérification d'exhaustivité ne peut pas toutes les énumérer. Pour ces types, un bras joker est requis :
flinmatch count {
0 -> "none"
1 -> "one"
_ -> "many" // required for int
}Sans le bras _, le compilateur rejette le match :
error[E0015]: non-exhaustive match
--> app.flin:5:1
|
5 | match count {
| ^^^^^ patterns 0, 1 do not cover all possible int values
|
= hint: add a wildcard arm: _ -> ...Le type Never en pratique
Détection de code inatteignable
Lorsque le rétrécissement de type réduit une variable à Never, tout code utilisant cette variable est inatteignable :
flinvalue: int | text = getData()
if value is int {
// value: int
} else if value is text {
// value: text
} else {
// value: never -- this branch is unreachable
// The compiler may warn about dead code
}Après avoir traité int et text, l'union est épuisée. La branche else a le type Never, ce qui signifie qu'aucune valeur ne peut l'atteindre. Le compilateur peut signaler cela comme du code mort.
Type de retour de fonction
Les fonctions qui lèvent inconditionnellement une exception, terminent le programme ou bouclent indéfiniment retournent Never :
flinfn unreachable(message: text) -> never {
log("UNREACHABLE: " + message)
abort()
}
fn todo(feature: text) -> never {
panic("TODO: " + feature + " not implemented")
}Ces fonctions sont utiles comme placeholders et gestionnaires d'erreurs. Parce que Never est un sous-type de tout, elles peuvent être utilisées dans n'importe quelle position d'expression :
flinfn process(value: int | text) -> text {
match value {
is int -> text(value)
is text -> value
_ -> unreachable("all types covered")
}
}Le bras joker appelle unreachable(), qui retourne Never. Puisque Never est assignable à text (le type de retour de la fonction), le compilateur l'accepte.
Match exhaustif comme expression
Lorsqu'une expression match est exhaustive, le compilateur sait qu'un bras s'exécutera toujours. Cela signifie que le match produit toujours une valeur :
flinenum Direction { North, South, East, West }
// This match always produces a text value
description = match direction {
North -> "heading north"
South -> "heading south"
East -> "heading east"
West -> "heading west"
}
// description: text (guaranteed)Sans exhaustivité, le match pourrait ne pas exécuter de bras, et description serait non initialisé. La vérification d'exhaustivité garantit l'initialisation.
Le type Never dans la VM
Au niveau de la VM, Never n'existe pas comme valeur à l'exécution. Il n'y a pas de variant Value::Never. Le type Never est purement un concept de compilation -- il n'existe que dans le vérificateur de types.
C'est intentionnel. Une valeur de type Never ne peut jamais être créée, donc la VM n'a jamais besoin d'en représenter une. Tout chemin de code que le vérificateur de types détermine comme menant à une valeur Never est garanti inatteignable à l'exécution (via un appel à panic, une boucle infinie, etc.).
rustpub enum Value {
Int(i64),
Number(f64),
Text(String),
Bool(bool),
None,
Object(Box<Object>),
List(Vec<Value>),
// No Never variant -- it never exists at runtime
}Messages d'erreur
Les erreurs d'exhaustivité sont parmi les plus conviviales du compilateur de FLIN :
error[E0015]: non-exhaustive match
--> app.flin:10:1
|
10 | match shape {
| ^^^^^ missing variant(s): Triangle
|
= note: Shape has variants: Circle, Square, Triangle, Rectangle
= note: arms cover: Circle, Square, Rectangle
= hint: add a match arm: Triangle -> { ... }
= hint: or add a wildcard: _ -> { ... }L'erreur liste ce qui manque, ce qui est couvert, et suggère deux corrections : soit traiter le variant manquant spécifique, soit ajouter un joker. Les deux sont des solutions valides, et le développeur choisit en fonction de son intention.
Décisions de conception
L'exhaustivité est requise, pas optionnelle. Certains langages font de la vérification d'exhaustivité un avertissement. FLIN en fait une erreur. C'est un choix délibéré pour la sécurité. Si vous matchez sur un enum, vous devez traiter chaque variant. Point. Si vous ajoutez un variant à un enum, chaque match doit être mis à jour.
Les jokers se désengagent de l'exhaustivité pour des bras spécifiques, pas globalement. Un joker _ couvre tous les cas restants. C'est explicite -- le développeur dit « je sais qu'il y a d'autres cas, et je choisis de les traiter uniformément ». C'est différent d'ignorer les autres cas.
Pas de fall-through. Contrairement au switch du C, les bras match de FLIN ne passent pas au suivant. Chaque bras est indépendant. Cela élimine toute une classe de bugs où un break manquant cause l'exécution non intentionnelle du cas suivant.
Les clauses de garde ne comptent pas pour l'exhaustivité. Un bras avec une garde (x if x > 0) pourrait ne pas matcher même si le motif matche. Le compilateur ne peut pas déterminer à la compilation si la garde sera vraie, donc les bras avec garde sont traités comme potentiellement non-matchants pour les besoins de l'exhaustivité.
flinmatch count {
x if x > 0 -> "positive"
x if x < 0 -> "negative"
// Still need: _ -> "zero" or 0 -> "zero"
// Guards might both be false for count = 0
}Le fondement théorique
Never et l'exhaustivité sont profondément connectés par la correspondance de Curry-Howard -- l'observation que les types correspondent à des propositions et les programmes correspondent à des preuves. Dans cette perspective :
- Une expression match est une preuve que chaque cas est traité
- Un match exhaustif est une preuve complète
- Un match non exhaustif est une preuve incomplète
Neverest la proposition « ceci ne peut pas arriver », et une valeur de typeNeverserait une preuve de l'impossible
Les développeurs FLIN n'ont pas besoin de savoir tout cela. Mais la théorie explique pourquoi ces fonctionnalités existent et pourquoi elles interagissent comme elles le font. La vérification d'exhaustivité n'est pas une règle arbitraire du compilateur -- c'est une conséquence logique de la conception du système de types. Le compilateur n'est pas pointilleux. Il est correct.
Ceci est la partie 41 de la série « How We Built FLIN », documentant comment un CEO à Abidjan et un CTO IA ont conçu et implémenté un langage de programmation à partir de zéro.
Navigation de la série : - [39] Tuples, Enums, and Structs - [40] Type Guards and Runtime Type Narrowing - [41] The Never Type and Exhaustiveness Checking (vous êtes ici) - [42] Generic Bounds and Where Clauses - [43] While-Let Loops and Break With Value