Journal Letlang, encore un nouveau langage de programmation

Posté par  (site web personnel) . Licence CC By‑SA.
Étiquettes :
52
6
jan.
2022

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éfinitions let 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 :

raclette

  • # Side project

    Posté par  . É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  (site web personnel) . Évalué à 5.

      Bonne année aussi à toi ! :)

      Tu décris ça comme un "side project", je suis plutôt impressionné.

      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.

      À défaut d'avoir les compétences pour collaborer

      J'avoue également manquer de compétences sur l'implémentation de certains aspects du langage, c'est l'occasion d'apprendre :)

      succès qui dépendra probablement de la disponibilité d'une collection de modules standard

      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

  • # Intéressant

    Posté par  . É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 :

    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

    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  . Évalué à 4.

      Une question sur l’aspect équation…

      let x-3 = 0 // => x = 3 la valeur x vaut-elle 3 ou c’est une contrainte ?

x:=2   // Erreur ?
x:=3   // Ok

      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 ?

      let x > 0
let y < 0

y := -2
x := y    // Erreur

      Voilà pour mes interrogations actuelles ;-)

      • [^] # Re: Intéressant

        Posté par  (site web personnel) . Évalué à 3.

        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 ?

        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 :

        let x-3 = 0 // => x = 3, c'est la seule solution

x:=2   // Erreur
x:=3   // Valide mais inutile, on sait déjà que x = 3

        Quand on ajoute une contrainte, est-elle testé à la compilation ?

        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 :

        let x: int
let x > 0
x := readline() |> parse_int()  # pipeline operator comme en Elixir

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

        • [^] # Re: Intéressant

          Posté par  . Évalué à 4.

          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.

          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  (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 :

            match val:
  SomeClass(a, b):
    # ...

  SomeOtherClass(c):
    # ...

            Et Elixir :

            case val do
  (:some_val, a, b) -> # ...
  (:some_other_val, c) -> # ...
end

            Ou TypeScript :

            type SomeTaggedUnion =
  | { t: 'SomeClass', a: osef, b: osef }
  | { t: 'SomeOtherClass', c: osef }

const f = (val: SomeTaggedUnion) => {
  switch (val.t) {
    case 'SomeClass': # ...
    case 'SomeOtherClass': # ...
  }
}

            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 :

            class some_class(ab: (osef, osef))
class some_other_class(c: osef)

res := match val {
  some_class((a, b)) => # ...
  some_other_class(c) => # ...
}

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

  • # Wow

    Posté par  (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  (site web personnel) . Évalué à 3.

      je suis tout de même très impressionné par le volume de fonctionnalités.

      Avant d'être impressionné, attend que je l'implémente :)

      L'avantage que je vois immédiatement sur des langages comme Haskell, c'est l'expressivité de letlang

      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

  • # Choix du nom

    Posté par  . É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  (site web personnel) . Évalué à 4.

      En mathématiques, tu verras très souvant le genre de phrase :

      Soit x blablabla

      Ou en anglais :

      Let x blablabla

      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

  • # Contraintes

    Posté par  . É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  (site web personnel) . Évalué à 3.

      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 ?

      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

      • [^] # Re: Contraintes

        Posté par  . É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  (site web personnel) . Évalué à 2.

          Tu veux un système symbolique ou numérique ?

          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.

          tu risques de te retrouver à devoir gérer des problèmes d’arrondis sur les flottants, d’intervalle et caetera …

          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.

          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.

          Je vais lire ça avec attention, merci! :)

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

          • [^] # Re: Contraintes

            Posté par  (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  (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

    • [^] # Re: Contraintes

      Posté par  . Évalué à 6.

      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 ?

      Ç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 à écrire let -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 style let 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  (site web personnel) . Évalué à 1.

        Ça me semble aussi limite impossible dans l'absolu

        Ça serait dommage, mais c'est une éventualité que je n'exclu pas.

        Ce que je n'ai pas trop compris, c'est ce qui était censé être du ressort du compilateur.

        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.

        si ça se fait à l'exécution, ça va avoir une conséquence sur les perfs

        Oui, mais je suis justement curieux de voir l'ampleur de cet impact.

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

        • [^] # Re: Contraintes

          Posté par  . Évalué à 2.

          Ça serait dommage, mais c'est une éventualité que je n'exclu pas.

          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  (site web personnel) . Évalué à 1.

            > Ça serait dommage, mais c'est une éventualité que je n'exclu pas.
            Je ne suis pas sûr de comprendre.

            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.

            Mais au final, je me demande quand même, à part l'exploit, à quoi ça peut servir.

            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 :

            let s: string
let l = std.strlen(s)
let l < some_buffer_maxsize

s := "foo"
let 3 = l

s := "hello"
let 4 = l

s := "too big for buffer"  # une erreur

            Pas besoin d'écrire plusieurs fois std.strlen, on connait déjà la définition de l. En ajoutant une contrainte à la valeur de l, on contraint aussi les valeurs possibles de s.-

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

            • [^] # Re: Contraintes

              Posté par  . É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  (site web personnel) . Évalué à 1.

                Je comprends l'intérêt de "let x = y2 - 3*y + 2", mais pas de "let x2 -5*x + 3 = 6*y".

                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 :

                pub struct LetStatement {
  expression: Box<Expression>
}

pub enum Expression {
  Add { lhs: Box<Expression>, rhs: Box<Expression> }, // +
  Sub { lhs: Box<Expression>, rhs: Box<Expression> }, // -
  // ...
  Eq { lhs: Box<Expression>, rhs: Box<Expression> },  // =
  // ...
}

                Autoriser la première forme, c'est autoriser la seconde. Sachant que pour la seconde, si je connais la valeur de x et de y, 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) :

                let (x, y): (int, int)
let x**2 - 5 * x + 3 = 6 * y  # tout seul ne sert pas a grand chose

x := get_int_from_stdin()
# si le user tape "0" alors :
# l'equation devient 3 = 6 * y
# il n'y a pas de solutions dans int
# ==> runtime error!

                Ce qui pourrait aussi être utilisé comme il suit :

                data := csv_data
  |> filter(record =>
    record.x ** 2 - 5 * record.x + 3 = 6 * record.y
  )
# data ne contient que les lignes qui valident l'équation

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

        • [^] # Re: Contraintes

          Posté par  . É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  . É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.

  • # Prolog ?

    Posté par  . É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  (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

  • # Très intéressant !

    Posté par  . É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  (site web personnel) . Évalué à 1.

      Félicitations pour ce travail !

      Merci :)

      Pour information, à combien estimes-tu le temps passé jusqu'ici sur la spécification du langage ?

      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

  • # Lapin compris

    Posté par  . Évalué à 2.

    Y a un truc qui m'échappe sur la gestion des valeurs indéfinies.

    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

    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 :

    let x: int

if (x = 3)
   # plein de trucs à faire

    Je fais plein de trucs, ou pas ?

    • [^] # Re: Lapin compris

      Posté par  (site web personnel) . Évalué à 3.

      Mais ça fait quoi si mon if est comme ça :

      let x: int

if (x = 3)
   # plein de trucs à faire

      Je fais plein de trucs, ou pas ?

      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:

      let x: int

if (x = 3) ## error

if solvable (x = 3) ## true

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

      • [^] # Re: Lapin compris

        Posté par  . É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 :

        let x: int

if (3 in x) ## true

if (3 = x) ## false

        • [^] # Re: Lapin compris

          Posté par  . É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  (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 à (ou in). L'opération = est alors défini comme il suit :

          • Soit A et B deux objets, A = B si et seulement si :
          • Pour tout X appartenant à A, X appartient à B
          • Pour tout Y appartenant à B, Y appartient à A

          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 :

          • Soit 0 un objet tel que :
          • Pour tout X, X n'appartient pas à 0

          NB: En utilisant la définition de = et de 0, 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 }, ou S(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 de in. En effet si on accepte A = B comme synonyme de B in A :

          • on brise la définition même de l'opération = en théorie ZFC
          • on insinue que A = B => B < A ce qui est contraire au sens commun

          Enfin, 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 que 0, 1, 2 etc…
          • w = N U { N } est le successeur de N, et on a la définition des nombres ordinaux

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

          • [^] # Re: Lapin compris

            Posté par  . É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 ;)

  • # Et TapTempo ?

    Posté par  (site web personnel) . Évalué à 8.

    Est-il prévu qu’on puisse transposer TapTempo en LetLang ?

  • # C'est bien joli mais

    Posté par  (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.