Journal [Letlang] Et si on rédigeait la spec ?

Posté par David Delassus (site web personnel) le 06 mai 2022 à 02:12. Licence CC By‑SA.

Étiquettes :

mai

2022

Bonjour Nal,

Aujourd'hui pas de code, mais de la doc !

En effet, il est grand temps de mettre mes idées sur papier pour les générations futures.

Voici d'abord une petite table des matières de ma série d'articles sur ce projet :

La documentation, c'est bien

On dira ce qu'on veut de Python (c'est pas performant, le packaging il sens la merde, etc…), mais le choix qu'ils ont fait pour aborder la spécification du langage et de son écosystème est selon moi le meilleur qui soit :

pas de comité mystérieux qui sort une spec du 800 pages une fois tout les 5 ans (cc C++)
pas de process obscur qui refuse toute contribution et disparaît de la surface de la planète (cc Lua)

Non, à la place, on a les PEP, Python Enhancement Proposals :

chaque document décrit une fonctionnalité, un élément de syntaxe, une guideline, etc…
chaque document est indépendant des autres ("self contained" pour les intimes).
n'importe qui peut en soumettre un
le processus de discussion et de validation est clairement défini
on a une explication du "pourquoi" en plus du "comment"
on a souvent un historique des idées rejetées

Bref, c'est rempli de transparence et de bonnes intentions. Que demande le peuple ?

C'est pourquoi j'ai décidé de reprendre le concept sous forme de LEP, Letlang Enhancement Proposals (pour ceux qui vont me dire "meh ça sonne un peu comme la lèpre", je leur répondrais "trouve moi un meilleur nom et soumet une LEP par mail").

Cela me servira à mettre par écrit les différents aspects du langage, et me servira de base pour les évolutions futures. Il faut dire qu'aujourd'hui, la spec n'existe que dans ma tête et via quelques exemples de code par-ci par-là.

Je dois t'avouer que pour avancer sur l'implémentation, c'est pas top.

Au moment présent de l'heure du jour d'aujourd'hui, j'ai rédigé 4 LEPs :

LEP-001: Language Target - Défini Rust comme étant la sortie de mon compilateur
LEP-002: Import resolution - Défini le mécanisme d'import
LEP-003: Statements - Parle de "statement" vs "expression"
LEP-004: Type System - Défini le système de type du langage une bonne fois pour toute

Dans les jours qui viendront, j'ajouterai :

LEP-005: Functions - Définira la structure d'une fonction, et comment le type checking sera implémenté
LEP-006: Side Effects - Définira le mécanisme de side effect et d'exceptions
LEP-007: SAT Solver - Ça sera un draft qui parlera du système d'équation intégré au langage, je reporte donc l'implémentation de cette fonctionnalité à plus tard

Bien d'autres arriveront encore par la suite, mais au moins cela posera les bases.

Une fois ceci fait, et que le "hello world" sera compilable, je rendrais enfin le dépôt open source (quid de la licence selon toi ? j'aimerais bien vos avis sur la question).

En attendant, si tu souhaites quand même me filer un coup de pouce, tu es le bienvenu, je te donnerais un accès collaborateur au dépôt sur Github ;)

# LAP

Posté par Gil Cot ✔ (site web personnel, Mastodon) le 06 mai 2022 à 02:41. Évalué à 6.

C'est pourquoi j'ai décidé de reprendre le concept sous forme de LEP, Letlang Enhancement Proposals (pour ceux qui vont me dire "meh ça sonne un peu comme la lèpre", je leur répondrais "trouve moi un meilleur nom et soumet une LEP par mail").

Letlang Amelioration Proposals et la traduction en français est miroir et non secam hugh. Mais je soumets par ce commentaire et non par mail.

“It is seldom that liberty of any kind is lost all at once.” ― David Hume
# LEP

Posté par barmic 🦦 le 06 mai 2022 à 08:33. Évalué à 5.

Si tu cherche d'autres inspirations, tu as les JEP de Java. Historiquement java utilise des JSR (Java Specification Request) qui sont des document énormes (une centaines de pages a4) ça s'inscrivait dans un processus assez lourd avec commité. Depuis un certain temps maintenant ils utilisent des JEP. Un exemple :

https://openjdk.java.net/jeps/409

Perso j'aime bien le fait d'avoir une section goals/non-goals pour cadrer un peu.

https://linuxfr.org/users/barmic/journaux/y-en-a-marre-de-ce-gros-troll
# théorie des ensembles pas naives

Posté par Thomas Douillard le 06 mai 2022 à 09:08. Évalué à 5.

Pas encore tout lu mais dans l'intro du système de type j'ai l'impression qu'il est suggéré que RFC est soumise au paradoxe de Russel.

C'est l'inverse, a l'instar des théories des types c'est une théorie qui a été conçue pour NE PAS être soumise à des paradoxes, elle succède a des théories dites "naïves" des ensembles.

Si je ne m'abuse il n'y a pas non plus de concept de "classe propre" dans ZFC : par conception les classes propres sont exclues de la théorie qui n'en parle pas.

(Wp)

Furthermore, proper classes (collections of mathematical objects defined by a property shared by their members where the collections are too big to be sets) can only be treated indirectly. Specifically, Zermelo–Fraenkel set theory does not allow for the existence of a universal set (a set containing all sets) nor for unrestricted comprehension, thereby avoiding Russell's paradox.

Ta présentation me semble au minimum maladroite. Mais j'ai prête mal compris.
- [^] # Re: théorie des ensembles pas naives
  
  Posté par David Delassus (site web personnel) le 06 mai 2022 à 09:48. Évalué à 4.
  
  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
  - [^] # Re: théorie des ensembles pas naives
    
    Posté par PR le 08 mai 2022 à 13:36. Évalué à 3. Dernière modification le 08 mai 2022 à 13:36.
    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.
    
    Moui.
    
    This creates a strong coupling between the structure of data and the implementation of the operations manipulating such data.
    
    However, in mathematics, objects have no type. Instead, the mathematician will define a collection with rules indicating which objects are part of said collection.
    
    Franchement j’ai du mal avec ta justification sur les types. Je trouve ça casse-gueule de vouloir parler mathématiques aussi fondamentales et surtout pas très pertinent pour un système de types informatiques.
    
    De base, par exemple :
    - ℕ se définit par l’existence d’une application successeur : les naturels sont aux mathématiciens ce que les listes chainées sont aux informaticiens ; idem pour l’opérateur d’addition (appelons-le +⁰) ; les naturels sont définis à travers ces opérateurs (cf. arithmétique de Peano). Il y a couplage entre l’ensemble et les opérateurs admis sur ses éléments.
    - En ZF, de même tu as la relation d’appartenance ∈ qui est explicitement une primitive ;
    - Tout le reste est construit par-dessus, et là ta remarque a effectivement une certaine pertinence : par exemple on définit ℚ à partir de ℕ, ℝ à partir de ℚ, etc. puis on définit des opérateurs et des relations sur ces ensembles.
    Mais dire qu’il n’y a pas de “types” en mathématiques est toujours faux. C’est même à la base de toute l’algèbre générale : on parlera plutôt de structures, c’est-à-dire des ensembles munis d’opérateurs, +, ×, etc.
    
    Si tu dis ∀x ∈ ℚ tel que x = 42, ∀y ∈ ℝ tel que y = 42 : en toute rigueur x ≠ y.
    
    Il faut définir un injecteur i : ℚ → ℝ, c’est-à-dire une fonction telle que y = i(x). Cette injecteur a les bonnes propriétés pour que les opérateurs usuels définit sur ℚ collent avec les opérateurs usuels sur ℝ: ainsi i(x +¹ z) = i(x) +² i(z) où +¹ est l’addition dans ℚ et +² l’addition dans ℝ, et = est complètement défini car on compare bien un réel avec un réel (et pas des choux et des carottes). On parle de i comme d’un homomorphisme de groupes (ℚ +¹) → (ℝ +²). Et si on y adjoint les multiplications (×¹ et ×²) on parle des corps ℚ et ℝ et d’homomorphismes de corps.
    
    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.
    
    Ajoute à cela que tes opérateurs +⁰, +¹, etc. n’existent pas sur les ensembles en tant que tels. En réalité dire ∀x,y ∈ ℕ, x +⁰ y = … est un pur abus de langage. Il est admis parmi les mathématiciens qu’on parle en réalité ici de “ℕ muni de son addition usuelle…”. Pour ℚ et ℝ c’est leur structure de corps qui est implicite ; ℚ muni de +¹ et ×¹, ℝ de +² et ×². Si je mets un exposant, c’est pas pour faire joli :
    - c’est parce qu’il ne s’agit pas du même opérateur : c’est l’injecteur, parce qu’il est un homomorphisme, qui permet d’identifier +¹ à +²) ;
    - c’est parce qu’on ne peut pas mixer un rationnel et un réel pour faire une addition.
    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.
    
    Mort aux cons !
    - [^] # Re: théorie des ensembles pas naives
      
      Posté par PR le 08 mai 2022 à 13:47. Évalué à -1. Dernière modification le 08 mai 2022 à 13:49.
      
      Erratum
      
      En réalité dire ∀x,y ∈ ℕ, x +⁰ y = … est un pur abus de langage. Il est admis parmi les mathématiciens qu’on parle en réalité ici de “ℕ muni de son addition usuelle…”.
      
      C’est faux si on construit ℕ avec l’arithmétique de Peano (puisque +⁰ est une primitive).
      
      Si ℕ est construit depuis ZF, c’est en munissant un ensemble d’un +⁰ — car ce n’est pas une primitive dans ZF — entre autres, qui fait de cette ensemble qu’il correspond à ℕ.
      
      Mort aux cons !
    - [^] # Re: théorie des ensembles pas naives
      
      Posté par Thomas Douillard le 08 mai 2022 à 14:12. Évalué à 5.
      
      D’autant plus qu’on peut faire des maths pas seulement dans la théorie des ensembles, mais aussi dans la théorie des types.
      
      Les assistants de preuves comme Coq ou Lean qui a fait récemment parler de lui, cf. https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ par exemple sont basés sur des théories des types. Les théories des types sont un sujet de recherche actif du point de vue mathématique, et pas seulement pour les maths-infos mais aussi pour des choses purement mathématiques. Cf. la théorie homotopique des types dont il a déjà été question ici je crois.
      
      Si on travaille dans la théorie des ensembles un meilleur exemple pour montrer l’ambiguité serait peut être de parler de l’ensemble vide : il peut représenter assez naturellement … l’élément neutre de l’opération d’union de la théorie des ensemble, mais aussi si on code des nombres il peut coder le nombre 0 dans les entiers naturels dans la construction classique.
      
      Mathématiquement 0 et l’ensemble vide sont bien évidemment des objets totalement différents, en théorie des ensembles, si on applique les axiomes et le codage classique des entiers naturels, ils sont … égaux (deux ensemble sont égaux si ils ont les même éléments).
      
      C’est souvent un exemple d’absurdité qui est utilisé pour introduire la théorie des types aux mathématiciens qui sont habitués à travailler avec la théorie des ensembles. Le truc à noter c’est qu’en choisissant un autre codage des entiers naturels dans la théorie des ensembles le paradoxe disparait (mais d’autres pourraient apparaitre). Tout dépend de comment on choisit de coder les objets sur lesquels on veut travailler.
      
      Je pense que ce qui pourrait manquer à la présentation, également, c’est une définition de ce que sont les « objets ». Ils sont pas introduits ni définis dans la présentation actuellement. Et il semble y avoir une confusion entre « objet » et « littéral » : le littéral « 5 » peut être utilisé pour représenter l’entier naturel 5 dans le code d’un programme. L’entier naturel a naturellement un type, par contre les littéraux c’est à définir. On peut très bien convenir que dans un contexte de calcul vectoriel ou sur les flottants on donne au littéral « 5 » d’autre significations … Et soit interprétés comme deux objets (dans le sens de valeur manipulées par le langage, des valeurs que peuvent prendre les variables) différents.
      
      Dernier point sur le paradoxe de Russel : en quoi est-ce un problème en pratique ? Les classes pourraient être manipulables en tant que valeur du langage (« objet ») sans avoir la possibilité que le langage soit assez puissant pour pouvoir définir une collection de ces valeurs. Si tu veux avoir des variables « non déterministes » qui pourraient avoir comme valeur plusieurs « objet classes » possibles ça doit pouvoir rester possible en faisant attention à ce que cet ensemble de classe soit « fermé », ou alors faire en sorte que les variables qui contiennent des classes soient « déterministes » dans le sens ou il ne peuvent avoir qu’une seule valeur possible.
      - [^] # Re: théorie des ensembles pas naives
        
        Posté par Michaël (site web personnel) le 09 mai 2022 à 23:28. Évalué à 3.
        
        […] le codage classique des entiers naturels […]
        
        Je suppose que tu fais référence à la construction de Von Neumann mais il est aussi très commun de partir de l'axiome de l'infini. En bref la méthode fonctionne en énonçant l'axiome de l'infini comme suit:
        
        Il existe un ensemble X qui n'est pas l'ensemble vide et $\sigma: X \to X$
        une application injective qui n'est pas surjective.
        
        Puis on choisit un un point qui n'est pas dans l'image de $\sigma$ et on prend l'intersection de toutes les parties $\sigma$ -stables de qui contiennent , ce qui nous permet ensuite de suivre la méthode de Peano.
    - [^] # Re: théorie des ensembles pas naives
      
      Posté par David Delassus (site web personnel) le 08 mai 2022 à 21:54. Évalué à 4.
      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
      - [^] # Re: théorie des ensembles pas naives
        
        Posté par Nicolas Boulay (site web personnel) le 09 mai 2022 à 11:25. Évalué à 5.
        
        Si tu veux éviter les problèmes de la théorie des ensembles, il y a une théorie dont j'ai oublié le nom (théorie des types ?) qui a donné les "modules" d'Ocaml. Il me semble que c'est la base de coq par exemple.
        
        "La première sécurité est la liberté"
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par Thomas Douillard le 09 mai 2022 à 13:23. Évalué à 3.
        
        calcul des constructions ?
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par kantien le 09 mai 2022 à 17:30. Évalué à 3.
        
        Comme déjà dit par Thomas Douillard, c'est le calcul des constructions (une théorie des types) qui est à la base de Coq. Pour OCaml, le système de types qui s'en rapproche le plus c'est le système F de Jean-Yves Girard. Par contre, utiliser les modules OCaml pour éviter les paradoxes n'est pas un bon choix. Leo White a implémenté le paradoxe de Girard dans le système de modules de OCaml.
        
        D'une manière générale, il me semble que si la logique sous-jacente d'un système de types est non contradictoire, alors le système de calcul associé n'est pas turing complet (ce qui est, par exemple, le cas de Coq); ce qui n'est pas une propriété désirée pour un langage généraliste.
        
        Après, il y a un point que je ne comprends pas trop dans la LEP de David Delassus, lorsqu'il dit que les objets mathématiques n'ont pas de types. Pour moi les mots types et concepts mathématiques sont synonymes, donc si, les objets mathématiques ont tous un type (type qui, certes, n'est pas unique : les entiers sont des rationnels, qui sont eux-mêmes des réels, qui sont des complexes…)
        
        Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par David Delassus (site web personnel) le 09 mai 2022 à 17:48. Évalué à 2.
        
        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
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par octachron le 09 mai 2022 à 19:02. Évalué à 3. Dernière modification le 09 mai 2022 à 19:04.
        
        Le problème est que le type d'un objet, du point vue de la théorie des types, c'est une approximation (syntaxique) qui permet à travers un système de type de prouver des propriétés de programmes en temps borné.
        
        De ce point de vue de là, les objets de Letlang ont un type unique. Le système de type de Letlang permet juste de construire un type comme une union de types pré-existants. Un système de type avec un produit, une union et des constructeurs de types n'est pas très original en soi.
        
        Par contre, le manque de types sommes, récursifs ou algébriques est un choix de conception fort, et une lacune pour un système de type de mon point de vue.
        
        Et je ne suis pas vraiment sûr de savoir comment se comporte la segmentation des types des valeurs en univers. Mais c'est pour partie parce que les règles de typage des univers ne sont pas décrit.
        
        Par exemple, soit une valeur x de type t de l'univers 1, et une valeur y de type de u l'univers 2: quel est l'univers de (x,y)? À moins que (x,y) ne soit pas autorisé? Qu'en est-t-il du polymorphisme d'univers?
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par David Delassus (site web personnel) le 09 mai 2022 à 19:39. Évalué à 2.
        
        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
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par Thomas Douillard le 09 mai 2022 à 20:02. Évalué à 2.
        
        Tu peux dans ce cas probablement définir un type unique de la manière suivante : le type de ton objet est le type de l’intersection de toutes les spécification des types qu’il peut remplir.
        
        la constante 8 serait alors l’intersection des types int, even et mod4, donc de type mod4 puisque c’est un sous type strict des 2 et que even est un sous type de int.
        
        Ça signifie que 8 peut être utilisé à la fois partout ou on attend un entier, un nombre pair ou un multiple de 4.
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par David Delassus (site web personnel) le 09 mai 2022 à 20:08. Évalué à 2.
        
        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
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par Thomas Douillard le 09 mai 2022 à 20:21. Évalué à 4.
        
        Dans ce cas tu attaches bien plus d’importance aux étiquettes de type que tu veux bien le croire, vu qu’un type ne peut être un sous-type d’un autre que s’il est spécifié comme tel. Alors que si tu veux démontrer des choses, tu pourrais partir sur une vérification non nominale que toutes les valeurs d’un type respectent le prédicat de validation d’un autre sans que ce soit explicitement écrit par sous-typage explicite.
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par octachron le 09 mai 2022 à 20:19. Évalué à 3.
        
        Avec la définition usuelle de type, le type de 8 est number; et int, even, mod4 sont des refinement types de number. La distinction est potentiellement intéressant vu que le type number est facilement inférrable sans ambiguïtés tandis qu'il n'est pas souhaitable de vérifier que le type de 8 puisse être raffiné en mod4 avant d'essayer d'appliquer une fonction de type mod4 → α à 8.
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par kantien le 09 mai 2022 à 23:55. Évalué à 4. Dernière modification le 09 mai 2022 à 23:56.
        
        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?
        
        Je ne vois toujours pas en quoi ils n'ont pas de type au sens IT du terme. Un type c'est un ensemble de valeurs (comme N, Q ou R), et la notion d'ensemble au sens "naïf", telle qu'utilisée en mathématiques, est bien plus proche de celle de type que de celle d'ensemble au sens de ZFC (personnellement, je préfère de loin les théories de types comme fondements des mathématiques à ZFC).
        
        Après, ton système de classe revient à appliquer le principe de la définition par compréhension, ce qui génère des sous-types de ton type d'entrée. En OCaml, on pourrait formuler le principe général ainsi :
        
        module Comprehension (M : sig type t val prop : t -> bool end) : sig type t = private M.t val make : M.t -> t end = struct type t = M.t let make x = if M.prop x then x else failwith "make" end
        
        Le schéma de compréhension prend en entrée un type t ainsi qu'un propriété sur ce type, puis renvoie en sortie le sous-type (ou sous-ensemble) des éléments de t qui satisfont la propriété. Exemple avec le type even :
        
        module Even = Comprehension (struct type t = int let prop x = x mod 2 = 0 end) let deux = Even.make 2;; val deux : Even.t = 2 (* ici `deux` est considéré comme de type `Event.t` et non comme `int` *) deux + 3;; Line 1, characters 0-4: Error: This expression has type Even.t but an expression was expected of type int (* mais on peut aussi le caster vers un `int` *) (deux :> int) + 3;; - : int = 5
        
        Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par David Delassus (site web personnel) le 10 mai 2022 à 00:09. Évalué à 2.
        
        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
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par kantien le 10 mai 2022 à 00:54. Évalué à 3. Dernière modification le 10 mai 2022 à 00:54.
        
        Dans ton exemple, OCaml croit que l'on ne peut pas additionner des nombres pairs, ce qui est complètement faux.
        
        Non, il demande simplement à être explicite sur le type que je donne à une valeur dans chaque contexte. Autrement dit, quand il voit la valeur deux, il demande au programmeur : la considères tu comme un entier pair ou simplement comme un entier ?
        
        Sinon, je m'arrête là, il y a certaines notions qui semble t'échapper au sein de la théorie des types et des mathématiques en générale.
        
        Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par David Delassus (site web personnel) le 10 mai 2022 à 01:03. Évalué à 3.
        
        Autrement dit, quand il voit la valeur deux, il demande au programmeur : la considères tu comme un entier pair ou simplement comme un entier ?
        
        Peu importe, on est censé pouvoir additionner les deux.
        
        Sinon, je m'arrête là, il y a certaines notions qui semble t'échapper au sein de la théorie des types et des mathématiques en générale.
        
        Bonjour la condescendance. De une je n'ai jamais prétendu être un expert, de deux je présente un système de type inspiré de la théorie des ensembles, et non inspiré d'une quelconque théorie des types (car il y en a plusieurs).
        
        Je suis franchement étonné du nombre "d'expert" qui est venu critiquer une explication vulgarisée et simplifiée pour un public non matheux qui ne sert que d'introduction à un système de type, dont apparemment personne n'a lu la spec correctement car chacun pose des questions qui sont répondues dans cette même spec, et d'autres choisissent simplement d'ignorer le concept que je veux implémenter sous prétexte que la partie "math" n'est pas rigoureuse (c'était pas le but de faire un cours magistral).
        
        Non effectivement, j'ai pas envie de débattre avec ce genre de personne, alors remonte dans ta tour d'ivoire, et regarde moi de haut si ça te fait plaisir.
        
        https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par kantien le 13 mai 2022 à 11:32. Évalué à 4.
        
        Peu importe, on est censé pouvoir additionner les deux.
        
        Mais, on le peut ! Il est tout à fait possible d'ajouter des nombres pairs et des nombres impairs, en les considérant en tant que int. C'est juste qu'il y une annotation explicite de typage pour dire cela au type checker; mais la valeur deux de mon exemple précédent est bien à la fois de type Event.t et de type int.
        
        Ce que tu fais, c'est du sous-typage : c'est le cœur de la logique des classes d'Aristote. J'en avais parlé lors d'une dépêche sur OCaml pour expliquer la distinction entre héritage et sous-typage, et la différence fondamentale entre le système objets d'OCaml et celui de Java (par exemple).
        
        Il n'y pas que les objets mathématiques qui ont plusieurs types, tous les êtres sont ainsi. Par exemple, Socrate est un homme mais c'est aussi un animal, un philosophe grec… Si tu sais que tous les animaux sont mortels et que Socrate est un homme, pour pouvoir appliquer le premier principe à Socrate (et conclure qu'il est mortel), il faut justifier du fait que c'est un animal, ce que tu peux faire si tu sais que les hommes sont des animaux.
        
        Tous les animaux sont mortels
        
        Tous les hommes sont des animaux
        
        or Socrate est un homme
        
        donc Socrate est un animal
        
        donc Socrate est mortel
        
        La hiérarchie entre les concepts mortel, animal, homme : c'est ça le sous-typage. En OCaml, lorsque j'écris ceci :
        
        type t = private M.t
        
        j'affirme au type-checker que tous les t sont des M.t ou, de manière équivalente, que t est un sous-type de M.t. Ainsi par application du principe de définition par compréhension, on obtient que tous les Event.t sont des int. Après quand je veux appliquer la fonction +, dont le type est int -> int -> int, avec parmi les paramètres la valeur deux : Event.t, il se passe deux choses. Dans un premier temps, je ne dis pas au type checker que je veux oublier la parité de deux, alors il se plaint, les deux types int et Event.t étant distincts (tous les entiers ne sont pas pairs). Par contre si je lui dis que je veux oublier sa parité et le voir comme un int en écrivant deux :> int, il valide le tout car il sait que les Event.t sont des int et que donc deux est bien aussi un int.
        
        Cela étant, je tiens à signaler que tout ceci est réalisé statiquement (le code non annoté refuserai de compiler), ce qui n'est pas le cas de LetLang d'après tes specs. La différence étant que les cast doivent être explicites en OCaml.
        
        Après, il y a un point non abordé dans ta spec : quid des listes de even ? Sont-elles des listes de number ? Si c'est le cas, il te faudra aborder la notion de variance (invariance, covariance et contravariance) des types paramétriques. Exemple en OCaml :
        
        (* une fonction qui somme une liste de `int` *) let sum l = List.fold_left (+) 0 l;; val sum : int list -> int = <fun> (* la somme des 3 premiers `int` *) sum [1; 2; 3];; - : int = 6 (* elle somme aussi les listes de `Event.t`, le type list étant covariant *) sum ([deux; deux] :> int list);; - : int = 4
        
        Je ne suis pas sûr que tu te sois posé la question, car d'après ta spec sur les fonctions, on peut lire :
        
        NB: The class func[arguments -> return] contains every function with the same signature.
        
        Pourtant les types des fonctions -> est contravariant sur son entrée (arguments) et covariant sur sa sortie (return). Ainsi la classe func[number -> number] devrait aussi contenir les fonctions avec cette signature func[number -> int] (si on retourne un int, on retourne aussi, a fortiori, un number).
        
        let foo (f : int -> int) x = f x;; val foo : (int -> int) -> int -> int = <fun> (* je peux appliquer `foo` a une fonction de type `int -> Event.t` *) let bar (f : int -> Even.t) = foo (f :> int -> int);; val bar : (int -> Even.t) -> int -> int = <fun>
        
        Bonjour la condescendance. De une je n'ai jamais prétendu être un expert, de deux je présente un système de type inspiré de la théorie des ensembles, et non inspiré d'une quelconque théorie des types (car il y en a plusieurs).
        
        Ce n'était pas de la condescendance, juste un peu d'agacement de ma part au ton perçu (peut-être à tort) de ton message. Et j'avais lu ta spec : tu t'inspires de l'approche de Russel et Whitehead dans leur principia mathamtica. Je voulais juste signaler que la proposition selon laquelle les objets mathématiques n'avaient pas de type été fausse (au sens IT ou non du terme, sens qui reste somme toute assez flou). Tu prends le partie de la compréhension sur celui de l'extension en ce qui concerne un concept. Un concept pouvant être envisagé de deux points de vue : celui de la compréhension (les conditions sous lesquelles un objet tombe sous un concept, ce qui en constitue sa définition) ou celui de son extension (la totalité des choses qui tombent sous ce concept, ce qui en fait une collection, un ensemble de choses). Tu prends le partie de la compréhension est en fait un fonction qui retourne un booléen, fonction qui ne sera appliquée qu'à l'exécution.
        
        Cela étant, il y a un point qui m'intrigue dans ta spec. Tu prétends avoir rejeté l'idée d'un classe object qui contiendrait toutes les valeurs du langage, parce que cela irait à l'encontre de la hiérarchie des set. Mais qu'en est-il de cette classe que je semble pouvoir définir ?
        
        class object (v : !even | even)
        
        De ce que je comprends, sa fonction de compréhension vaut true pour toutes valeurs du langage, et donc l'extension de cette classe contiendrait bien toutes les valeurs.
        
        Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par David Delassus (site web personnel) le 13 mai 2022 à 12:56. Évalué à 2.
        
        Il est tout à fait possible d'ajouter des nombres pairs et des nombres impairs, en les considérant en tant que int. C'est juste qu'il y une annotation explicite de typage pour dire cela au type checker; mais la valeur deux de mon exemple précédent est bien à la fois de type Event.t et de type int.
        
        C'est justement ça que je trouve dommage, devoir explicitement le dire, alors qu'il est possible de le déterminer implicitement.
        
        Cela étant, je tiens à signaler que tout ceci est réalisé statiquement (le code non annoté refuserai de compiler), ce qui n'est pas le cas de LetLang d'après tes specs. La différence étant que les cast doivent être explicites en OCaml.
        
        Yes, pour l'instant je fais au runtime, c'est plus simple. Mais à terme, j'imagine très bien de l'analyse statique de code avant la compilation pour appliquer ce type-check "implicite".
        
        Après, il y a un point non abordé dans ta spec : quid des listes de even ? Sont-elles des listes de number ? Si c'est le cas, il te faudra aborder la notion de variance (invariance, covariance et contravariance) des types paramétriques.
        
        Oui, et une LEP dédiée s'attaquera à ces notions.
        
        Je ne suis pas sûr que tu te sois posé la question, car d'après ta spec sur les fonctions, on peut lire :
        
        NB: The class func[arguments -> return] contains every function with the same signature.'
        
        Pourtant les types des fonctions -> est contravariant sur son entrée (arguments) et covariant sur sa sortie (return). Ainsi la classe func[number -> number] devrait aussi contenir les fonctions avec cette signature funcnumber -> int.
        
        Problème de formulation, j'aurais du dire "with a compatible signature" à la place. Mais je me suis bien posé la question.
        
        tu t'inspires de l'approche de Russel et Whitehead dans leur principia mathematica.
        
        Totalement, j'ai les 3 volumes à la maison. Et quelques autres ouvrages qui traitent de théorie des ensembles, des types et catégories.
        
        Cela étant, il y a un point qui m'intrigue dans ta spec. Tu prétends avoir rejeté l'idée d'un classe object qui contiendrait toutes les valeurs du langage, parce que cela irait à l'encontre de la hiérarchie des set. Mais qu'en est-il de cette classe que je semble pouvoir définir ?
        
        class object (v : !even | even)
        
        De ce que je comprends, sa fonction de compréhension vaut true pour toutes valeurs du langage, et donc l'extension de cette classe contiendrait bien toutes les valeurs.
        
        AAAAAAAAAAAAAAH…. merci. Il va falloir que j'ajoute à ma TODO d'interdire ce genre de définition (il me semble que des outils comme coq pourrait m'aider à implémenter cette fonctionnalité).
        
        Au passage :
        
        class never(v: !number & number);
        
        https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par Nicolas Boulay (site web personnel) le 13 mai 2022 à 14:55. Évalué à 3.
        
        Comme dis plus haut, le "non" permet tout un tas de truc bizarre. Commencer à interdire des "a | !a" risque d'aller trés loin dans la complexité.
        
        La théorie que je cherchais était celle des catégories, qui pose normalement moins de soucis que la théorie des ensembles.
        
        "La première sécurité est la liberté"
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par Thomas Douillard le 15 mai 2022 à 10:11. Évalué à 3.
        
        Ça ne pose pas de problème pour les classes au sens mathématique du terme, il me semble. Le principe c’est justement qu’on peut utiliser n’importe quel prédicat sur une classe propre ?
        
        Le truc pour ne pas avoir de paradoxe en théorie des ensembles c’est que tu ne peux pas statuer de « l’appartenance » d’une classe propre à une autre classe propre, et a fortiori à un ensemble. Si tu ne fais jamais ce genre de truc j’avoue que je vois pas trop en quoi il y aurait un problème à avoir n’importe quel prédicat. C’est juste que si ça laisse tout passer il y a des chances qu’une fonction avec un paramètre d’un tel type ne peut pas supposer grand chose.
        
        https://fr.wikipedia.org/wiki/Classe_(math%C3%A9matiques)
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par Nicolas Boulay (site web personnel) le 15 mai 2022 à 15:12. Évalué à 3.
        
        J'ai tenté de faire un logiciel de schema yaml "par l'exemple." (Coherentyaml)
        
        Si a est une feuille, "a & b" est vrai si les 2 sont de même type. "Non a" veut dire "Non(a&b)", ce qui est sans doute l'origine de mon soucis.
        
        Si a==b, cela devrait toujours etre vrai :
        // ((A -> B) & ~B) -> ~A
        Avec // (a -> b) = (~a or b)
        
        "La première sécurité est la liberté"
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par kantien le 17 mai 2022 à 00:02. Évalué à 6. Dernière modification le 17 mai 2022 à 00:04.
        
        AAAAAAAAAAAAAAH…. merci. Il va falloir que j'ajoute à ma TODO d'interdire ce genre de définition (il me semble que des outils comme coq pourrait m'aider à implémenter cette fonctionnalité).
        
        Je ne suis pas certain qu'il soit nécessaire d'interdire ce genre de définition. Dans ton langage, comme tu peux raffiner un type à l'exécution, le type object c'est juste le interface {} du Go. Tu perds toute information de typage, mais ce n'est pas en soit dangereux, juste peut utile du point de vue typage. Et si on ne peut pas raffiner le type, c'est juste un singleton (même s'il semble contenir plus de valeurs en apparence) : voir cette discussion sur le forum OCaml.
        
        Après, d'une manière générale, comme te l'a fait remarquer Octachron, tu ne précises rien sur la hiérarchie des univers : si even et !even était dans le même univers, le type even | !even ne contiendrait pas toutes les valeurs.
        
        Enfin, avoir une contradiction dans le système de types (vu comme une logique) n'est pas si grave si tu ne cherches pas à implémenter un assistant de preuves. Dès que tu as de la récursion générale, c'est inévitable.
        
        let rec f x = f x;; val f : 'a -> 'b = <fun> (* l'équivalent de ton type `never` *) type never = | (* et pourtant il n'est pas vide, un calcul qui ne termine pas peut recevoir ce type *) let _ : never = f () (* ou encore avec une exception *) let _ : never = failwith "faux"
        
        Plus d'infos sur cette présentation de la correspondance de Curry-Howard.
        
        Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par Gil Cot ✔ (site web personnel, Mastodon) le 10 mai 2022 à 07:05. Évalué à 7.
        
        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.
        
        Je crois que ce que kantien tente de te dire, c'est qu'en restant sur l'aspect purement mathématique (vu que le sujet t'intéresse), ce que tu appelles « collection » forme un type ou « ensemble de valeurs »
        L'opposition « type au sens IT » ne fait pas sens pour tout le monde… parce-que d'une part IT est un peu vague et surtout d'autre part ne recouvre pas les expériences de tout le monde. Or kantien a une autre expérience des langages (à la lecture il ne fait pas que du OCaml mais aussi fort vraisemblablement des langages de preuve et de spécification formelle ?) bien différente de la tienne.
        
        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.
        
        Voilà, le type en C n'est pas le type en OCaml ni le type en Prolog ni le type en Lisp ni…
        Pour des langages comme C/C++/Python/Java la notion de type est plutôt loin de la définition mathématique des ensembles (malgré le parallèle en surface) car ce qui est appelé type est plutôt pour la représentation en mémoire… Un langage pour lequel on doit se préoccuper de savoir comment on interprète chaque octet (int/byte/float/char/whatever) a un typeof alors que d'autres langages s'en foutent (ou du moins c'est transparent pour les usagers.)
        
        Dans ton exemple, OCaml croit que l'on ne peut pas additionner des nombres pairs, ce qui est complètement faux.
        
        C'est juste que l'exemple choisi fait lever une alerte (ce n'est pas une erreur ou une impossibilité) sur une ambiguïté : doit-on considère qu'on reste en nombres pairs (et donc si pour une raison quelconque on se retrouve avec des trucs impaires ça passe pas) ou doit-on juste voir que ce sont des entiers après tout (et donc il n'y a pas de problème si on se retrouve avec des impaires.) Ce genre de comportement n'est pas lié aux typeof stricto-sensus mais au fait que ces langages se veulent un peu contraint (c'est le cas aussi en Ada, parce-que tu peux avoir défini un ensemble comme des pointures de chaussure et l'autre comme des nombres de paire de chaussures, donc on peut additionner mais le compilo craint d'additionner des choux et des carottes là où justement C n'y aurait vu que du feu.)
        
        “It is seldom that liberty of any kind is lost all at once.” ― David Hume
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par barmic 🦦 le 10 mai 2022 à 09:43. Évalué à 4.
        
        Dans ton exemple, OCaml croit que l'on ne peut pas additionner des nombres pairs, ce qui est complètement faux.
        
        Ce n'est pas du tout une remise en cause. La partie conceptuelle m'intéresse mais uniquement comme lecteur. Comment en letlang on distingue qu'on a le droit d'additionner des nombre paire avec des nombres impaires, mais pas des carottes avec des minutes ?
        
        https://linuxfr.org/users/barmic/journaux/y-en-a-marre-de-ce-gros-troll
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par Thomas Douillard le 10 mai 2022 à 09:46. Évalué à 3.
        
        Et aussi, si on étend, comment on considère que c’est OK d’additionner des nombres complexes avec des flottants ?
    - [^] # Re: théorie des ensembles pas naives
      
      Posté par Anthony Jaguenaud le 09 mai 2022 à 10:33. Évalué à 1.
      
      Il y a deux trois trucs qui me gène.
      
      Se sont des ensembles, donc si tu as un ensemble de bonbon. Et un ensemble de nouriture au chocolat, un bonbon au chocolat sera dans les deux ensembles. C’est l’intersection.
      
      Quand tu dis :
      
      Si tu dis ∀x ∈ ℚ tel que x = 42, ∀y ∈ ℝ tel que y = 42 : en toute rigueur x ≠ y.
      
      Non, en toute rigueur, x = y. En informatique, x ≠ y parce qu’ils n’ont pas le même type, mais pas en math. Tous les éléments de ℕ sont dans ℤ, tous les éléments de ℤ sont dans ℚ, tous les éléments de ℚ sont dans ℝ, mais se sont bien les mêmes éléments.
      
      Autre chose :
      
      par exemple on définit ℚ à partir de ℕ, ℝ à partir de ℚ
      
      Bah non, plus. ℚ est défini à partir de ℤ. ℝ n’est pas défini à partir de ℚ, mais parce que certaines solutions à des équations n’ont pas de solutions de ℚ. Ex : x² = 2.
      - [^] # Re: théorie des ensembles pas naives
        
        Posté par rewind (Mastodon) le 09 mai 2022 à 11:08. Évalué à 4.
        
        ℝ n’est pas défini à partir de ℚ
        
        Si, ℝ est défini traditionnellement comme étant l'ensemble des limites des suites de Cauchy dans ℚ.
      - [^] # Re: théorie des ensembles pas naives
        
        Posté par Thomas Douillard le 09 mai 2022 à 11:47. Évalué à 4.
        
        Si tu ne mets que les polynômes tu ne retrouves pas ton compte mais juste les Nombre_algébrique. Les nombres algébriques sont dénombrables, il existe un algorithme infini qui peut lister tous les polynomes, et chaque polynome a un nombre fini de solutions. Du coup comme on sait par l’Argument_de_la_diagonale_de_Cantor que les nombres réels ne le sont pas, dénombrables, on a pas assez de solutions polynomiales pour avoir tous les réels.
        
        Les réels sont encore plus grands, on les trouve soit avec des coupures de Dedekin, c’est à dire l’ensemble des manières de découper les rationnels en deux partitions telles que tous les éléments d’une partition sont inférieurs à tous les autres, soit avec des suite de Cauchy, comme des limites de suites de rationnels qui convergent vers un truc. Ce truc étant un nombre réel.
      - [^] # Re: théorie des ensembles pas naives
        
        Posté par PR le 09 mai 2022 à 11:51. Évalué à -3. Dernière modification le 09 mai 2022 à 11:51.
        
        https://www.youtube.com/watch?v=-4iFWhzU230
        https://en.wikipedia.org/wiki/Embedding
        https://en.wikipedia.org/wiki/Construction_of_the_real_numbers
        
        Mort aux cons !
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par David Delassus (site web personnel) le 09 mai 2022 à 16:02. Évalué à 2.
        
        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
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par Thomas Douillard le 09 mai 2022 à 16:21. Évalué à 3.
        
        Et ça se passe comment si tu veux faire concrètement des calculs sur les variables entières ?
        
        Genre la division entière, tu comptes t’y prendre comment ? Les opérandes sont des entiers et ça retourne un entier ou des nombres quelconques et tu dois garantir d’une manière ou d’une autre que le prédicat « frac(n) = 0 » est vrai ?
        
        Sinon partie terminologique, tu parle de « part of the class », traditionnellement une partie c’est pas du tout un élément d’un ensemble mais un sous-ensemble, si tu veux être sur la théorie des ensembles. ça porte à confusion.
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par David Delassus (site web personnel) le 09 mai 2022 à 16:39. Évalué à 2. Dernière modification le 09 mai 2022 à 16:41.
        
        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
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par Thomas Douillard le 09 mai 2022 à 16:43. Évalué à 2.
        
        C’était pas ma question, c’était surtout, dans le cas a // b comment tu garantis que a et b sont bien des entiers ?
        
        A priori si tu définis simplement le fait d’être un entier par un prédicat sur le fait d’être un nombre, n’importe quel nombre pourrait être candidat à une division euclidienne. Le truc pour que ça marche c’est que tu dois être capable de garantir que ce nombre respecte bien ce prédicat ?
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par David Delassus (site web personnel) le 09 mai 2022 à 17:02. Évalué à 2. Dernière modification le 09 mai 2022 à 17:03.
        
        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
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par Thomas Douillard le 09 mai 2022 à 19:11. Évalué à 3.
        
        C’est un système de typage nominal alors finalement. Le type est déterminé par le fait que tu ait fait passer la valeur par un constructeur du type, du coup tu peux lui coller l’étiquette « entier ». Si tu as une valeur de type nombre dont il serait possible avec un démonstrateur qu’elle est nécessairement un entier, elle ne sera pas déterminée comme tel comme ça pourrait l’être avec un système structurel de type (le type n’est pas donné par une étiquette de type mais par la forme/les propriétés de l’objet, cf. Système_structurel_de_types ). C’est quelque chose qui est assez classique en typage finalement, un constructeur d’un type apporte une preuve que certaines propriétés du type sont bien garanties. Un constructeur d’un type « liste triée » par exemple pourrait appliquer un tri sur une liste non triée en garantissant que le résultat est bien trié, et la propriété est garantie dans le système de type parce que la liste a bien le type « liste triée », qui permet de tracer la propriété finalement.
        
        Tu dois avoir des « constructeurs » qui garantissent qu’une valeur de ton type a bien les bonnes propriétés. Et « int » ici c’est un sous-type de nombre dans le sens ou tu peux mettre un « int » dans n’importe quel contexte ou tu peux mettre un nombre, avec une relation de sous-typage qui est explicitement spécifiée. cf. Principe de substitution de Liskov.
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par David Delassus (site web personnel) le 09 mai 2022 à 19:36. Évalué à 2.
        
        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
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par Thomas Douillard le 09 mai 2022 à 19:54. Évalué à 2.
        
        Mais ce n’est valable que sur les constantes non ?
        
        Si tu as des fonctions style :
        
        func f(four: mod4) -> { … } func plop(a : int) -> int { b : int = 8 * a f(b) }
        
        ça typecheck ou tu comptes vérifier ça à l’exécution ?
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par David Delassus (site web personnel) le 09 mai 2022 à 20:04. Évalué à 2.
        
        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
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par Thomas Douillard le 09 mai 2022 à 20:15. Évalué à 2.
        
        Ton assert est donc totalement synonyme d’un truc style
        
        class six(a: int) { n=6 }
        
        a : six = add_five(1) ;
        
        Ça amène a une question : tu typecheck dans ton document uniquement les paramètre des fonctions. En principe on vérifie que toutes les instructions typecheckent ?
        
        [^] # Re: théorie des ensembles pas naives
        
        Posté par David Delassus (site web personnel) le 09 mai 2022 à 20:23. Évalué à 2.
        
        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
- [^] # Re: théorie des ensembles pas naives
  
  Posté par David Delassus (site web personnel) le 06 mai 2022 à 14:34. Évalué à 3.
  
  C'est corrigé :)
  
  https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
# Une grammaire ?

Posté par rewind (Mastodon) le 07 mai 2022 à 09:20. Évalué à 4.

Je suis déçu, je pensais qu'on allait voir une grammaire du langage. Mais non, pas encore. Mais ça serait bien de définir une grammaire (ou du moins des morceaux de grammaires) pour qu'on se fasse une idée plus précise du langage autrement qu'avec des exemples. Une spécification, ça doit être assez formel et les grammaires sont le bon outil pour un langage (même si ça ne suffit).
- [^] # Re: Une grammaire ?
  
  Posté par David Delassus (site web personnel) le 07 mai 2022 à 10:54. Évalué à 2.
  
  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
  - [^] # Re: Une grammaire ?
    
    Posté par Gil Cot ✔ (site web personnel, Mastodon) le 09 mai 2022 à 01:10. Évalué à 2.
    
    /me vote for BNF…
    
    “It is seldom that liberty of any kind is lost all at once.” ― David Hume
# Permettre d'envoyer les retours sans être contributeur

Posté par Neozahikel le 10 mai 2022 à 23:27. Évalué à 2.

Lors de ma lecture de la première LEP une faute de conjugaison m'a sauté aux yeux et j'ai tâché de voir comment t'en faire part. J'ai cliqué sur le lien github qui m'a renvoyé une page 404 (je suppose au vu de ce que tu écris dans le commentaire qu'il faut un accès collaborateur pour le voir?). Du coup je n'ai pas pu faire part de ma remarque ni créer une "issue". Je me rabat donc sur les commentaires de ton journal:

LEP-001:
it was choosen -> it was chosen

Rien de plus constructif à rajouter, si ce n'est que je valide totalement la démarche.
- [^] # Re: Permettre d'envoyer les retours sans être contributeur
  
  Posté par David Delassus (site web personnel) le 10 mai 2022 à 23:31. Évalué à 2.
  
  Oui effectivement, j'aimerais bien pouvoir ouvrir au moins les issues, mais tant que le hello world est pas exécutable et que j'ai pas choisi la licence, ca restera avec accès collaborateur.
  
  Merci pour le feedback, je vais corriger ça au plus vite :)
  
  https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg

Suivre le flux des commentaires

Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.