David Delassus a écrit 749 commentaires

Je ne vois toujours pas en quoi ils n'ont pas de type au sens IT du terme.

Il n'existe pas d'opération typeof qui retourne le type de l'objet, car il existe une infinité de collection distincte qui contiennent cet objet.

Un type c'est un ensemble de valeurs (comme N, Q ou R)

Ce qui n'est pas le cas dans la plupart des langages de programmation, en C, en C++, en Python, en Java, etc… le type est une propriété intrinsèque de la-dite valeur.

ici deux est considéré comme de type Event.t et non comme int

Sauf qu'en Letlang, deux est toujours un int et un number.

mais on peut aussi le caster vers un int

En Letlang il n'y a pas besoin de caster, l'opération + attend un number, elle reçoit un number, car deux est un number.

C'est tout l'argument de ce système de type : c'est stupide de devoir caster quand la définition même de l'opération accepte cette valeur.

Dans ton exemple, OCaml croit que l'on ne peut pas additionner des nombres pairs, ce qui est complètement faux.

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

Paramètre (input) ET valeur de retour (output).

Les opérateurs sont aussi des fonctions sous le capot.

Les expressions let introduisent du type checking supplémentaire (spec en cours de rédaction) :

let a: six = add_five(1);
let a < 0;  # TYPE CHECK ERROR

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

Sauf que dans l'exemple que j'ai donné, le type mod4 n'est pas un sous type de even.

Je peux faire le même exemple avec :

class even(n: int) {
  n % 2 = 0;
}

class mod3(n: int) {
  n % 3 = 0;
}

Avec 6 qui fait partie des deux, et 9 qui fait partie que de mod3.

Après, tu peux le tourner dans tout les sens que tu veux pour essayer de lui assigner un type unique. Mais l'implémentation n'est pas faite comme ça. Donc ça ne sert un peu à rien.

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

https://letlang.dev/lep/005/#type-checking

Le but c'est de faire un maximum à la compilation, mais on continue de le faire au runtime quand même (faut bien type-check les side effects aussi :P)

Donc non, ce n'est pas valable que pour les constantes.

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

De ce point de vue de là, les objets de Letlang ont un type unique.

Bah non, toujours pas, vu que Letlang défini un type comme étant une collection d'objet, et spécifie bien qu'un objet peut appartenir à plusieurs collections différentes.

Je reprend un exemple donné dans un autre commentaire:

class even(n: int) {
  n % 2 = 0;
}

class mod4(n: int) {
  n % 4 = 0;
}

L'objet 8 respecte donc tout les type-checks suivants:

assert 8 is number;
assert 8 is int;
assert 8 is even;
assert 8 is mod4;

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

Le type est déterminé par le fait que tu ait fait passer la valeur par un constructeur du type

Non, le type n'est "que une fonction de validation". Cf un de mes articles précédent dans la série, et la section implémentation Rust de la spec.

Par exemple:

class even(n: int) {
  n % 2 = 0;
}

class mod4(n: int) {
  n % 4 = 0;
}

Ici, even et mod4 sont définis tout deux à partir de int et n'ont pas connaissance de l'autre.

Et pourtant :

8 is even;  # because 8 is int and 8 % 2 = 0 is true
8 is mod4;  # becaues 8 is int and 8 % 4 = 0 is true

Et voici l'implémentation Rust de number et int qui sont appelés lors de l'appel de is ou passage en paramètre d'une fonction :

use crate::{Value, PrimitiveValue, Type};

pub struct NumberType;

impl Type for NumberType {
  fn has(&self, llval: &Value) -> bool {
    match llval {
      Value::Primitive(PrimitiveValue::Number(_)) => true,
      _ => false,
    }
  }
}

pub struct IntegerType;

impl Type for IntegerType {
  fn has(&self, llval: &Value) -> bool {
    match llval {
      Value::Primitive(PrimitiveValue::Number(a)) => a.fract() == 0.0,
      _ => false,
    }
  }
}

Je pourrais très bien modifier ces implémentations pour dire que la string "1.5" est un nombre.

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

Devrais-je clarifier dans la LEP que quand je dis "ils n'ont pas de type" je parle de "type" au sens IT du terme?

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

Il faut voir les opérateurs du langage comme des fonctions infixes.

Quand a / b a pour signature number / number -> number, a // b aura pour signature int // int -> int, ensuite c'est le type checking de letlang qui va valider les données en input et output ou lever une exception.

La division euclidienne du type Rust f64 garantie que la sortie est un entier (frac(n) = 0). Du coup j'ai juste besoin de valider que a et b sont des int.

https://doc.rust-lang.org/std/primitive.f64.html#method.div_euclid

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

Le type f64 de Rust fournit des fonctions pour faire de la division euclidienne, donc on peut imaginer des opérateurs différents :

• a / b = float
• a // b = int (division euclidienne)
• a % b = int (reste de la division euclidienne)

C'est pas encore spécifié, donc ça va peut être changer d'ici là.

Pour le "x is part of the class y" je traduit ça par "x fait partie de la classe y" la ou "x is a part of the class y" se traduirait par "x est une partie de la classe y". Mais je vois la confusion, je vais voir pour remplacer par "is included" ou "is contained in". Merci :)

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

Oui, c'est bien, mais en Letlang int et number c'est f64 en Rust.

Et f64 c'est pas N, c'est pas Q, c'est pas R, c'est https://fr.wikipedia.org/wiki/IEEE_754.

int est défini comme ceci:

class int(n: number) {
  frac(n) = 0;
}

On a donc bien le même objet qui appartient à deux ensembles.

Si on peut arrêter la branlette intellectuelle et la guerre d'égo pour se recentrer sur le sujet, ça serait bien. Merci.

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

Moui

Utilité de ce commentaire ?

surtout pas très pertinent pour un système de types informatiques

En quoi c'est pas pertinent ? Je parle de l'inspiration derrière le système de type afin de présenter le système de type justement qui diffère de la plupart des autres langages de programmation.

Mais dire qu’il n’y a pas de “types” en mathématiques est toujours faux.

Il n'y a pas de "type" au sens informatique du terme. Le "type" au sens mathématique du terme c'est l'appartenance à une collection muni ou non d'opérations. Et un objet n'a pas un unique type car c'est la définition de la collection qui détermine cette appartenance.

Si tu dis ∀x ∈ ℚ tel que x = 42, ∀y ∈ ℝ tel que y = 42 : en toute rigueur x ≠ y.

Mais en pratique c'est le cas. x et y désignent tout deux le même objet qui, par la définition de ℚ et ℝ, appartient aux 2 ensembles.

Par abus les mathématiciens finissent par dire que x = y. Mais c’est pas si évident que ça et ça demande tout un travail algébrique pour arriver à dire que ce raccourci d’écriture est légitime.

Et je n'ai pas besoin de rentrer dans ce niveau de détail pour expliquer que ce sont les classes Letlang qui déterminent quels objets sont inclus, et non l'inverse.

Pour les espaces vectoriels tu es obligé de faire la distinction. Parler de 42 comme d’un vecteur ça veut rien dire, tu voulais probablement dire : 42 = 42 · 1 où le gras est un vecteur, en admettant que tu prennes la base canonique. La structure de l’espace vectoriel ℝ n’est pas celle du corps ℝ (le 42 non-gras : c’est le scalaire, c’est une coordonnée qui appartient par définition au corps ℝ, le 42 gras : c’est un vecteur, il appartient au ℝ-espace vectoriel ℝ). Le 42 que tu as donné c’est la coordonnée du vecteur : pour ce faire, tu as considéré ℝ muni d’une structure de (corps-ℝ)-espace vectoriel, avec une base qui plus est.

C’est une erreur classique que de confondre les coordonnées d’un vecteur et le vecteur lui-même.

Je me demande si tu as lu la même chose que j'ai écrit. A aucun moment je ne parle de 42 comme étant un vecteur.

En vrai la seule mention de vecteur dans la spec c'est :

To reduce code duplication, a class can require type parameters:

class vector<T>(v: {x: T, y: T});

According to the above definition:

{x: 0, y: 0} is vector<int> = true;
{x: 0, y: 0} is vector<string> = false;

J'insiste sur le according to the above definition.

Les entiers, les nombres à virgule flottante, la définition de vecteur ci-dessus, et beaucoup de choses en informatique, n'ont pas grand chose à voir avec leur contrepartie mathématique.

Dans cette spec, je parle constamment de la structure des données, et de la définition des collections qui les contiennent. Je fais un rapide parallèle avec la théorie des ensembles ou c'est la définition de la collection qui détermine la structure des objets qu'elle contient.

Alors oui, la partie mathématique n'est pas la plus rigoureuse qui soit, mais ce n'est pas le but en fait, le but c'est de présenter un concept.

Le public auquel je m'adresse n'est pas forcément mathématicien, donc un peu de vulgarisation et quelques raccourcis, ça ne fait de mal à personne.

Le vrai mathématicien lira ça et se dira "oui, bon c'est un peu simplifié et pas très rigoureux, mais soit".

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

Bof, on stocke quand même une entrée dans la "table des matières" du système de fichier pour référencer un fichier vide.

De mémoire, un inode sur ext4 c'est 256 octets, alors que :

$ sh -c "exit 0"

C'est 14 octets pour la commande complète.

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

C'est prévu.

J'ai déjà une grammaire partiellement implémentée avec LALRPOP et Logos (cf un des articles de la série). J'hésite à mettre simplement des bouts de code de cette grammaire, ou à la traduire en grammaire BNF.

Il y aura donc une série de LEP dans la catégorie "Language Grammar" ou "Language Implementation". Mais avant je tenais à mettre sur papier le design des fonctionnalités du language (faisons les choses dans l'ordre).

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

C'est corrigé :)

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

Ta présentation me semble au minimum maladroite. Mais j'ai prête mal compris.

Non-non, je me suis bien mélangé les pinceaux.

La théorie ZFC utilise un axiome de compréhension restreint qui empêche la construction d'un ensemble selon le paradoxe de Russel.

Si je ne m'abuse il n'y a pas non plus de concept de "classe propre" dans ZFC

Il me semble justement décrire les classes comme étant un ajout qui ne fait pas parti de ZFC, je vais reformuler pour clarifier.

DISCLAIMER: Je ne suis pas mathématicien de profession, juste quelqu'un de très curieux qui a lu beaucoup de choses sur le sujet.

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

Dans l'article il explique que la restriction était faite sur daniel.haxx.se et non haxx.se globalement.

Du coup, j'en doute.

EDIT: grillé

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

En gros, on peut mettre des littéraux dans une définition

Oui, ça permet par exemple de définir des énumérations :

class roles(r: "admin" | "moderator" | "guest")

on peut définir le type d'un champ plus tard.

J'ai pas encore réfléchit à comment implémenter le type unknown. J'aimerais aussi éviter le type any si possible. Je regarderais sûrement l'implémentation de TypeScript pour m'en inspirer.

D'ailleurs, est-ce que tu as déjà codé et tester le "&" et le "non" dans ton typage ?

J'ai l'implémentation qui est décrite dans l'article (les structs OneOfType, AllOfType et NotType).

Avec les tests suivants :

let ival = Value::Primitive(PrimitiveValue::Integer(42));

let itype = IntergerType {};

let is_42_type = ValueType { llval: PrimitiveValue::Integer(42) };
let not_42_type = NotType { lltype: &is_42_type };
let int_but_not_42 = AllOfType { lltypes: vec![&itype, &not_42_type] };

assert!(itype.has(&ival));
assert!(!int_but_not_42.has(&ival));

Ce qui en Letlang s'écrirait :

ival := 42

assert ival is int
assert !(ival is (int & !42))

Ç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

Rien de bien récursif. Je le parcours toujours avec un algo impératif.

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

A titre personnel, je trouve ce genre de commentaire inutile. Vraiment..

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

est-ce par principe un nouveau langage de programmation n'a pas de très fortes chances d'être inutile?

Dans ce que ça apporte à celui qui l'écrit :

• une meilleure compréhension des concepts derrière chaque fonctionnalité du langage
• apprentissage

Ensuite, selon le but du langage de programmation, cela te permet de répondre à un besoin que tu as identifié (Domain Specific Language), ou de fournir une implémentation différente à des concepts existant (donc performances différentes, etc…).

C'est jamais inutile de faire un nouveau langage.

Mais franchement, si on veut faire quelque chose d'utile pour la communauté, il y a peut-être mieux à faire que de créer un nouveau langage de programmation.

Pour les arguments que j'ai cité ci-dessus. C'est jamais inutile.

En tout cas, je ne me lasserai jamais des ridiculités cosmétiques qui accompagnent tout projet de nouveau langage. Genre, regardez, il existait #include, using(), library(), module(), package(), \usepackage(), et bah mon nouveau langage c'est use:: pour inclure une bibliothèque. Et puis pour définir une fonction, c'est pas def truc:, ni sub truc { }, ni func truc() { }, ni int truc() { }, c'est fn truc() = { }.

C'est assez ridicule comme remarque. Ce qui est important dans un langage de programmation, c'est la facilité de réutiliser les design patterns que tu connais déjà, et la facilité que tu as pour en apprendre d'autres.

Un langage de programmation c'est avant tout représenter des algorithmes, de la logique métier et de la glue entre tout ça (à l'aide de design pattern).

La syntaxe, c'est accessoire, et au bout d'un moment cela ne devrait pas te poser problème.

Que j'écrive func, function, fun, fn, on a compris. Pareil pour #include, import, use, require, …

Discuter de la syntaxe, c'est comme discuter des goûts et des couleurs. Ça sert à rien.

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

Ce puit à toxicité qu'est Twitter, va devenir un océan de connerie.

https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

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

Alors pour reprendre ton exemple :

class message_def(v: {
  address: int,
  data: unknown,
})

class message_def_speed(v: message_def & {
  address: 0x04,
  data: float32,
})

let message_speed: message_def_speed = {
  address: 0x04,
  data: 4.2
})

Est-ce que cela répond à la problématique ?

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.

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

Tu aurais un exemple à donner ?

Parce qu'il restera possible de définir un type comme ceci :

class config(json_data: {
  debug: bool,
  loglevel: "debug" | "info" | "warn" | "error" | "critical",
  logformat: string,
})

Et ensuite de l'utiliser dans une fonction :

# lèvera une exception au runtime si la conf est pas bonne
let cfg: config = json.loadfile("/path/to/config.json")

Ce qu'il faut bien comprendre, c'est la syntaxe :

Keyword("class") Identifier LeftParen Identifier : TypeDef RightParen [LeftBracket TypeConstraintBlock RightBracket]

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

Je vois que tu as pensé à créer des types pour les litéraux. C'est une bonne idée.

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 une string. Tout les types composites sont construit à partir de littéraux, peu importe le langage.

Concrètement, cela veut dire que le type est une donnée comme une autre.

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 :

func foo(t: type) -> type {
  # n'existe pas en letlang
}

Le seul moyen de "passer un type en argument" c'est en utilisant des fonctions génériques :

func foo<T>(v: T) -> T {
  # ...
}

Mais on ne peut toujours pas manipuler T comme on manipulerait un entier ou un booléen.

tendre le concept de "constante propagation" lors de la phase d'optimisation en incluant les types structurées

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