Sommaire
Bonjour Nal,
Tu seras peut-être content d'apprendre que Letlang avance plutôt bien. Voici donc un nouveau "devlog" qui aujourd'hui parlera de vérification des types, et de comment je compte compiler une définition de type.
Voici d'abord une petite table des matières de ma série d'articles sur ce projet :
- Encore un nouveau langage de programmation
- Écrire un compilateur en Rust
- Écrire un compilateur en Rust (partie 2)
- Faire la différence entre un nombre et une quantité
Rappel de syntaxe
Avant de rentrer dans le vif du sujet, faisons un petit point sur la notion de type en Letlang.
Concept 1 : Une variable n'a pas de type qui lui est propre.
Prenons l'exemple du langage C :
int i;
char c;
struct Foo myvar;
Les variables i
, c
et myvar
ont un et un seul type.
En Python :
def action(duck):
duck.quack()
duck
a toujours un unique type, la fonction action
ne sait pas lequel, mais une erreur sera levée si ce type ne définit pas une méthode quack
. Le fait est quand même que duck
a un unique type que l'on peut récupérer avec le code suivant :
print(type(duck))
En Letlang, c'est une autre histoire. On n'a pas de fonction type
, ou typeof
. Une variable peut appartenir à plusieurs types.
Par exemple, 42
est un int
, un float
, un nombre pair, un nombre complexe, etc…
Concept 2 : C'est le type qui définit les propriétés nécessaires pour déterminer si une variable lui appartient.
Des exemples de code valent mille mots :
class even(n: int) {
n % 2 = 0
}
On définit un nouveau type even
. Il est construit à partir d'une valeur qui appartient au type int
. Et il stipule qu'il contient toutes les valeurs dont le modulo par 2 est égal à 0.
C'est comme si l'on définissait la fonction suivante (code Python) :
def is_even(n):
return isinstance(n, int) and n % 2 == 0
Et cette fonction est ensuite exécutée à chaque fois qu'il y a besoin de vérifier qu'une variable est bien un nombre entier, par exemple :
func div_by_2(n: even) -> int {
n / 2
}
Un appel de cette fonction se traduirait par (code Python) :
if not is_even(n):
raise TypeError("oops")
div_by_2(n)
Concept 3 : On peut composer les types ensembles.
En Letlang, comme en TypeScript, on va avoir les opérateurs |
, &
et !
qui vont permettre de composer plusieurs types pour en créer de nouveaux.
Exemple :
class even(n: int) {
n % 2 = 0
}
class odd(n: int & !even)
Concept 4 : Il existe des types primitifs.
Les "valeurs littérales" en Letlang sont typées :
-
42
est unint
et unfloat
(et unnumber
) -
"hello world"
est unestring
-
true
est unbool
-
:ok
est unatom
(cf Erlang/Elixir) -
(:ok, 42)
est untuple<atom, number>
J'ai pas encore implémenté les types plus complexes comme les listes, les ensembles, et les dictionnaires (à la TypeScript). Mais ça viendra, chaque chose en son temps :)
Concept 5 : Les valeurs littérales sont également des types.
Cela permet de créer des types du style :
class result<T, E>(v: (:ok, T) | (:error, E))
:ok
et :error
sont utilisés en tant que type. Ainsi le tuple (:un_autre_atom, 42)
n'appartient pas à ce type.
Un framework pour vérifier les types
Que je vérifie les types à la compilation, ou au runtime (les deux seront nécessaires), j'ai besoin d'une manière de représenter en Rust à la fois :
- les valeurs
- les types
- les propriétés à vérifier
- les paramètres des types génériques
Commençons par se représenter les valeurs primitives :
#[derive(Debug, Clone, PartialEq)]
pub enum PrimitiveValue {
Boolean(bool),
Integer(i64),
Float(f64),
String(String),
Atom(String),
}
Et de manière plus générale, n'importe quelle valeur :
#[derive(Debug, Clone, PartialEq)]
pub enum Value<'a> {
Primitive(PrimitiveValue),
Tuple(Vec<&'a Value<'a>>),
// list, set, dict, ...
}
Maintenant, le compilateur va pouvoir encapsuler les données avec ce type Value
lors de la génération du code :
let ok_atom = Value::Primitive(PrimitiveValue::Atom("ok".to_string()));
let n_val = Value::Primitive(PrimitiveValue::Integer(42));
let result_tuple = Value::Tuple(vec![&ok_atom, &n_val]);
Comme dit précédemment, un type Letlang équivaut à une fonction qui prend en paramètre une valeur et retourne un booléen (vrai si la valeur appartient au type, faux sinon).
Cette "fonction" a besoin d'information supplémentaires, comme les paramètres génériques du type par exemple. On va donc plutôt représenter cela avec une structure qui implémente un trait.
Notre trait va être tout simple :
pub trait Type {
fn has(&self, llval: &Value) -> bool;
}
Ainsi, chaque "type" Letlang sera traduit par une structure qui implémente ce trait. Bien sûr, le "runtime" Letlang va en fournir quelques uns par défaut :
pub struct BooleanType;
impl Type for BooleanType {
fn has(&self, llval: &Value) -> bool {
match llval {
Value::Primitive(PrimitiveValue::Boolean(_)) => true,
_ => false,
}
}
}
Jusque là, c'est plutôt simple, on va avoir la même chose pour les autres types primitifs.
On va ensuite créer un type ValueType
qui représentera les valeurs primitives en tant que type :
pub struct ValueType<'v> {
pub llval: &'v PrimitiveValue,
}
impl<'v> Type for ValueType<'v> {
fn has(&self, llval: &Value) -> bool {
match llval {
Value::Primitive(pval) => {
pval == self.llval
},
_ => false,
}
}
}
NB : Ici, j'utilise bien PrimitiveValue
et non Value
. On verra par la suite que les valeurs composites sont typées par des types génériques.
En parlant du loup, vient maintenant notre premier type générique. En effet, le type tuple
n'existe pas, il s'agirat plutôt du type tuple<T...>
. Son implémentation n'est pas très compliquée :
pub struct TupleType<'t> {
pub members_types: Vec<&'t dyn Type>, // T...
}
impl<'t> Type for TupleType<'t> {
fn has(&self, llval: &Value) -> bool {
match llval {
Value::Tuple(members) => {
// si pas le même nombre d'éléments, même pas la peine de continuer
if members.len() != self.members_types.len() {
return false;
}
// liste de couple (value, type)
let pairs = members.iter().zip(self.members_types.iter());
for (member_val, member_type) in pairs {
if !member_type.has(member_val) {
// si l'un des membres du tuple ne correspond pas au type attendu...
return false;
}
}
true
},
_ => false,
}
}
}
En bref, on s'assure que chaque élément de la valeur correspond au type correspondant du tuple.
Pour boucler notre framework, on a besoin d'implémenter le résultat des opérateurs |
, &
et !
. Rien de bien complexe encore une fois :
pub struct OneOfType<'t> {
pub lltypes: Vec<&'t dyn Type>,
}
impl<'t> Type for OneOfType<'t> {
fn has(&self, llval: &Value) -> bool {
for lltype in self.lltypes.iter() {
if lltype.has(llval) {
return true;
}
}
false
}
}
On se prépare à une future optimisation qui traduira a | b | c
en |(a, b, c)
et non |(a, |(b, c))
. Même si l'implémentation actuelle de mon AST n'intègre pas cette optimisation, ce n'est pas très grave.
pub struct AllOfType<'t> {
pub lltypes: Vec<&'t dyn Type>,
}
impl<'t> Type for AllOfType<'t> {
fn has(&self, llval: &Value) -> bool {
for lltype in self.lltypes.iter() {
if !lltype.has(llval) {
return false;
}
}
true
}
}
Pareil, pas de grande surprise ici. Juste totalement l'opposé du type OneOfType
.
pub struct NotType<'t> {
pub lltype: &'t dyn Type,
}
impl<'t> Type for NotType<'t> {
fn has(&self, llval: &Value) -> bool {
!self.lltype.has(llval)
}
}
Voilà. On a maintenant notre framework complet. Mettons le à l'épreuve.
Une paire d'exemple
Exemple 1 : Le type result<T, E>
Reprenons sa définition :
class result<T, E>(v: (:ok, T) | (:error, E))
Quel code Rust devrait produire le compilateur ?
En premier lieu, il y a sa représentation :
pub struct ResultType<'t> {
pub ok_val_type: &'t dyn Type, // T
pub err_val_type: &'t dyn Type, // E
}
NB : Les noms des structures et des champs ici sont générés par un humain (moi), pas par le futur compilateur qui produira sûrement des choses du style branch_0
/ branch_1
/ etc…
Et pour l'implémentation :
impl<'t> Type for ResultType<'t> {
fn has(&self, llval: &Value) -> bool {
// le but est de créer dans un premier temps le type `(:ok, T) | (:error, E)`
// on commence par `(:ok, T)` :
// on représente l'atom `:ok` en tant que type
let ok_tag = PrimitiveValue::Atom("ok".to_string());
let ok_tag_type = ValueType { llval: &ok_tag };
// et on construit le type `tuple<:ok, T>`
let ok_tuple_type = TupleType {
members_types: vec![&ok_tag_type, self.ok_val_type],
};
// on enchaîne avec `(:error, E)` :
// on représente l'atom `:error` en tant que type
let err_tag = PrimitiveValue::Atom("error".to_string());
let err_tag_type = ValueType { llval: &err_tag };
// et on construit le type `typle<:error, T>`
let err_tuple_type = TupleType {
members_types: vec![&err_tag_type, self.err_val_type],
};
// enfin, on peut combiner les deux avec l'opérateur | :
let lltype = OneOfType {
lltypes: vec![
&ok_tuple_type,
&err_tuple_type,
],
};
// le type `result<T, E>` n'inclut pas de check supplémentaire :
lltype.has(llval)
}
}
Ok, c'est plutôt intéressant. Grâce à ce mécanisme, le système d'inférence de type sera juste une "factory" qui à partir d'un AST retourne une instance de ces structures.
Exemple 2 : Le type even
Reprenons sa définition :
class even(n: int) {
n % 2 = 0
}
Cela donnerait :
pub struct EvenType;
impl Type for EvenType {
fn has(&self, llval: &Value) -> bool {
let int_type = IntegerType {};
if !int_type.has(llval) {
return false;
}
let res = call("=",
call("%",
llval,
&Value::Primitive(PrimitiveValue::Integer(2))
),
&Value::Primitive(PrimitiveValue::Integer(0))
);
match res {
Value::Primitive(PrimitiveValue::Boolean(true)) => true,
_ => false,
}
}
}
NB : Ici l'usage de call
représente l'exécution du code présent dans la définition du type. Cela ne sera certainement pas sa forme définitive cela dit. Mais l'idée est bien là.
Conclusion
Ce framework me permettra d'implémenter le type checking lors de la phase de compilation, et le système d'inférence de type sera un ensemble de "factory" générant les types en fonction de l'AST. Ce code généré lors de la compilation sera également inclut au runtime. En effet, les données issues d'effets de bords (comme la lecture depuis un fichier, socket, clavier, …) devront aussi être vérifiées au runtime.
Je suis curieux d'avoir ton avis sur le design et l'implémentation. Penses tu qu'il y a mieux ?
Pour ceux qui ont tout lu, voici un carré glacé :
# type
Posté par Nicolas Boulay (site web personnel) . Évalué à 4.
Je vois que tu as pensé à créer des types pour les litéraux. C'est une bonne idée.
J'ai un cas d'usage assez chiant quand tu veux créer des définitions de configuration pour un système. Imagines une liste de définition de message, tu peux avoir une matrice de base (exemple A429), une lib de ta boite (A429 + extension Thales), et tu veux tout mettre ensemble et ajouter les spécificités de ton équipements (pilote auto). La lib peut définir des messages (vitesse), messages définis dans le fichier final, mais qui peut contenir des informations comme "le type de la colonne 2 est un entier". Concrètement, cela veut dire que le type est une donnée comme une autre.
Aujourd'hui, vouloir faire cela avec les outils classiques imposent d'utiliser un enum et de recoder un système de typage.
Le deuxième point qui pourrait être très sympa, est d'étendre le concept de "constante propagation" lors de la phase d'optimisation en incluant les types structurées. Actuellement, ce genre d'optimisation ne marche qu'avec les types primitifs. Peu de langages permettent d'écrire un littéraux d'un type structuré ou une liste (comme le Json de JS). Imagines si on peut faire de la constante propagation de string, si on a un interpréteur de regexp, on obtient un compilateur de regexp. Les performances obtenus n'auraient plus rien à voir.
"La première sécurité est la liberté"
[^] # Re: type
Posté par David Delassus (site web personnel) . Évalué à 3.
C'est nécessaire vu que le langage target est statiquement typé. En fait, même si je target le Python ou l'Assembleur, à un moment j'ai besoin de savoir que
"hello world"
est unestring
. Tout les types composites sont construit à partir de littéraux, peu importe le langage.En Letlang ce n'est pas le cas. Je n'ai pas de type
type
par exemple. Ce qui veut dire que tu ne peux pas passer un type en argument d'un fonction :Le seul moyen de "passer un type en argument" c'est en utilisant des fonctions génériques :
Mais on ne peut toujours pas manipuler
T
comme on manipulerait un entier ou un booléen.Je suis encore loin d'implémenter des optimisations, mais oui c'est dans mon radar.
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
[^] # Re: type
Posté par Nicolas Boulay (site web personnel) . Évalué à 3.
Dommage, pour les variables qui contiennent un type, cela serait pratique pour un truc comme du JSON.
"La première sécurité est la liberté"
[^] # Re: type
Posté par David Delassus (site web personnel) . Évalué à 2.
Tu aurais un exemple à donner ?
Parce qu'il restera possible de définir un type comme ceci :
Et ensuite de l'utiliser dans une fonction :
Ce qu'il faut bien comprendre, c'est la syntaxe :
En gros, tout ce qui est après le
:
dans les( )
c'est une définition de type. En d'autres mots, toutes les expressions suivantes sont des types :int
int | bool & !42
(:ok, int)
{ debug: bool }
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
[^] # Re: type
Posté par Nicolas Boulay (site web personnel) . Évalué à 3.
Non, cela n'est pas strictement équivalent.
Tu aurais un cas ou tu définis message comme :
class messageDef({
address: int,
type_: type,
})
class messageDefSpeed({
adress: 0x04,
type: float32,
})
classe messageSpeed({
def: messageDefSpeed,
data: def.type
})
Les 3 classes pourraient être dans 3 bibliothèques différentes. Une instance de messageSpeed serait le contenu d'un paquet circulant sur le réseau.
La différence avec ton cas, est l'existence d'un "metatype" qui contraint ce que peut être messageDefSpeed qui est lié à la nature du lien (un message sur ARINC 429). Et chaque message est différent selon son adresse.
C'est une manière de contraindre les données lors d'utilisation d'une lib. Peut-être que c'est faisable avec des types paramétriques, mais est-ce que cela resterait lisible ?
Cela me fait aussi penser que j'aurais aimer parfois un moyen de déclarer les dépendances entre modules, et surtout les dépendances que je ne veux jamais. Le but est d'éviter un refactoring avec des inclusions sauvages qui transforment le code en plat de spaghetti.
Par exemple, exiger qu'une classe utilitaire ne puisse jamais être dépendante de module "business". Cela serait une manière de contraindre la structure du programme.
"La première sécurité est la liberté"
[^] # Re: type
Posté par David Delassus (site web personnel) . Évalué à 2.
Alors pour reprendre ton exemple :
Est-ce que cela répond à la problématique ?
Tu veux quelque chose de similaire à Boundary en Elixir. C'est aussi dans mon radar mais pour bien plus tard.
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
[^] # Re: type
Posté par Nicolas Boulay (site web personnel) . Évalué à 3.
Oui. En gros, on peut mettre des littéraux dans une définition, et l'on peut définir le type d'un champ plus tard.
Oui, en gros, c'est ça. Si tu définit une architecture hexagonal, par exemple, comment faire pour le déclarer dans le code pour éviter que des refactorisation ne casse accidentellement l'architecture. Typiquement, tu veux éviter l'introduction de certaine dépendance, que des modules feuilles restent des feuilles, etc…
D'ailleurs, est-ce que tu as déjà codé et tester le "&" et le "non" dans ton typage ? J'ai écris un début de truc semblable qui mélange type et validité, et le "non" me pose un gros problème de définition. Si cela t'intéresse je pourrais retrouver le cas.
C'est l'outil coherentyaml ( https://github.com/nicolasboulay/coherentyaml ). Il faudrait que je le termine d'ailleurs.
"La première sécurité est la liberté"
[^] # Re: type
Posté par David Delassus (site web personnel) . Évalué à 2.
Oui, ça permet par exemple de définir des énumérations :
J'ai pas encore réfléchit à comment implémenter le type
unknown
. J'aimerais aussi éviter le typeany
si possible. Je regarderais sûrement l'implémentation de TypeScript pour m'en inspirer.J'ai l'implémentation qui est décrite dans l'article (les structs
OneOfType
,AllOfType
etNotType
).Avec les tests suivants :
Ce qui en Letlang s'écrirait :
Ça fonctionne bien.
NB: Je vais peut-être changer les symboles pour pas confondre :
!true = false
!42 = false
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
[^] # Re: type
Posté par Nicolas Boulay (site web personnel) . Évalué à 3.
Mes erreurs autour de non était lors de composition.
J'ai utilisé les tautologies de https://fr.wikipedia.org/wiki/Implication_(logique) comme test. De mémoire, c'était le Modus Tollens qui était faux : ((A -> B) & ~B) -> ~A avec (a -> b) = (~a or b)
"La première sécurité est la liberté"
# Carré glacé ?
Posté par Tit . Évalué à 1. Dernière modification le 25 avril 2022 à 17:46.
Mais où sont donc ces carrés ? que l'on regarde de dessus ou de coté on ne voit que des rectangles ?
moi j'ai toujours entendu appelé ça des mille-feuilles (je reconnais que ce nom n'est pas plus approprié), j'avais jamais entendu le terme carré glacé… Où est-ce qu'on cause comme ça ?
[^] # Re: Carré glacé ?
Posté par David Delassus (site web personnel) . Évalué à 3. Dernière modification le 25 avril 2022 à 17:51.
62 méfie te
(si tu le coupe en deux, ça fait 2 petits carrés)
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
[^] # Re: Carré glacé ?
Posté par Tit . Évalué à 1.
pas compris
[^] # Re: Carré glacé ?
Posté par Tit . Évalué à 2.
Compris : https://www.youtube.com/watch?v=4pWwEg4Zqso
[^] # Re: Carré glacé ?
Posté par Ysabeau 🧶 (site web personnel, Mastodon) . Évalué à 3.
Je me suis dit, en voyant la photo que, s'il avait des problèmes de code, l'explication était peut-être là. (je sors)
« Tak ne veut pas quʼon pense à lui, il veut quʼon pense », Terry Pratchett, Déraillé.
[^] # Re: Carré glacé ?
Posté par Benoît Sibaud (site web personnel) . Évalué à 5.
Bah des fois si : « L'adoption plus récente d'un pliage en deux par certains cuisiniers conduit à un mille-feuille comportant un nombre différent de feuillets, 2048 paires dans le cas de la recette d'André Guillot »
cf https://fr.wikipedia.org/wiki/Mille-feuille (page que j'avais regardé ce matin car je ne connaissais pas « carré glacé » non plus)
[^] # Re: Carré glacé ?
Posté par Tit . Évalué à 1.
ça alors, c'est beaucoup, j'aurais pas cru !
Déjà avec la méthode traditionnelle "en six étapes de pliages en trois, le mille-feuille comporte en réalité 729 paires de feuillets"
Je comprends pas le "paire" si je plie en 3, j'ai 3 feuillets, pas trois paires de feuillets, non ?
[^] # Re: Carré glacé ?
Posté par Benoît Sibaud (site web personnel) . Évalué à 4.
Cf la formule de https://fr.wikipedia.org/wiki/P%C3%A2te_feuillet%C3%A9e
Ainsi, dans la recette classique, en pliant la pâte en trois (deux plis type pli roulé) et en réalisant six tours, on obtient (…) 729 couches de beurre et donc 730 feuillets de pâte.
[^] # Re: Carré glacé ?
Posté par Gil Cot ✔ (site web personnel, Mastodon) . Évalué à 2. Dernière modification le 01 mai 2022 à 00:36.
2048 …c'est de là un certain jeu ?
après, pour en revenir aux carrés qui sont rectangles, je crois que c'est la quadrature de Letlang ; je l'ai compris en lisant « En Letlang, c'est une autre histoire. On n'a pas de fonction type, ou typeof. Une variable peut appartenir à plusieurs types. Par exemple, 42 est un int, un float, un nombre pair, un nombre complexe, etc… » et en me disant « polymorphe »
“It is seldom that liberty of any kind is lost all at once.” ― David Hume
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.