Sommaire
Bonjour Nal,
Cela faisait longtemps que je ne t'avais pas écrit, mais je n'avais pas grand chose de pertinent à dire, tu me pardonneras j'espère.
Aujourd'hui, je vais te parler d'un de mes "side-project", j'ai nommé Letlang.
Si tu as la flemme de tout lire, tu peux aller mettre en favoris le site web https://letlang.dev pour une lecture du soir.
DISCLAIMER: Très peu de code existe pour l'instant, le projet en est à ses balbutiements. Même le design de la syntaxe et fonctionnalités ne sont pas définitifs.
Un peu de contexte
Au cours de ma carrière, j'ai pu toucher à de nombreux langages de programmation, et je me suis spécialisés dans certains. Je regarde aussi les petits nouveaux qui génèrent de l'engouement, ou les propositions d'améliorations de langage existant (coucou TC39, un jour je comprendrais ton nom, promis).
Pour chacun de ces langages, j'ai une liste de choses qui me déplaisent et une liste de choses que j'adore. J'en suis venu à me poser la question suivante:
A quoi ressemblerait mon langage idéal ? Celui dont la liste de choses qui me déplaisent n'existerait pas.
Un papier, un crayon plus tard, je commençait à décrire Letlang.
Quelques amuse-gueules
Tout d'abord, il s'agit d'un langage de programmation fonctionnelle, paradigme dont je suis tombé éperdument amoureux. Le compilateur est implémenté en Rust.
Il s'inspire de Elixir (mon petit favori), Python, Rust, Go (et pourtant je déteste ce langage), TypeScript et des mathématiques.
Système de type
Letlang a ce que j'appelle un typage strict (j'aime pas la notion de fort/faible) :
On vérifie la cohérence des types le plus souvent possible, à la compilation comme à l'exécution
Cependant, à la différence de la plupart des langages de programmation, une valeur n'a pas un unique type. Au contraire, je m'inspire ici des mathématiques :
-
42
est un entier mais aussi un réel -
(1; 2)
est un vecteur 2D mais aussi une matrice 2x1
De la même manière, en Letlang, c'est la définition d'un type qui détermine si une valeur lui appartient. Ainsi, je peux écrire :
class int(n: number) check {
frac(n) = 0
}
Ici je défini un type int
qui est construit à partir d'un number
nommé n
. Je lui rajoute un prédicat que tout n
lui appartenant doit valider, ici: la partie décimale du nombre doit être 0.
Les prédicats sont une logique d'ordre supérieur (Higher Order Logic), je peux ainsi définir le type suivant :
class even(n: int) check {
thereis k: int, n = 2 * k
}
Le prédicat dit qu'il existe un entier tel que n = 2 * k
, qui est la définition mathématique d'un nombre pair. Ainsi 42
appartient aux types number
, int
et even
, alors que 43
appartient uniquement aux types number
et int
.
On peut également combiner plusieurs types en un seul avec les opérateurs |
, &
et !
:
class odd(n: int & !even)
Par définition, un nombre impair est un entier qui n'est pas pair.
Pour terminer sur le système de type, on a les types génériques :
class ok<T>(val: (:ok, T))
class err<E>(val: (:error, E))
class result<T, E>(val: ok<T> | err<E>)
Les paramètres d'un type générique peuvent être contraint à un autre type :
class vector2<T: int | float>(xy: (T, T))
Dans l'exemple ci-dessus, vector2<int>
et vector2<float>
existent, mais vector2<string>
génèrera une erreur de compilation.
Null et undefined
En Letlang, une variable peut ne pas avoir de valeur définie, mais la valeur null
ou undefined
n'existe pas.
C'est particulièrement utile pour travailler avec des équations :
let x: int # x n'a pas de valeur, mais cela sera un entier
let x > 0 # toujours pas de valeur, mais elle est positive
x - 3 = 0 # cette équation possède une solution, donc l'expression retournera true
1 / x = 0 # aucune solution n'existe pour cette équation, donc l'expression retournera false
NB:
=
est un opérateur de comparaison,==
dans la plupart des langages. L'opérateur d'assignation est:=
.
De la même manière, on pourra définir la valeur de x
grâce au mot clé let
:
let x: int # x n'a pas de valeur
let x - 3 = 0 # une seule solution existe, x = 3
Attention avec cette notation cependant:
let x: number
let 1 / x = 0 # produira une erreur, car aucune solution n'existe.
Pour résumer :
- le mot clé
let
est une assertion de la part du développeur au compilateur/runtime - les variables sans valeur définie peuvent être utilisées dans des comparaisons
- une variable est définie si on lui assigne une valeur avec
:=
ou si l'ensemble des définitionslet
produit une unique solution
Coroutines et Streams
En Letlang, comme en Go, les fonctions n'ont pas de couleur.
N'importe quelle fonction peut être exécuté en parallèle :
- le mot clé
coro
transforme un appel de fonction en coroutine - le mot clé
join
permet d'attendre la fin d'une coroutine et d'en récupérer le résultat
Un exemple vaut 1000 mots :
import stdlib as std
func main(args: list<string>) -> :ok {
c := coro std.strlen("foo")
# do other stuff
let 3 = join c
:ok
}
Les streams sont des objets qui permettent de communiquer avec des coroutines :
- envoyer une valeur dans un stream est instantané
- lire une valeur depuis un stream est bloquant tant que le stream est vide
let s: stream<int>
let v: int
# écrit dans le stream
s << 42
# lit depuis le stream et place le résultat dans la variable v
s >> v
Ce qui peut donner par exemple :
func double(s: stream<int>) -> :ok {
let x: int
s >> x
match x {
-1 => :ok,
_ => {
s << (x * 2)
double(s)
}
}
}
func main(args: list<string>) -> :ok {
let s: stream<int>
c := coro double(s)
s << 1 << 2 << 3 << 4 << -1
let :ok = join c
let (a, b, c, d): (int, int, int, int)
s >> a >> b >> c >> d
let a = 2
let b = 4
let c = 6
let d = 8
:ok
}
Effets de bord et exceptions
Faire un langage fonctionnel pur c'est bien, mais les effets de bords c'est quand même bien pratique parfois.
Une fonction pure c'est une fonction qui, comme en math, retourne toujours le même résultat étant donné les mêmes paramètres. Si f(x) = x + 1
, alors f(1)
donnera toujours 2
.
Les fonctions du style readline()
ou get_time()
retourneront des résultats différents, ce sont donc des fonctions impures.
En Letlang, ce n'est pas possible de créer de telles fonctions. A la place, on va utiliser les effets. Un effet se déclare comme une signature de fonction :
effect log(level: "debug" | "info", message: string) -> :ok
On peut ensuite appeler cet effet grâce au mot clé perform
:
let :ok = perform log("info", "hello world")
Cela permet de déléguer la gestion de l'effet à celui qui appelle le code l'utilisant, cela avec la structure de contrôle do {}
:
let :ok = do {
perform log("info", "hello world")
}
effect log("debug", _message) {
:ok
}
effect log("info", message) {
std.print(message)
:ok
}
Si un effet n'est pas géré par une clause effect
, alors il sera propagé jusqu'au runtime de Letlang. Si le runtime ne connait pas l'effet en question, le programme plantera.
Ainsi, le runtime Letlang fournit un ensemble d'effets "builtin" sur lesquels le développeur pourra se reposer pour interagir avec le monde extérieur.
Ensuite, les exceptions sont un cas particulier d'effet : elles ne rendent pas le contrôle au code qui les appelle.
C'est un mécanisme de retour prématuré :
let :oops = do {
throw :error
:never_reached
}
catch :error {
:oops
}
Ensembles infinis
Allez, un dernier pour la route. Letlang peut travailler avec des ensembles infinis, ils sont construit à l'aide d'une variable et d'un prédicat :
s := { x: int | x > 0 }
42 in s # true
-1 in s # false
Ici, le type de s
est donc set<int>
. C'est important à cause du paradoxe de Russel.
Imaginons 2 secondes que le type set<any>
existe (ce qui n'est pas le cas car any
n'existe pas).
On pourrait écrire :
s := { x: set<set<any>> | x not in x }
Soit : L'ensemble de tout les ensembles qui ne se contiennent pas eux même.
Posons nous la question suivante : est-ce que s
appartient à s
?
- si oui, alors le prédicat
x not in x
est faux, donc non en fait - si non, alors le prédicat
x not in x
est vrai, donc oui en fait
Le simple fait que any
n'existe pas nous empêche de créer de tels ensembles. Ouf.
Bravo
Pour ceux qui ont tout lu jusqu'ici, voici une petite récompense :
# Side project
Posté par Serge Julien . Évalué à 10.
Alors tout d'abord bonne année à toi (et aux personnes qui lisent ce commentaire)!
Tu décris ça comme un "side project", je suis plutôt impressionné. Le langage a des caractéristiques intéressantes et originales. À défaut d'avoir les compétences pour collaborer, je vais suivre ton actu là-dessus.
Je souhaite beaucoup de succès à ce projet/langage, succès qui dépendra probablement de la disponibilité d'une collection de modules standard (je pense à Python qui est fourni "batteries included").
Encore bravo!
[^] # Re: Side project
Posté par David Delassus (site web personnel) . Évalué à 5.
Bonne année aussi à toi ! :)
Rien d'impressionnant pour l'instant, au niveau du code j'ai l'AST, et j'ai commencé à écrire le validateur sémantique. Même pas encore de parseur à l'heure actuelle (je compte faire ça avec la librairie pest).
Le plus abouti dans le projet, c'est le design de la syntaxe et des fonctionnalités.
J'avoue également manquer de compétences sur l'implémentation de certains aspects du langage, c'est l'occasion d'apprendre :)
Pour moi, ce sera un succès le jour ou j'arrive à compiler un programme écrit en Letlang ^
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
# Intéressant
Posté par Anthony Jaguenaud . Évalué à 7. Dernière modification le 06 janvier 2022 à 09:25.
Salut, je trouve certaines idées intéressante, mais il y a un point que je voudrais comprendre :
En quoi est-ce différent du système de haskell, dont les classes de type permet de résoudre élégamment se problème ?
[^] # Re: Intéressant
Posté par Anthony Jaguenaud . Évalué à 4.
Une question sur l’aspect équation…
Quand on ajoute une contrainte, est-elle testé à la compilation ? L’équation est-elle résolu ou utilisée lors de l’affectation pour vérifier les contraintes ?
Un code comme ci-dessous va-t-il détecter l’erreur à la compilation ou à l’exécution ?
Voilà pour mes interrogations actuelles ;-)
[^] # Re: Intéressant
Posté par David Delassus (site web personnel) . Évalué à 3.
C'est également similaire au système de type de TypeScript ou toute forme de pattern matching structurelle que l'on trouve en Erlang/Elixir, et qui commence à apparaître en Python avec
match
.Ici c'est pour dire que l'information de type ne se situe pas au niveau de la variable. Il n'y aura pas de mot clé
typeof
par exemple.Pour le système de contrainte, tu as vu juste :
Comme je l'ai dit dans le disclaimer, très peu de code pour l'instant. Le but ultime est d'en faire un langage compilé vers LLVM IR, pour l'instant c'est un interpréteur.
Je compte faire le plus de vérifications possibles à la compilation, mais l'exemple suivant devra être testé à l'exécution :
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
[^] # Re: Intéressant
Posté par barmic 🦦 . Évalué à 4.
C'est plus du typage par valeur, non ? Je connais pas de nom plus utilisé pour ça.
Ça permet de définir une fonction
foo
qui prend un entier par polymorphisme sur les valeurs (tu crée une fonction pour la valeur 0 et une pour les autres entiers par exemple).Python a toujours fais du typage structurel dynamique, mais rien sur les valeurs il me semble et le match est un if amélioré il n'a pas d'impact sur le typage il me semble.
https://linuxfr.org/users/barmic/journaux/y-en-a-marre-de-ce-gros-troll
[^] # Re: Intéressant
Posté par David Delassus (site web personnel) . Évalué à 2.
La sémantique est bien différente dans chacun de ces langages. Mais à l'usage, ça se ressemble.
Entre Python :
Et Elixir :
Ou TypeScript :
La réflexion du développeur est la même bien que l'implémentation du langage et le sens du code soit différent.
En Letlang on aurait donc :
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
# Wow
Posté par Guillaume Denry (site web personnel) . Évalué à 6.
Très impressionnant !
Je n'ai pas les compétences pour savoir si ce que tu as fait existe dans d'autres langages mais je suis tout de même très impressionné par le volume de fonctionnalités.
L'avantage que je vois immédiatement sur des langages comme Haskell, c'est l'expressivité de letlang, c'est probablement une des choses les plus complexes à faire émerger dans un langage fonctionnel.
Bonne continuation pour la suite.
[^] # Re: Wow
Posté par David Delassus (site web personnel) . Évalué à 3.
Avant d'être impressionné, attend que je l'implémente :)
Cette expressivité tu la retrouves beaucoup en mathématiques, qui à l'avantage de pouvoir utiliser plus de symboles qu'il n'existe sur un clavier et de ne pas être limité à une seule ligne de texte pour écrire une expression.
Je m'étais d'ailleurs acheté "Principia Mathematica" et 2-3 autres livres, pour au final me rendre compte que cette expressivité vient du manque de règles dans l'écriture des mathématiques.
Merci pour ton retour en tout cas.
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
# Choix du nom
Posté par Enzo Bricolo 🛠⚙🛠 . Évalué à 9.
Je m'attendais à un truc punchy comme "nogolang" puisque tu n'aimes pas le golang ou alors un truc marrant genre "jacklang" ou "aveclalang".
[^] # Re: Choix du nom
Posté par David Delassus (site web personnel) . Évalué à 4.
En mathématiques, tu verras très souvant le genre de phrase :
Ou en anglais :
Dans mes premiers brouillons, tout se définissait en utilisant le mot clé
let
(fonctions, classes, etc…). Ce qui a donné le nom Letlang.J'ai fini par écarter cette dernière idée par soucis de lisibilité.
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
# Contraintes
Posté par barmic 🦦 . Évalué à 7.
Bravo pour ton projet et le courage de le partager !
J'ai pas encore tout lu mais avant de faire une pause dans ma lecture j'avais une question.
Le système de contraintes (que je trouve vraiment cool) demander d'implémenter un solveur d'équation, c'est pas très lourd quand on dépasse les exemples simples ?
https://linuxfr.org/users/barmic/journaux/y-en-a-marre-de-ce-gros-troll
[^] # Re: Contraintes
Posté par David Delassus (site web personnel) . Évalué à 3.
Exact, le solveur d'équation va être la fonctionnalité la plus difficile à implémenter, et je n'ai aucune idée des performances que cela donnera.
J'ai même songé à faire un bête appel à Wolfram Alpha pour le coup. Je vais sûrement essayer de les contacter à un moment.
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
[^] # Re: Contraintes
Posté par Thomas Douillard . Évalué à 6.
Tu veux un système symbolique ou numérique ? Si c’est numérique tu risques de te retrouver à devoir gérer des problèmes d’arrondis sur les flottants, d’intervalle et caetera …
il y a des solveurs pour ça, https://choco-solver.org/docs/ qui fait les variables discrètes et aussi les flottants apparemment, ou http://www.ibex-lib.org/ pour les domaines flottants.
[^] # Re: Contraintes
Posté par David Delassus (site web personnel) . Évalué à 2.
Je ne me suis pas encore penché sur la question. J'avais gratté un peu la surface des solveurs SAT mais sans plus. Pour le coup, je compte contacter des gens plus compétents à l'INRIA pour m'aider sur cet aspect.
J'avais imaginé utiliser libgmp pour représenter les nombres et esquiver les problèmes d'arrondi. A voir comment ça s'intègre avec le solveur d'équation.
J'espère pouvoir utiliser un solveur existant (et pourquoi pas plusieurs backend qu'on peut choisir à la compilation ?) et ne pas devoir en implémenter un de 0.
Je vais lire ça avec attention, merci! :)
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
[^] # Re: Contraintes
Posté par Nicolas Boulay (site web personnel) . Évalué à 4.
Ton système pourrait permettre d'implémenter les vérifications d'unité de calcul sans être méga lourd ?
"La première sécurité est la liberté"
[^] # Re: Contraintes
Posté par David Delassus (site web personnel) . Évalué à 1.
Sans être méga lourd, je sais pas.
J'avoue qu'à part des solveurs SAT/SMT pour résoudre des Sudokus ou autre problèmes du genre, j'y connais pas grand chose.
J'ai réuni un ensemble de papier de recherche sur le sujet que je dois encore lire pour vraiment me faire une idée des possibilités et limitations.
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
[^] # Re: Contraintes
Posté par Nicolas Boulay (site web personnel) . Évalué à 4. Dernière modification le 09 janvier 2022 à 09:51.
Lisaac avait aussi une syntaxe à mot clef intéressante.
https://fr.wikibooks.org/wiki/Lissac/slot_param%C3%A8tres_et_mots_cl%C3%A9fs
sinon niveau compilation, il était aussi très fort en utilisant le typage pour enlever les appel virtuel, il avait un mot clef "expanded" pour pouvoir éviter le boxing d'object, etc…
"La première sécurité est la liberté"
[^] # Re: Contraintes
Posté par arnaudus . Évalué à 6.
Ça me semble aussi limite impossible dans l'absolu, mais on pourrait imaginer que les capacités du solveur font partie des spécifications du langage. Par exemple, le solveur sait gérer tel ou tel types d'équations, mais par tel autre.
Ce que je n'ai pas trop compris, c'est ce qui était censé être du ressort du compilateur. J'ai l'intuition que le solveur n'a que peu d'intérêt s'il n'est pas dynamique, puisqu'en pratique le compilateur ne serait qu'une calculette scientifique. Si tu veux spécifier un truc comme
let x^2-4 < 0
, ça revient à écrirelet -2 < x < 2
, je ne vois pas trop l'intérêt. Autant avoir un onglet ouvert sur Wolfram en même temps que tu codes. Là où ça devient vraiment intriguant, c'est d'avoir des limites dynamiques, du stylelet y*x^2-4 < 0
, où y est un paramètre de la fonction. Mais forcément, ça ne peut pas trop se faire à la compilation, et si ça se fait à l'exécution, ça va avoir une conséquence sur les perfs.[^] # Re: Contraintes
Posté par David Delassus (site web personnel) . Évalué à 1.
Ça serait dommage, mais c'est une éventualité que je n'exclu pas.
Pour le coup, c'est comme les constexpr en C++ : si le compilateur peut le faire, alors il le fait. Sinon, c'est au runtime.
Oui, mais je suis justement curieux de voir l'ampleur de cet impact.
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
[^] # Re: Contraintes
Posté par arnaudus . Évalué à 2.
Je ne suis pas sûr de comprendre. Certaines équations ont une solution qu'on peut déterminer par un algorithme, d'autres n'ont pas de solution exprimables avec des fonctions usuelles—mais pour un programme informatique, ça n'est pas un problème majeur, puisqu'il n'y a pas de différence entre l'approximation numérique d'une fonction usuelle (comme log()) et d'une fonction non-usuelle (comme probit() ou LambertW() ). Par contre, certaines équations n'ont qu'une solution "ingénieuse" (de nombreuses intégrales par exemple), qu'il semble impossible d'implémenter dans un compilateur.
Mais au final, je me demande quand même, à part l'exploit, à quoi ça peut servir. À moins qu'il ne s'agisse d'un langage de résolution d'équations, qui a besoin de définir des variables à partir d'équations aussi complexes.
[^] # Re: Contraintes
Posté par David Delassus (site web personnel) . Évalué à 1.
Ce que je voulais dire, c'est que si il s'avère qu'implémenter cette fonctionnalité est impossible ou apporte plus de problèmes que de solutions, je n'exclu pas de la retirer.
Cette idée est partie du concept de undefined, pour permettre de travailler avec les propriétés d'une variable sans forcément connaître sa valeur (ce qui se fait beaucoup en math).
Si tu prend l'exemple suivant :
Pas besoin d'écrire plusieurs fois
std.strlen
, on connait déjà la définition del
. En ajoutant une contrainte à la valeur del
, on contraint aussi les valeurs possibles des
.-https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
[^] # Re: Contraintes
Posté par arnaudus . Évalué à 2.
Pardon, je m'étais mal exprimé. Je ne mettais pas en cause l'intérêt de travailler avec des contraintes sur des variables, mais je voulais dire "à quoi servirait un solveur d'équations". On peut très bien faire reposer la résolution d'équations sur le programmeur, qui lui-même peut utiliser l'outil qu'il souhaite. Je comprends l'intérêt de "let x = y2 - 3*y + 2", mais pas de "let x2 -5*x + 3 = 6*y".
[^] # Re: Contraintes
Posté par David Delassus (site web personnel) . Évalué à 1.
La deuxième forme n'est qu'une conséquence du fait que
=
est une opération. La plupart des langages appellent cette opération==
, du coup je comprend la confusion.Au niveau de l'AST, j'ai :
Autoriser la première forme, c'est autoriser la seconde. Sachant que pour la seconde, si je connais la valeur de
x
et dey
, il est logique de pouvoir faire ce test.Ce qu'il faut comprendre, c'est que
let
ajoute des contraintes (qui doivent être compatibles avec les contraintes existantes) :Ce qui pourrait aussi être utilisé comme il suit :
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
[^] # Re: Contraintes
Posté par Thomas Douillard . Évalué à 2.
Outre prolog, tu peux peut-être regarder aussi le langage Oz qui intègre les contraintes dans son paradigme : http://mozart2.org/
[^] # Re: Contraintes
Posté par steph1978 . Évalué à 6.
En effet le solveur aura sûrement des limites, sinon on pourrait lui demander
let x: P ≟ NP
et ça nous aiderai bien.[^] # Re: Contraintes
Posté par Joël Thieffry (site web personnel) . Évalué à 2.
Ça répondrait
true
oufalse
, on serait à peine plus avancé…# Prolog ?
Posté par Aldoo . Évalué à 7.
Alors ok, syntaxiquement, Letlang est aux antipodes de Prolog. Mais quand on me parle de langage de programmation basé sur des contraintes logiques et leur résolution, c'est tout de suite à Prolog que je pense.
Y a-t-il des liens assumés ? (j'ai l'impression que non, vu que Prolog n'est pas cité dans les sources d'inspiration)
[^] # Re: Prolog ?
Posté par David Delassus (site web personnel) . Évalué à 4.
Indirectement,
Elixir compile en Erlang qui est inspiré de Prolog.
Je voulais vraiment intégrer de la programmation logique (cf prédicat des classes et ensembles et
let
).En pattern matching par exemple, on utilise la notion d'unification (l'article parle justement de Prolog).
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
# Très intéressant !
Posté par Pierre86 . Évalué à 1.
Félicitations pour ce travail !
Je n'ai pas les compétences pour juger, mais c'est en tout cas particulièrement intéressant à lire.
Pour information, à combien estimes-tu le temps passé jusqu'ici sur la spécification du langage ?
[^] # Re: Très intéressant !
Posté par David Delassus (site web personnel) . Évalué à 1.
Merci :)
Les premiers brouillons datent d'il y a 1 an et demi. En temps cumulé, je dirais bien 6 à 8 mois du coup.
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
# Lapin compris
Posté par Dring . Évalué à 2.
Y a un truc qui m'échappe sur la gestion des valeurs indéfinies.
Donc si je suis en train de faire un pauvre if, sur une variable x à laquelle j'ai oublié d'assigner une valeur, au lieu de planter ça va me dire "faux" ou "vrai" en fonction de si une solution existe ? C'est pas un peu dangereux ça ?
Bon, j'imagine qu'on tape pas tous les jours "x - 3 = 0" pour vérifier que x vaut 3. Mais ça fait quoi si mon if est comme ça :
Je fais plein de trucs, ou pas ?
[^] # Re: Lapin compris
Posté par David Delassus (site web personnel) . Évalué à 3.
Hahaha. Selon ma spec actuelle, oui tu fais plein de trucs.
Peut être rajouter un mot clé
solvable <equation>
pour éviter de perdre les développeurs non matheux ?Ainsi:
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
[^] # Re: Lapin compris
Posté par Letho . Évalué à 1. Dernière modification le 08 janvier 2022 à 13:51.
Je dis peut-être une bêtise, mais ne pourrait-on pas considérer qu'une variable représente l'ensemble des valeurs possibles selon les contraintes définies ?
Définir
x := 2
reviendrait à affecter àx
le singleton { 2 }.L'opérateur
=
ne serait alors que du sucre syntaxique pour les ensembles à un seul élément : pour une variable x représentant un singleton et une valeur n,x = n
serait équivalent àn in x
.Et l'on pourrait réécrire le code ci-dessus de cette façon :
[^] # Re: Lapin compris
Posté par Letho . Évalué à 1.
Pardon, il fallait lire
if (x = 3) ## false
sur la dernière ligne. Si un gentil modo passait dans le coin ;)[^] # Re: Lapin compris
Posté par David Delassus (site web personnel) . Évalué à 4.
Dans la théorie ZFC, qui est une théorie de fondation des mathématiques, au même titre que la théorie des catégories, on ne manipule que des objets que l'on pourrait qualifier d'ensemble.
La seule opération de base est
appartient à
(ouin
). L'opération=
est alors défini comme il suit :On peut définir les opérations union et intersection de la même manière.
On définit ensuite l'ensemble vide avec le théorème suivant :
NB: En utilisant la définition de
=
et de0
, on arrive à prouver que l'ensemble vide est unique.L'ensemble vide, je l'ai appelé
0
c'est pas pour rien. On peut définir quelques autres ensembles :1 = 0 U { 0 } = { 0 } = { {} }
2 = 1 U { 1 } = { 0, 1 }
3 = 2 U { 2 } = { 0, 1, 2 }
A partir de cette construction, on peut créer la formule suivante :
S(n) = n U { n }
, ouS(n)
est le "successeur de n".NB : On peut définir l'opération
A < B
tel que A appartient à B.Tout ça pour dire que
=
est très différent dein
. En effet si on accepteA = B
comme synonyme deB in A
:=
en théorie ZFCA = B => B < A
ce qui est contraire au sens communEnfin, on a défini
let x: int
, c'est bizarre de le considérer comme étant un ensemble d'int. D'un point de vue typage, ça passe pas non plus.Fun facts:
N = { 0, 1, 2, 3, ... }
est un objet de la même forme que0
,1
,2
etc…w = N U { N }
est le successeur de N, et on a la définition des nombres ordinauxhttps://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
[^] # Re: Lapin compris
Posté par Letho . Évalué à 2.
Merci (sincèrement).
Je suis développeur, mais ne suis pas passé par une école d'ingénieur. Je touche assez rapidement à mes limites quand il s'agit de mathématiques – ce qui est d'autant plus frustrant que je trouve cela passionnant.
Je viens de me trouver un cours sur ZFC, je vais aller potasser cela ;)
[^] # Re: Lapin compris
Posté par barmic 🦦 . Évalué à 2.
N'hésite pas à le partager :)
https://linuxfr.org/users/barmic/journaux/y-en-a-marre-de-ce-gros-troll
[^] # Re: Lapin compris
Posté par David Delassus (site web personnel) . Évalué à 1.
https://www.youtube.com/watch?v=-4iFWhzU230 :)
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg
# Et TapTempo ?
Posté par Elephant (site web personnel) . Évalué à 8.
Est-il prévu qu’on puisse transposer TapTempo en LetLang ?
# C'est bien joli mais
Posté par Axioplase ıɥs∀ (site web personnel) . Évalué à 4.
La question importante pour le décideur pressé, c'est "peut-on écrire TapTempo en Letlang ?"
Si oui, alors c'est un succès. Si non, c'est une perte de temp(o).
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.