Skip to content

This issue was moved to a discussion.

You can continue the conversation there. Go to discussion →

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Formalisation du système de type de publicodes #14

Closed
johangirod opened this issue Sep 16, 2020 · 24 comments · Fixed by #66
Closed

Formalisation du système de type de publicodes #14

johangirod opened this issue Sep 16, 2020 · 24 comments · Fixed by #66

Comments

@johangirod
Copy link
Member

Je propose d'élargir ici la discussion entamé dans #10, et de réfléchir aux types dans le langage publicodes.

Cette discussion est un préliminaire à une meilleure intégration des types dans publicodes : il s'agit d'établir une formalisation idéale minimale du système de type de publicodes afin d'en fiabiliser l'implémentation, tout en aboutissant au moins de modifications des programmes existants possible.

Le système de type de publicodes

Le système de type de publicode côté utilisateur est relativement simple. Il comporte les types suivants :

  • Booléen
  • Texte
  • Date
  • Nombre
  • Objet externe
  • Option
  • Possibilités

Nombre

type nombre = { valeur: number; unité: unit }

Le type nombre définit également une unité. Celle-ci peut être vide, dans ce cas, le nombre est considéré un rapport (par exemple un taux).

Lorsqu'un nombre peut être converti d'une unité vers d'autres, alors ces unités forment une classe d'équivalence. Par exemple année, mois, jour et semaine. Ou kg, g, mg, lb et oz.

Par conséquent, on peut substituer type de nombre unité par un autre type d'unité de même classe. Par exemple : €/mois et €/an. La conversion est effectuée à l'évaluation.

Cela abouti aux effets suivants :

  • 3 €/mois + 154 €/an est une formule valide
  • 3 €/mois + 154 % est une formule invalide

Option et Possibilités

Option est un type littéral définit globalement. On peut en construire une instance via le symbole '#'

Dans l'exemple ci dessous:

CDD: 
    formule: '#CDD'

CDD est de type #CDD

Le constructeur de type Possibilités permet de définir une union d'Option.

contrat: 
  type:
    une possibilité parmis: 
      - CDD
      - CDI
      - Stage

Le type de contrat sera: #CDD | #CDI | #Stage

Il est possible de tester l'égalité d'options :
contrat = #CDD

On peut ne peut remplacer une règle de type possibilité seulement par une union plus restreinte (sous-type)

assimilé salarié . contrat: 
  type: option
  remplace: 
    - règle: contrat
      par: '#CDI'

On peut imaginer l'ajout d'un mécanisme correspondance qui vérifie la complétude des options listées (comme évoqué dans betagouv/mon-entreprise#824 (comment)).

Objet externe

Le type Objet externe est un type permettant de manipuler dans publicodes des objets javascript, généralement issus d'API externes. Le seul mécanisme qui permet de manipuler une variable de ce type est synchronisation.

Par exemple, le cas de l'API commune peut être traité ainsi :

localisation . commune:
  type: objet externe
  affichage:
    champs spécial: commune

localisation . département:
  synchronisation: 
    règle: commune
  chemin: departement . nom
  type: 
    une possibilité parmi:
        - Ain
        - Aisne
        - Allier
          ...
        - Martinique
        - Guyane
        - La Réunion
        - Mayotte
    

localisation . versement transport:
  synchronisation: 
    règle: commune
  chemin: taux versement transport
  unité: '%'

Le cas d'usage est la mise à jour de plusieurs variables à partir de la réponse à une seule question.

C'est la seule potentielle faiblesse du système de type, on l'utilisateur est attendu de fournir un objet javascript de la bonne forme dans la situation, sans vérification formelle de la part du moteur.

Type internes

Par ailleurs, publicodes possède un certains nombre de type interne utile pour définir son modèle d'évaluation et pour l'inférence de type des mécanismes :

  • Non Applicable : la valeur est non applicable dans le cadre de la situation présente. Cela correspond conceptuellement au fait qu'elle est non définie (par exemple, le type d'activité libérale règlementée n'est pas applicable dans le cas d'une entreprise d'artisanat), ou qu'elle ne s'applique pas (par exemple, la cotisation CURPS ne s'applique pas pour les revenus professionnels négatifs)

  • Manquant : il est impossible de connaître la valeur de cette variable. Par exemple, si elle n'a ni formule, ni valeur par défaut et pas de valeur dans la situation. Ou alors elle possède une formule mais une des composante est manquante.

  • Temporelle T : type une variable dont la valeur change au cours du temps. C'est un foncteur applicatif.

Toute formule de règle possède un type qui peut être inféré par le moteur. En outre, la règle possède un champs "type" permettant de vérifier le type de sa formule, ou de définir son type dans le cas de variable "feuille" (définie par l'utilisateur dans la situation).

Formule = Booléen | Nombre | Texte | Date | Spécial | Possibilités

Le type Valeur, correspondant à l'évaluation d'une règle de type T est le suivant :

Valeur T = Non Applicable | Manquante | T

Temporelle T

Le type temporelle permet de representer une variable dont la valeur change au cours du temps. Il ne peut pas être explicitement définit par l'utilisateur au niveau de la règle. Le moteur s'occupe de 'lifter' automatiquement les mécanismes opérant sur le type T pour qu'ils opèrent sur Temporelle T. Au vu de l'utilisateur, le fait qu'une règle soit une variable ou variable temporelle est donc tout à fait transparent.

Par conséquent, le type temporel d'une règle n'est pas determinable statiquement. Chaque noeud peut donc être de type T | Temporelle (T), de manière indifférenciée. Seule l'execution du programme aboutit à l'une ou l'autre des valeurs.

Temporelle est un foncteur applicatif.

Fonctionalités limités

Contrairement à la plupart des langages de programmation, publicodes n'a pas les fonctionalités suivantes :

  • L'utilisateur ne peut pas manipuler de type fonction : les mécanismes sont définis une fois pour toute dans la structure du langage même.
  • L'utilisateur ne peut pas manipuler d'unions de type (outre Possibilité).
  • L'utilisateur ne peut pas manipuler de type "record".
  • L'utilisateur ne peut pas manipuler d'intersections de type.

Au vu de la faible complexité de son système de type, Publicodes devrait pouvoir être un langage statiquement typé.

Type des mécanisme

On peut donc définir une inférence de type pour chaque mécanisme, ainsi que les types pour lesquelles ils sont définit.

a x b

Par exemple, pour la multiplication, on a les règles suivante :

(a: Non Applicable, b:*) => Non Applicable
(a: Manquante, b:*) => Manquante
(a: Nombre u, b:Nombre v) => Nombre (u.v)
(a: T, b: U) => U x T

Définit sur l'espace (Evaluation(Nombre), Evaluation(Nombre))

somme

Pour le mecanisme somme, on a :

(a: Valeur(T)[]) => Valeur(T)[]

Definit sur Evaluation(Nombre)[]

Questions ouvertes

  • Quel solution d'implémentation pour la verification de type dans publicodes ?
  • Comment la question des unités est-elle soluble dans un système de type standard ? Ou doit-elle être approchée séparément ? Le type doit-il être le même pour une classe d'unité ? Mais alors comment définir la notion de conversion ?
  • Comment bien appréhender le type des variables temporelle ? Est-ce une bonne chose qu'elles soient complètement invisible pour l'utilisateur ?
@denismerigoux
Copy link

Salut ! Ça y est on se rapproche d'une vraie formalisation, je commence à voir de la syntaxe apparaître :)

Alors votre concept d'"Option" se rapproche d'un type somme, sauf que vous voulez pas franchir le pas et mettre du pattern matching. C'est dommage, parce que c'est une des features les plus intuitives et incroyables de langages fonctionnels. Sans pattern matching, votre compilateur ne pourra pas vérifier si l'utilisateur traite bien "tous les cas" avant d'exécuter le programme.

Par exemple, pour une fonction qui calcule un truc sur un contrat, dans Publicodes vous allez devoir écrire :

if contrat.type = #CDD then 
   ... 
else if contrat.type = #CDI then 
   ...
else # contrat.type = #Stage 
  ...

Mais en faisant comme ça impossible de savoir si vous n'avez pas oublié un cas, ce qui est sous-optimal puisque justement vous déclarer tous les cas possible quand vous définissez votre type option. Avec du pattern matching, vous aurez quelque chose comme ça :

match contrat.type with 
 | #CDD -> ...
 | #CDI -> ...

Là j'ai oublié le cas #Stage, et le compilateur peut me sortir un message d'erreur pour me dire "tu as oublié le cas Stage !".

Sans ce mécanisme, vous retombez sur ce qu'on appelle un "type variant" (e.g. https://caml.inria.fr/pub/docs/u3-ocaml/ocaml051.html) qui est beaucoup moins intéressant qu'un type somme car impossible d'en faire une vérification statique.

Sinon pour répondre à vos questions ouvertes:

Quel solution d'implémentation pour la verification de type dans publicodes ?

Il vous faut un vérificateur de type. Vous pouvez écrire ça en JS, c'est juste un fonction qui prend votre AST et qui le traverse en vérifiant partout que les types vont bien.

Comment la question des unités est-elle soluble dans un système de type standard ? Ou doit-elle être approchée séparément ? Le type doit-il être le même pour une classe d'unité ? Mais alors comment définir la notion de conversion ?

Votre système d'unités est pas trop mal, chaque unité est un type "primitif" (et donc différents des uns des autres). Pour la conversion ("casting"), il faut faire l'hypothèse de fonctions primitives qui transforment un type primitif en un autre.

Comment bien appréhender le type des variables temporelle ? Est-ce une bonne chose qu'elles soient complètement invisible pour l'utilisateur ?

Là ça dépend le but de ce truc de variables temporelles. Si c'est juste un mécanisme interne qui permet d'appliquer N fois la même fonction à une liste de N situations (classées par date) pour affichage sur le site, pas besoin de le formaliser. Par contre si vous voulez en faire un mécanisme de votre langage ça devient beaucoup plus compliqué. Deux possibilités :

  • Soit vous en faites comme vous dites un "foncteur applicatif" mais là il faut rajouter dans votre formalisation un type liste et du polymorphisme défini par l'utilisateur
  • Soit vous vous en sortez par métaprogrammation, et vous dites que vous avez un opérateur qui transforme un programme opérant sur 1 variable en un programme opérant sur une liste de variables. Plus simple mais ça fait des messages d'erreur moche pour l'utilisateur puisque ça crée du code "invisible".

@johangirod
Copy link
Member Author

johangirod commented Sep 17, 2020

sauf que vous voulez pas franchir le pas et mettre du pattern matching. C'est dommage, parce que c'est une des features les plus intuitives et incroyables de langages fonctionnels

Si, si, justement ! Le pattern matching serait effectué par un mécanisme dédié : betagouv/mon-entreprise#824 (comment). De même, là ou la structure structure if / else, (appelée variations), possède toujours un else qui branche par défaut à Non Applicable, la correspondance lève une erreur de type si toutes les options ne sont pas adressée.

Par contre si vous voulez en faire un mécanisme de votre langage ça devient beaucoup plus compliqué.

C'est justement cette option qui a finalement été choisie (nous avions également hésité à l'abstraire au dehors du langage). La raison : certains dispositifs législatifs demande de manipuler des valeurs qui changent au cours du temps (comme la régularisation). Plus généralement, la temporalité est une donnée essentielle à la législation, et il nous semblait important de pouvoir la traduire directement dans publicodes.

On doit donc en passer par du "compliqué".

Soit vous en faites comme vous dites un "foncteur applicatif" mais là il faut rajouter dans votre formalisation un type liste et du polymorphisme défini par l'utilisateur

Doit-on obligatoirement l'exposer à l'utilisateur ? Autrement dit, ne peut-on pas considérer que lorsque l'utilisateur spécifie le type T d'une variable, le moteur infère automatiquement T | Temporelle T ? En ajoutant la contrainte suivante à publicodes : tous les mécanismes / opérateurs de publicodes doivent opérer sur des arguments de type T | Temporelle T. Un peu comme pour les types Non applicable et Manquante.

@denismerigoux
Copy link

Ah j'avais pas vu votre syntaxe pour le pattern matching. Du coup c'est bon vous avez de vrais types somme :)

Hum je vois mieux ce que vous voulez faire avec T | Temporelle T. Mais du coup y a un truc que je comprend pas. Si tous les mécanismes et opérateurs sont polymorphiques sur T | Temporelle T, quand-est ce que vous choisissez de calculer sur une valeur ou une série temporelle ? Il doit bien y avoir des opérateurs qui ne sont pas polymorphiques non ?

@johangirod
Copy link
Member Author

A priori non : les opérateurs qui opèrent "par défaut" sur T sont liftés pour opérer sur Temporelle T. Et pour les mécanismes qui opèrent sur Temporelle T, on transforme les arguments de type T en Temporelle en considérant qu'ils ont la même valeur pour l'éternité. Du point de vue de l'utilisateur, tous les opérateurs sont polymorphique, d'où l'idée de type "caché". En vérité, les transformations sont effectuées lors de l'évaluation, en fonction du type des données fournie.

L'avantage est que le programme de sorti est une fonction polymorphique, et peut être utilisée de manière indifférenciée avec des valeurs "simple" ou "temporelle"

En fait, en y réfléchissant, il semblerait qu'à partir du moment où l'on ne veut pas formaliser le polymorphisme de type dans publicodes, il reste seulement deux possibilités :

  1. Le premier que je viens de développer, équivaut en fait à considérer que le langage est défini exclusivement avec des variables temporelles, les littéraux "classique" étant des variables temporelles définis sur l'éternité.
  2. Ou alors l'utilisateur doit spécifier pour chaque variable dont le type ne peut être inféré (donné en entrée dans la situation par exemple) si son type est T ou Temporelle T. A ce moment là, lorsque l'utilisateur écrit : type: booléen sur une règle, cela est compris comme l'assertion de type suivante : Booléen | Non Applicable | Manquant | Temporelle (Booléen | Non Applicable | Manquant)

Le 1. a l'avantage de la cohérence et de la simplicité, le 2. permet un contrôle plus fin et d'avoir des mécanisme définit exclusivement sur T ou Temporelle T

Je serais d'avis de sélectionner la 1. qui a le mérite d'orienter toute la production de règles de publicode vers une intégration de la dimension temporelle à la racine, sans trop d'effort. Mais qui pourrait être transparente pour l'utilisateur, lors de l'affichage si une valeur est définie sur l'éternité, on ne fait pas mention de la temporalité.

@denismerigoux
Copy link

Merci pour les clarifications. Oui le 1. correspond à ce que j'avais compris dans ta description. Dans ce cas, pas le T | Temporelle T ne rentre même pas dans la formalisation de votre langage, puisque c'est quelque chose d'externe qui concerne uniquement la manière dont vous utilisez les programmes compilés.

@lajarre
Copy link
Contributor

lajarre commented Oct 6, 2020

@johangirod question noob:

CDD: 
    formule: '#CDD'

pourquoi CDD n'est pas string?

@mquandalle
Copy link
Collaborator

Comment la question des unités est-elle soluble dans un système de type standard ? Ou doit-elle être approchée séparément ? Le type doit-il être le même pour une classe d'unité ? Mais alors comment définir la notion de conversion ?

Voir l'utilisation dans F# https://docs.microsoft.com/en-us/dotnet/fsharp/language-reference/units-of-measure

@denismerigoux
Copy link

denismerigoux commented Dec 7, 2020

Ah intéressant, je savais pas que F# avait ça. Par contre ce que cette page de doc ne dit pas c'est que la vérification de types statique pour ces unités est assez compliquée. En gros il vous faudrait un système de type à la Hindley-Milner avec inférence de type basé sur une structure de données union-find : https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system. C'est d'ailleurs ce que F# utilise, comme indiqué dans ce post de blog : https://fsharpforfunandprofit.com/posts/type-inference/.

Désolé pour les gros mots théoriques mais là vous arrivez sur un problème très classique de design de systèmes de type avec une solution également classique et très éprouvée. Là aussi je vous préviens, si vous vous y lancez en mode custom vous allez arriver à un truc mais ce sera très buggué et si jamais vous arrivez à le débugguer complètement vous serez retombé sur l'algorithme W de Hindley-Minler :)

Par exemple, voilà l'algorithme de typage de Catala, également basé sur l'algorithme W : https://github.com/CatalaLang/catala/blob/master/src/catala/default_calculus/typing.ml.

@mquandalle
Copy link
Collaborator

@johangirod grâce à ton message betagouv/mon-entreprise#1291 (comment), j'ai réalisé que j'avais mal compris ta proposition concernant le type Manquante. Vu la définition que tu proposes et afin d'éviter les confusions avec la notion distincte de "variable manquante", je te propose de parler plutôt de type Indéfini quand la formule n'est donnée ni dans la règle ni dans la situation.

Un problème que j'identifie avec un type Indéfini + Non applicable c'est la question du résultat Indéfini × Non Applicable. Tu proposes qu'Indéfini soit "dominant" et donc d'avoir Indéfini × Non Applicable = Indéfini, mais le problème c'est qu'on a en même temps Non applicable × unknown = Non applicable ce qui voudrait dire que notre multiplication n'est pas commutative dans ce cas — sauf à définir Non applicable × Indéfini = Indéfini mais ça nous obligerait à revenir sur l'évaluation paresseuse.

Une alternative c'est de considérer que Non applicable et Indéfini sont tous les deux des erreurs dans un type Result<T, E> avec le type E defini comme une union des erreurs : E = NonApplicable | Indefini. D'une certaine manière ça résout le problème de commutativité du produit, dès qu'on a un terme E le resultat vaut E aussi, et le type d'erreur est une information inférée (comme l'unité pour un type nombre). Cela permettrait aussi de définir d'autres erreurs comme division par zéro, etc.

La seule chose qui me chiffonne un peu c'est de considérer que "non applicable" est une "erreur", il faudrait sans doute trouver un autre terme que "erreur" pour indiquer "une raison pour laquelle cette valeur n'est pas disponible".

@mquandalle
Copy link
Collaborator

Option est un type littéral définit globalement

Sur la question du type littéral, la ré-implémentation des remplacements et les avertissements sortis dans betagouv/mon-entreprise#1298 rendent effectivement nécessaire d'avoir un type littéral global, ceci afin de l'utiliser dans plusieurs règles "une possibilité" pour exprimer des littéraux mutuellement exclusifs. C'est en particulier le cas avec le choix "assimilé salarié" qui est mutuellement exclusif avec à la fois les autres statuts du dirigeant assimilé salarié | indépendant | auto-entrepreneur mais aussi avec les autres contrats salariés assimilé salarié | CDI | CDD | Stage | Apprentissage.

Évidemment comme pour les règles le fait d'avoir un nom global n'empêche pas l'utilisation des espaces de noms.

En revanche je suis un peu gêné par la syntaxe #CDD dont je trouve qu'elle s'intègre mal avec notre modèle actuel :

  • possibilité d'utiliser des espaces dans les noms de variable, exemple “assimilé salarié”
  • symbole syntaxique dont le fonctionnement n'est pas explicite pour quelqu'un qui ne connaît pas la fonctionnalité (je pense que c'est aussi le sens de la dépréciation de [ref])

@mquandalle
Copy link
Collaborator

Enfin dernier point je pense qu'il faut considérer une équivalence entre les types Publicodes et les types Typescript afin d'améliorer le typage côté applicatif

const net = engine.evaluate("contrat salarié . rémunération . net")
net.value !== false // Type Error: value is a number

const jei = engine.evaluate("entreprise . statut JEI")
jei.value > 10 // Type Error: value is a boolean

const imposition = engine.evaluate("entreprise . imposition")
imposition.value === 'ir' // Type Error: value is of type 'IR' | 'IS'

@denismerigoux
Copy link

Enfin dernier point je pense qu'il faut considérer une équivalence entre les types Publicodes et les types Typescript afin d'améliorer le typage côté applicatif

Hum ça risque de ne pas marcher ça, le typage de TypeScript n'est pas dépendant, donc engine.evaluate ne peut pas retourner un type différent selon la valeur de ses arguments. Par contre ce que vous pouvez faire c'est que engine.evaluate retourne une énumération où les variants de l'énumération sont les types Publicodes. Comme ça le client de engine.evaluate peut pattern matcher sur l'enum et asserter que engine.evaluate retourne bien une valeur du bon type.

@johangirod
Copy link
Member Author

johangirod commented Dec 14, 2020

Un problème que j'identifie avec un type Indéfini + Non applicable c'est la question du résultat Indéfini × Non Applicable. Tu proposes qu'Indéfini soit "dominant" et donc d'avoir Indéfini × Non Applicable = Indéfini, mais le problème c'est qu'on a en même temps Non applicable × unknown = Non applicable ce qui voudrait dire que notre multiplication n'est pas commutative dans ce cas — sauf à définir Non applicable × Indéfini = Indéfini mais ça nous obligerait à revenir sur l'évaluation paresseuse.

En fait, je pointais juste dans mon commentaire qu'ils n'avaient pas la même sémantique, en prenant le cas particulier des sommes. Mais on peut imaginer que la valeur Non Applicable est "dominante" par rapport à Indéfinie dans la multiplication.

Une alternative c'est de considérer que Non applicable et Indéfini sont tous les deux des erreurs dans un type Result<T, E> avec le type E defini comme une union des erreurs : E = NonApplicable | Indefini

J'ai pas très bien compris la sémantique de Result. Si c'est un type Either cela revient à T | NonApplicable | Indéfini, ce qui revient à la proposition initiale. En fait je n'ai pas tellement compris le problème que tu essaye de résoudre :p.

En revanche je suis un peu gêné par la syntaxe #CDD dont je trouve qu'elle s'intègre mal avec notre modèle actuel :

Remarques très pertinentes, je suis d'accord. On pourrait imaginer un mécanisme créateur de type litteral ? Peut-être de litteral ? Ou option ?

Enfin dernier point je pense qu'il faut considérer une équivalence entre les types Publicodes et les types Typescript afin d'améliorer le typage côté applicatif

Si les règles sont parsées côté serveur, on peut tout à fait imaginer créer un rule.d.ts qui expose les bons types. J'imagine que ça répondrait au problème.

engine.evaluate ne peut pas retourner un type différent selon la valeur de ses arguments

A priori si, en utilisant les overloads

@mquandalle
Copy link
Collaborator

mquandalle commented Dec 14, 2020

Oui pas de problème avec TypeScript: Démo (édité)

@denismerigoux
Copy link

Ah oui d'accord je comprend mieux:

type RulesType = {
  "contrat salarié . rémunération . net": EngineNode<number>,
  "entreprise . statut JEI": EngineNode<boolean>
  "entreprise . imposition": EngineNode<"IR" | "IS">
}

Forcément avec un système de types Turing-complet on peut faire plein de choses :)

@mquandalle
Copy link
Collaborator

mquandalle commented Dec 14, 2020

En fait je n'ai pas tellement compris le problème que tu essaye de résoudre

C'est probablement pas un gros problème, et ce que je raconte ne change pas grand chose mais l'idée c'est qu'on a

Indéfini × Non Applicable = Indéfini 
Non applicable × Indéfini = Non applicable

Ce qui n'est pas top car notre multiplication est non commutative. On pourrait dire que l'une ou l'autre de ces valeurs est "dominante" ce qui résoudrait le problème de la commutativité mais au prix de l'évaluation paresseuse (car en pratique on s'arrête au premier terme qui n'a pas de valeur sans chercher à calculer les suivants).

L'idée est donc de ne plus faire la distinction au niveau du typage entre ces deux "erreurs" et d'avoir un type "Erreur" qui se comporte comme désiré dans un produit

Erreur × unknown = Erreur
unknown × Erreur = Erreur

Reste à "remonter" le type d'erreur, c'est là qu'il faut que je creuse les pointeurs que Denis nous a partagé, mais j'ai l'impression que c'est un paramétrage de type qui ressemble à ce qu'on fait avec les unités pour le type Number.

Erreur(x) × unknown = Erreur(x)
Erreur(x) × Erreur(y)= Erreur(x)
Number(x) × Number(y) = Number(x.y)

Forcément avec un système de types Turing-complet on peut faire plein de choses :)

This is a SQL database implemented purely in TypeScript type annotations. (!)

@johangirod
Copy link
Member Author

johangirod commented Dec 14, 2020

On peut effectivement imaginer regrouper les comportements de Indéfini et Non Applicable derrière le type Erreur dans la multiplication. Mais ça ne sera pas le cas dans tous les mécnanismes (la somme par exemple).

Par ailleurs, il ne faut pas oublier non plus la gestion des missings variables, qui complexifie un poil la chose au niveau de l'évaluation paresseuse.

Missing = None | Record<DottedName, number>
Evaluation<T extends Types , M extends Missing> = { nodeValue: T, missing: M]

Valeur<Erreur, None> x unknown  = Valeur<Erreur, None>
Valeur<Erreur, M1> x Valeur<unknow, M2> = Valeur<Erreur, M1 + M2>

@mquandalle
Copy link
Collaborator

Intéressant le type Validation. Mais pourquoi veut-on remonter les variables manquantes d'un terme non utilisé :

0 × y = 0
Indéfini × y = Indéfini
Non applicable × y = Non applicable 

Il me semble que la situation est la même dans ces trois cas, et qu'il n'est pas utile de remonter les variables manquantes de y comme variables manquantes du produit. Pour moi c'est le cas aussi quand y est le premier terme du produit.

@johangirod
Copy link
Member Author

(@mquandalle oups, j'ai effacé mon précedent commentaire et réecrit un plus exact).

@mquandalle
Copy link
Collaborator

mquandalle commented Dec 14, 2020

Oui, pas de soucis :)

Valeur<Erreur, M1> x Valeur<unknow, M2> = Valeur<Erreur, M1 + M2>

Mais a t-on besoin de ce comportement ? Pourquoi pas

Valeur<Erreur, M1> x Valeur<unknow, M2> = Valeur<Erreur, M1>

?

Mais ça ne sera pas le cas dans tous les mécanismes (la somme par exemple).

Pour la somme j'ai l'impression qu'on s'en sort avec un comportement identique aussi

0(manque M) + y(manque M') = 0(manque M + M')
Indéfini(manque M) + y(manque M') = Indéfini(manque M + M')
Non Applicable(manque M) + y(manque M') = Non Applicable(manque M + M')

Avec l'idée que ça fonctionne aussi pour d'autres "raisons" d'absence de valeurs (comme la division par zéro, ou la subdivision de "non applicable" en différents types de non applicabilités [dispositif terminé, saisie invalide, etc.])

@denismerigoux
Copy link

Alors là j'ai l'impression que vous voulez faire remonter des messages d'erreur lors de l'exécution. Pourquoi vous utilisez pas un mécanisme d'exceptions avec un try ... catch ? C'est beaucoup plus adapté à ce que vous essayez de faire non ?

@johangirod
Copy link
Member Author

johangirod commented Dec 14, 2020

Mais a t-on besoin de ce comportement ? Pourquoi pas : Valeur<Erreur, M1> x Valeur<unknow, M2> = Valeur<Erreur, M1>

Parce qu'on perdrait le principe des variables manquantes qui est de lister l'ensembles des valeurs manquantes (et non pas juste une sous partie). Je pense que c'est un bon principe, mais on peut le remettre en question.

Pour la somme j'ai l'impression qu'on s'en sort avec un comportement identique aussi
`Non Applicable(manque M) + y(manque M') = Non Applicable(manque M + M')

Ce n'est pas ce qui est implémenté aujourd'hui dans le moteur, et je ne suis pas sûr qu'on gagnerait à introduire un changement de sémantique.

En vrai, je ne suis pas sûr que Non Applicable est une erreur au même type que division par zéro. Pareil pour Indéfini. Pour moi ce sont des valeurs à part entière dans l'evaluation, et on pourrait tout à fait imaginer tester leur valeur. Alors qu'on aura jamais envie de tester la valeur 'division par zéro'

@mquandalle
Copy link
Collaborator

Parce qu'on perdrait le principe des variables manquantes qui est de lister l'ensembles des valeurs manquantes (et non pas juste une sous partie). Je pense que c'est un bon principe, mais on peut le remettre en question.

Il me semble que dans une "variations" on ne remonte actuellement pas les variables manquantes des branches non évaluées

si: C(manque M), alors: A(manque M'), sinon: B(manque M'') → A(manque M+M') | B(manque M+M'')

Si c'est bien le cas, il me semble que le produit par un terme "non applicable" est analogue et devrait donner le même résultat.

En fait pour aller au bout de mon idée, je pense qu'on peut ré-implémenter l'inférence des variables manquantes comme l'union des variables manquantes des arguments évalués par le mécanisme (ie les appels à evaluateNode). Cela permet d'abstraire cette logique à l'extérieur du code spécifique à chaque mécanisme. La chose que l'on perd c'est la possibilité de personnaliser le "poids" donné aux variables manquantes en fonction des mécanismes, logique qu'il me paraît préférable de remplacer par une combinaison de tri explicite et de tri basé sur l'arbre des dépendances.

D'accord avec toi que "Non applicable" n'est pas une erreur et que l'on veut pouvoir tester son résultat. Mais il me semble qu'il devrait avoir le même comportement qu'un "zéro", en particulier pour couper les branches inutiles lors de l'évaluation paresseuse, tout comme les erreurs doivent aussi avoir ce comportement de "zéro" (neutre pour une somme, absorbant pour un produit)

@mquandalle
Copy link
Collaborator

mquandalle commented Dec 14, 2020

Une question qui se pose s'est le résultat d'une somme avec un terme "Indéfini" (ou une autre "erreur"). Pour "non applicable" on sait qu'on veut ignorer le terme non applicable, mais à voir si c'est le même besoin sur les "erreurs". Je proposais de faire pareil, ce qui me semble toujours le plus intuitif, mais je réalise que les tableurs ignorent les cases "vides" dans une somme (élément neutre, ce qui correspond à notre "non applicable" donc) mais rendent "dominantes" les erreurs (élément absorbant)

tableur

@publicodes publicodes locked and limited conversation to collaborators Mar 29, 2022
@mquandalle mquandalle converted this issue into discussion #197 Mar 29, 2022

This issue was moved to a discussion.

You can continue the conversation there. Go to discussion →

Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

4 participants