Tu m'as un peu largué dans les types paramétriques.
Le problème dont je parle relève bien de ingénieries des modèles, j'avais l'impression que du point de vue du code, ce n'est qu'une structure de donné (à la con).
Imagines que tu dois documenter des messages qui circulent sur un bus de communication. Tu as une lib de base "définition des champs d'octet d'un message de communication". Elle contient, des informations comme : nom, offset et taille de champ, type du champs. Ensuite, tu veux faire le boulot pour une techno de bus particulière A429, tu va réutilisé cette lib pour dire que les 3 premiers bits ont tel nom, et ont une valeur fixe, et champ de donné de type int (genre un champ d'adresse sur 8 bits, et un champs de donné sur 18 bits).
Pour une instance particulière de ce bus A429, tu va réutiliser la lib de description A429, définir des types de messages, avec des champs fixes (littéraux) et d'autres dépendantes du message (genre le message de vitesse est à l'adresse 121 fixe, mais le contenu est un entier 16 bits en km/h, en virgule fixe avec 6 bits après la virgule).
Chaque lib peut être vue comme le type de la lib qui l'utilise, ce n'est pas une transformation de type vers un autre. C'est ce mélange entre type de base et littéraux qui est impossible et très chiant en pratique.
Tu me dis pourquoi se faire chier avec un système aussi compliqué ? Le coté formel permet plein de choses. C'est pratique pour vérifier que parmi les 1000 messages échangés sur un bus, l'émetteur et le receveur reçoivent la vitesse dans la bonne unité et dans le bon encodage. Voir que dans le cas contraire, de générer un convertisseur à la volé. Cela permet de générer de la documentation propre non ambigüe. Cela permet aussi de générer du code de génération de trame (ton "float64 speed" dans un code C, a mettre au bon endroit dans le message).
J'avais déjà essayé d'en parler sur linuxfr. J'ai tenté de faire un langage de description qui permet de faire. L'idée de base est simplement d'ajouter un opérateur "est compatible avec le type de", je le notait '~' ou même '=' dans les définitions.
Ainsi, tu écris 'int ~ 1 ~ Name "a"', pour définir un truc du nom de "a" qui est de type int et vaux 1. Cela permet de le composer en plusieurs fois.
Genre 'Ref "a" ~ 2', la référence à "a" dont on ajoute 2, ce qui est faux.
Ainsi je peux définir Name "message" ~ (Name "adresse" ~ int & Name "data") dans une lib de base.
Puis Name "messageVitesse" ~ Ref "message" ~ (Ref "message/adresse" ~ 121 & Ref "message/Data" ~ (Name "Value" ~ int && Name "unit" ~ ("km/h" || "m/s") )) dans une lib plus précise. Puis Name "MessageBusTartenpion" ~ (Ref "messageVitesse" ~ (Ref "message/data/unit" ~ "km/h") || Ref "messageDistance" ) etc...
Tu peux aussi gérer plusieurs noms ou des alias 'Name "Vitesse" ~ Ref "messageVitesse"'.
La où cela devient marrant, c'est si on introduit la négation. Genre int ~ (! 0), pour faire un entier qui n'est pas nulle.
J'avais tenter de faire un type checker de façon simple en Ocaml, c'est un boulot énorme. Je voulais le refaire en tagless qui me parait super puissant, mais je n'ai pas eu le temps. Ce langage que j'appelais "Grape" (ou Cherry mais je n'assume plus :) permet de remplacer le xml, la description d'un schéma et rajoute la notion de nommage pour faire des graphs orienté et pas seulement des arbres de données. Cela permet de faire la même chose que l'UML ou SysML mais en beaucoup plus simple et de façon formelle.
Depuis, j'ai aussi un peu changer d'avis : il n'est pas possible de "mélanger" les modèles. Si on peut jouer avec des types un "peu" différent, avec un typage "weak", il reste le problème de compositions structurelles que l'on ne peut pas mixer (par exemple, un modèle de donné l'UML et sa représentation graphique en widget ). En fait, il faut faire de la transformation de modèle vers un autre (description des messages vers sa représentation html avec une lib html comme base). On peut aussi avoir la même chose décrite avec 2 normes différentes (beaucoup de standard arrivent avec leur metamodèle UML). Mixer les 2 normes est complexe et si une troisième arrive... C'est plus simple de prévoir des transformations. Cela implique des aller-retour, et de la gestion de différence. Mais je n'ai pas encore de solutions, surtout si on part du principe que le modèle est gigantesque :)
[^] # Re: Reason
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche OCaml 4.04 et 4.05. Évalué à 3.
Tu m'as un peu largué dans les types paramétriques.
Le problème dont je parle relève bien de ingénieries des modèles, j'avais l'impression que du point de vue du code, ce n'est qu'une structure de donné (à la con).
Imagines que tu dois documenter des messages qui circulent sur un bus de communication. Tu as une lib de base "définition des champs d'octet d'un message de communication". Elle contient, des informations comme : nom, offset et taille de champ, type du champs. Ensuite, tu veux faire le boulot pour une techno de bus particulière A429, tu va réutilisé cette lib pour dire que les 3 premiers bits ont tel nom, et ont une valeur fixe, et champ de donné de type int (genre un champ d'adresse sur 8 bits, et un champs de donné sur 18 bits).
Pour une instance particulière de ce bus A429, tu va réutiliser la lib de description A429, définir des types de messages, avec des champs fixes (littéraux) et d'autres dépendantes du message (genre le message de vitesse est à l'adresse 121 fixe, mais le contenu est un entier 16 bits en km/h, en virgule fixe avec 6 bits après la virgule).
Chaque lib peut être vue comme le type de la lib qui l'utilise, ce n'est pas une transformation de type vers un autre. C'est ce mélange entre type de base et littéraux qui est impossible et très chiant en pratique.
Tu me dis pourquoi se faire chier avec un système aussi compliqué ? Le coté formel permet plein de choses. C'est pratique pour vérifier que parmi les 1000 messages échangés sur un bus, l'émetteur et le receveur reçoivent la vitesse dans la bonne unité et dans le bon encodage. Voir que dans le cas contraire, de générer un convertisseur à la volé. Cela permet de générer de la documentation propre non ambigüe. Cela permet aussi de générer du code de génération de trame (ton "float64 speed" dans un code C, a mettre au bon endroit dans le message).
J'avais déjà essayé d'en parler sur linuxfr. J'ai tenté de faire un langage de description qui permet de faire. L'idée de base est simplement d'ajouter un opérateur "est compatible avec le type de", je le notait '~' ou même '=' dans les définitions.
Ainsi, tu écris 'int ~ 1 ~ Name "a"', pour définir un truc du nom de "a" qui est de type int et vaux 1. Cela permet de le composer en plusieurs fois.
Genre 'Ref "a" ~ 2', la référence à "a" dont on ajoute 2, ce qui est faux.
Ainsi je peux définir Name "message" ~ (Name "adresse" ~ int & Name "data") dans une lib de base.
Puis Name "messageVitesse" ~ Ref "message" ~ (Ref "message/adresse" ~ 121 & Ref "message/Data" ~ (Name "Value" ~ int && Name "unit" ~ ("km/h" || "m/s") )) dans une lib plus précise. Puis Name "MessageBusTartenpion" ~ (Ref "messageVitesse" ~ (Ref "message/data/unit" ~ "km/h") || Ref "messageDistance" ) etc...
Tu peux aussi gérer plusieurs noms ou des alias 'Name "Vitesse" ~ Ref "messageVitesse"'.
La où cela devient marrant, c'est si on introduit la négation. Genre int ~ (! 0), pour faire un entier qui n'est pas nulle.
J'avais tenter de faire un type checker de façon simple en Ocaml, c'est un boulot énorme. Je voulais le refaire en tagless qui me parait super puissant, mais je n'ai pas eu le temps. Ce langage que j'appelais "Grape" (ou Cherry mais je n'assume plus :) permet de remplacer le xml, la description d'un schéma et rajoute la notion de nommage pour faire des graphs orienté et pas seulement des arbres de données. Cela permet de faire la même chose que l'UML ou SysML mais en beaucoup plus simple et de façon formelle.
Depuis, j'ai aussi un peu changer d'avis : il n'est pas possible de "mélanger" les modèles. Si on peut jouer avec des types un "peu" différent, avec un typage "weak", il reste le problème de compositions structurelles que l'on ne peut pas mixer (par exemple, un modèle de donné l'UML et sa représentation graphique en widget ). En fait, il faut faire de la transformation de modèle vers un autre (description des messages vers sa représentation html avec une lib html comme base). On peut aussi avoir la même chose décrite avec 2 normes différentes (beaucoup de standard arrivent avec leur metamodèle UML). Mixer les 2 normes est complexe et si une troisième arrive... C'est plus simple de prévoir des transformations. Cela implique des aller-retour, et de la gestion de différence. Mais je n'ai pas encore de solutions, surtout si on part du principe que le modèle est gigantesque :)
"La première sécurité est la liberté"