Formalisation du système de type de publicodes #197
Replies: 24 comments
-
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:
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.
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.
Là ça dépend le but de ce truc de variables temporelles. Si c'est juste un mécanisme interne qui permet d'appliquer
|
Beta Was this translation helpful? Give feedback.
-
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
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é".
Doit-on obligatoirement l'exposer à l'utilisateur ? Autrement dit, ne peut-on pas considérer que lorsque l'utilisateur spécifie le type |
Beta Was this translation helpful? Give feedback.
-
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 |
Beta Was this translation helpful? Give feedback.
-
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 :
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é. |
Beta Was this translation helpful? Give feedback.
-
Merci pour les clarifications. Oui le 1. correspond à ce que j'avais compris dans ta description. Dans ce cas, pas le |
Beta Was this translation helpful? Give feedback.
-
@johangirod question noob:
pourquoi CDD n'est pas string? |
Beta Was this translation helpful? Give feedback.
-
Voir l'utilisation dans F# https://docs.microsoft.com/en-us/dotnet/fsharp/language-reference/units-of-measure |
Beta Was this translation helpful? Give feedback.
-
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. |
Beta Was this translation helpful? Give feedback.
-
@johangirod grâce à ton message betagouv/mon-entreprise#1291 (comment), j'ai réalisé que j'avais mal compris ta proposition concernant le type Un problème que j'identifie avec un type Une alternative c'est de considérer que 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". |
Beta Was this translation helpful? Give feedback.
-
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 É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
|
Beta Was this translation helpful? Give feedback.
-
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' |
Beta Was this translation helpful? Give feedback.
-
Hum ça risque de ne pas marcher ça, le typage de TypeScript n'est pas dépendant, donc |
Beta Was this translation helpful? Give feedback.
-
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
J'ai pas très bien compris la sémantique de Result. Si c'est un type
Remarques très pertinentes, je suis d'accord. On pourrait imaginer un mécanisme créateur de type litteral ? Peut-être de
Si les règles sont parsées côté serveur, on peut tout à fait imaginer créer un
A priori si, en utilisant les overloads |
Beta Was this translation helpful? Give feedback.
-
Oui pas de problème avec TypeScript: Démo (édité) |
Beta Was this translation helpful? Give feedback.
-
Ah oui d'accord je comprend mieux:
Forcément avec un système de types Turing-complet on peut faire plein de choses :) |
Beta Was this translation helpful? Give feedback.
-
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
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
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
This is a SQL database implemented purely in TypeScript type annotations. (!) |
Beta Was this translation helpful? Give feedback.
-
On peut effectivement imaginer regrouper les comportements de 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.
|
Beta Was this translation helpful? Give feedback.
-
Intéressant le type Validation. Mais pourquoi veut-on remonter les variables manquantes d'un terme non utilisé :
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 |
Beta Was this translation helpful? Give feedback.
-
(@mquandalle oups, j'ai effacé mon précedent commentaire et réecrit un plus exact). |
Beta Was this translation helpful? Give feedback.
-
Oui, pas de soucis :)
Mais a t-on besoin de ce comportement ? Pourquoi pas
?
Pour la somme j'ai l'impression qu'on s'en sort avec un comportement identique aussi
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.]) |
Beta Was this translation helpful? Give feedback.
-
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 |
Beta Was this translation helpful? Give feedback.
-
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.
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 |
Beta Was this translation helpful? Give feedback.
-
Il me semble que dans une "variations" on ne remonte actuellement pas les variables manquantes des branches non évaluées
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 à 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) |
Beta Was this translation helpful? Give feedback.
-
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) |
Beta Was this translation helpful? Give feedback.
-
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 :
Nombre
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
etsemaine
. Oukg
,g
,mg
,lb
etoz
.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 valide3 €/mois + 154 %
est une formule invalideOption 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 est de type #CDD
Le constructeur de type Possibilités permet de définir une union d'Option.
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)
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 estsynchronisation
.Par exemple, le cas de l'API commune peut être traité ainsi :
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).
Le type Valeur, correspondant à l'évaluation d'une règle de type T est le suivant :
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 :
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 :
Définit sur l'espace
(Evaluation(Nombre), Evaluation(Nombre))
somme
Pour le mecanisme somme, on a :
Definit sur
Evaluation(Nombre)[]
Questions ouvertes
Beta Was this translation helpful? Give feedback.
All reactions