Sommaire
Obtenir du code correct par l'utilisation de types
Je vais illustrer cette idée avec un cas trivial mais pragmatique. Pour se mettre à un langage, rien ne vaut un petit projet perso, avant de passer aux choses sérieuses en regardant le code écrit par d'autres. Dans mon cas, il s'agit de l'écriture d'un utilitaire pour afficher des schémas Kicad et les différences entre deux versions (rien de gros ni professionnel comme GNU, comme dirait l'autre). Par avance, mes excuses aux grands maîtres d'Ocaml si j'écorche le langage ou ses concepts.
Les coordonnées sont représentées par des couples int*int, mais dans l'optique d'utiliser le typage, il était plus intéressant de différencier le type coordonnées d'une simple paire. En effet, rien n'est plus ressemblant à une paire d'entiers qu'une autre paire d'entiers. En Ocaml, par exemple, on peut définir des types qui sont synonymes du type « paire d'entiers » :
# type anon_coord = int*int;;
type anon_coord = int*int
# type anon_coord2= int*int;;
type anon_coord2= int*int
Mais alors les deux types sont synonymes aussi :
#let x:anon_coord = 5,7;;
val x : anon_coord = (5, 7)
# let y:anon_coord2 = x;;
val y : anon_coord2 = (5, 7)
J'ai donc opté dès le départ pour un type annoté, qui serait particularisé :
# type coord = Coord of (int*int);;
type coord = Coord of (int * int)
# let z = Coord (6,8);;
val z : coord = Coord (6, 8)
# let Coord (x,y) = z;;
val x : int = 6
val y : int = 8
Le type a alors un constructeur unique et l'annotation empêche de passer une simple paire là où on attend le type annoté. La déconstruction par pattern matching permet simplement d'accéder aux coordonnées individuelles.
L'affichage de schéma consiste à afficher les symboles des composants électroniques à certains emplacements ainsi que de primitives (lignes, textes). Ces composants sont décrits dans des fichiers bibliothèque et il est nécessaire de les translater et les tourner correctement dans le contexte du schéma. En fait, chaque symbole est décrit par un ensemble de primitives graphiques similaires à celle du schéma et qui doivent subir la même transformation pour obtenir la transformation du symbole.
Or, lors du codage de cette fonctionnalité, il est apparu assez rapidement que j'avais introduit des bugs qui faisaient que les primitives des composants étaient affichées sans subir de transformation, ce qui les collait toutes dans le coin supérieur gauche du schéma (un comportement de bug bien connu dès qu'on joue un peu à dessiner). J'aurais pu à ce moment dégainer le débugger ou ajouter quelques lignes de traces pour voir ce qu'il en était, mais le projet étant didactique, j'ai préféré recourir à une solution à base de typage.
J'avais utilisé le même type coord
dans le traitement du schéma et des bibliothèques, mais il parait plus judicieux de différencier ces types, car même si les bibliothèques de composant utilisent le même format de description que celles des fichiers de schéma, elles décrivent des coordonnées qui seront forcément relatives au point d'ancrage du composant dans le schéma. Il fallait donc créer un type annoté différent pour les coordonnées des primitives de bibliothèque, un type qui ne serait pas connu du canevas et qui permettrait de détecter un passage des primitives au canevas sans transformation.
# type relcoord = RelCoord of (int*int);;
type relcoord = RelCoord of (int*int)
Une fois le type injecté dans les types de primitives, merlin, l'outil de vérification à la volée indique dans l'éditeur tous les points qui nécessitent correction, indépendamment du fait que le comportement était correcte auparavant. Soit c'est une évolution de type et il faut changer le constructeur, au moment du parsing du fichier bibliothèque, ou l'utilisation, au moment d'injecter le composant dans le schéma, soit il y avait le bug et il faut ajouter la transformation adéquate pour transformer le type relcoord
en type coord
consommable par le contexte.
La beauté du truc, c'est que mis à part les oublis de transformation, j'avais tout codé correctement. Du coup, quand ça a compilé, ça a marché. Car c'est le compilateur qui m'a indiqué où se trouvaient mes bugs. Comparé à certaines pérégrinations de débogage de python dans certaines branches de traitement mal testées, je dois dire que ça a été une vraie bouffée d'oxygène et un argument supplémentaire pour coder plus en ocaml.
Quelques commentaires sur cette aventure
L'utilisation de types annotés n'introduit pas de code supplémentaire ou d'utilisation d'espace mémoire dans l'exécutable. Une fois la vérification de type effectuée, les types annotés sont identiques aux types synonymes à l'exécution.
L'injection du Relcoord est moins invasive qu'il n'y parait. Ocaml a l'inférence de type, ce qui limite les besoins à la définition des types internes du module de gestion des bibliothèques de composants de Kicad, et aux constructeurs et déconstructeurs. La création d'opérations au niveau d'abstraction Coord, Relcoord tels que
val +$ : coord -> relcoord -> coord
val rotation : relcoord -> relcoord
et le fait que la plupart des fonctions sont déclarées sans spécification de type diminue grandement le volume de la migration.
On peut (doit ?) pousser le concept plus loin, comme par exemple écrire une bibliothèque de calcul matriciel qui vérifie à la compilation la dimensionnalité des calculs.
Cela à un rapport (très simplifié) à la preuve de programme. Ainsi, à présent, je peux garantir qu'aucun composant électronique ne peut être passé directement à l'affichage. C'est une garantie sans intérêts pour l'utilisateur, mais on peut imaginer saisir dans les relations entre les types des garanties susceptible d'intéresser l'utilisateur, par exemple, que l'application ne fournit pas à un tiers les informations que je lui fournis.
À ma connaissance, seuls les langages fonctionnels typés offrent cette possibilité de différencier des types structurellement identiques, autrement qu'en faisant des classes.
# Go
Posté par ɹǝıʌıʃO . Évalué à 4.
En Go, les types qui ont la même structure ne sont pas synonymes, mais on peut transtyper très facilement. C’est effectivement très pratique pour vérifier qu’on écrit bien ce qu’on veut dire, mais parfois quelque peu pénible, par exemple quand on doit tout le temps passer de []byte à string et vice versa, ou quand les types deviennent un peu compliqués.
[^] # Re: Go
Posté par Guillaum (site web personnel) . Évalué à 5.
C'est cool ça.
En Haskell, le
newtype
est un type équivalent, mais non compatible :Après on peut convertir un
Int
enMyInt
de plusieurs manière, en utilisant le constructeur, par pattern matching ou via des casts sécurisés.Dans d'autres langages, ce serait contraignant car il faudrait écrire toutes les méthodes / fonctions associées. En haskell, on peut lui demander de dériver automatiquement tout comportement (
class
) implementée par le sous type.Exemple, si on veut faire un sous type qui se comporte comme un
String
(au moins pour certaines opérations) mais qui n'est pas compatible avec uneString
:Monoid
fournissant la concaténation de chaîne via(<>)
,Show
fournissant l'affichage.Eq
etOrd
fournissant respectivement les relations d'égalité et d'ordre. Cet exemple utilise l'extensionGeneralizedNewtypeDeriving
.Ce genre de chose est malheureusement difficile à réaliser dans d'autre langage, et souvent il faut réaliser une classe englobante et propager toutes les méthodes intéressantes, c'est beaucoup de code lourd pour pas grande chose.
En C++ on peut s'en sortir avec des types phantoms :
Mais cette solution devient vite embêtante quand on veut pouvoir définir un sous ensemble d'opération pour chaque type. Par exemple, l'addition entre deux couleurs peut avoir du sens, alors qu'entre deux positions ?
À ce niveau, la meilleur solution que je connaisse c'est de faire une classe
Point
qui contient toutes les opérations nécessaires, et des classesPosition
,Direction
,Couleur
qui encapsulent unPoint
de manière privée et qui n'exposent que les fonctions nécessaires.[^] # Re: Go
Posté par reno . Évalué à 5.
Hum, Ada?
# Module et type abstrait
Posté par kantien . Évalué à 5.
Il existe un autre moyen, pour éviter les alias entre types structurellement identiques, qui consiste à passer par le système de modules et les type abstraits. Ta solution, bien que résolvant ta problématique, rajoute une indirection en mémoire : tes types sont des pointeurs sur des couples de
int
(qui n'ont pas la même étiquette et ne sont donc pas identiques). Afin d'éviter ce pointeur, on peut utiliser des modules dans lesquels les types seront directement des couples mais en le cachant au monde extérieur.Exemple :
Ici, comme l'interface des modules définit un type t sans rien dire sur lui (on parle de type abstrait), les types
A.t
etB.t
sont incompatibles, bien que structurellement identiques.Ensuite, il est aisé, à partir des primitives des modules, d'écrire des fonctions de conversions d'un type dans l'autre :
P.S : tout système de types, quelque soit le langage, a à voir avec la preuve de programme, mais là c'est une autre histoire. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Module et type abstrait
Posté par Perthmâd (site web personnel) . Évalué à 4.
Pas forcément, ça dépend de la manière dont le type est écrit. Si tu écris
type coord = Coord of (int * int)
la représentation sera un constructeur à un argument (i.e. un 'fat pointer') vers une paire d'entiers (soit au total 5 mots mémoire). Si tu écris au contraire
type coord = Coord of int * int
sans les parenthèses, cela sera représenté par un constructeur à deux arguments entiers (soit au total 3 mots mémoire) ce qui est strictement équivalent en mémoire à un terme de type
int * int
.[^] # Re: Module et type abstrait
Posté par Aluminium95 . Évalué à 1.
C'est monstrueux ! Je suis curieux, ce comportement est documenté quelque part ?
[^] # Re: Module et type abstrait
Posté par Thomas Douillard . Évalué à 0.
Curryfication ?
[^] # Re: Module et type abstrait
Posté par Perthmâd (site web personnel) . Évalué à 4.
Pas vraiment, la curryfication c'est juste l'isomorphisme A × B → C ≅ A → B → C, et il n'y a pas de type fonctionnel impliqué ici. Ici ça serait plutôt genre l'associativité du produit ou un truc comme ça.
Fun fact: la curryification n'est pas valide en call-by-value avec effets (donc en particulier en OCaml). Il y a plus de monde dans A → B → C que dans A × B → C. Exemple:
fun (x : unit) -> (raise Exit : unit -> unit)
ne peut pas être écrite comme une fonction de la formefun (x, y) -> qqch
.[^] # Re: Module et type abstrait
Posté par Aluminium95 . Évalué à 1.
Notons que pour la même raison il y a aussi une différence entre A×B et B×A: à cause des exceptions et de l'ordre d'évaluation de la paire en call-by-value.
[^] # Re: Module et type abstrait
Posté par Perthmâd (site web personnel) . Évalué à 3.
Ce n'est pas monstrueux, c'est le comportement uniforme des types inductifs. Le seul point un peu subtil vient du front-end, qui fait que dans la syntaxe des arguments des types inductifs, les parenthèses sont signifiantes à toplevel. On peut s'en rendre compte en pratique en écrivant :
C'est implicitement spécifié dans la syntaxe formelle de la description des types inductifs, qui dit bien que ça prend une expression de la forme
typexpr1 * ... * typexprn
et pas juste untypexpr
.Ceci dit, avec les dernières version d'OCaml on peut commencer à faire des trucs vraiment gorky en utilisant des attributs
unboxed
pour compiler certains types sans les indirections intermédiaires. Heureusement c'est opt-in, et c'est pas observable dans le langage de toute façon. Seuls les gens qui font des bindings C doivent faire gaffe à ce genre de truc, ou à la rigueur si le programme est vraiment tendax sur les perfs.[^] # Re: Module et type abstrait
Posté par JN . Évalué à 1.
Et du coup, ça veut aussi dire qu'on ne peut plus passer une paire pré-existante au constructeur. Par contre le message d'erreur est vraiment contre-intuitif…
Sur la dernière ligne, on comprends qu'on passe un argument unique, qui est une paire…
[^] # Re: Module et type abstrait
Posté par kantien . Évalué à 2.
Il est vrai que la notation pour l'application des constructeurs de types inductifs peut apparaître contre intuitive, car elle n'est pas consistante avec celle des fonctions : c'est parce que en OCaml, on ne peut pas faire d'application partielle sur un constructeur de type (contrairement à Haskell, il me semble). Résultat les paramètres se passent entre parenthèses, comme en python par exemple.
Pour la taille mémoire, 5 ou 3 mots, cela se voit ainsi : un type somme occupe 1 mot mémoire qui contient des informations sur entre autre la structure des paramètres, plus 1 mot par paramètre. Ainsi dans le cas
Coord of (int * int)
, on a 1 mot + 1 mot pour le paramètre qui pointe sur une paireint * int
, paramètre qui contient lui même 1 mot de « tag » et 1 mot pour chaqueint
; d'où un total de 5 mots avec une indirection. Dans le casCoord of int * int
, on a 1 mot de « tag » plus 1 mot par paramètre, soit un total de 3 mots.Si tu veux pouvoir créer une variable de type
Coord of int * int
à partir d'une paire préexistante, il faut passer par un «smart » constructeur, c'est-à-dire une fonction de qui prend une paire et renvoie une valeur du bon type (à l'instar de mes fonctionsmake
dans mes exemples avec modules).Sinon pour revenir sur l'approche modulaire, un de ses intérêts pourrait être, dans un premier temps, de te familiariser avec le système de module. Ensuite, tu pourrais jeter un œil sur les fonctions qui prennent des modules comme arguments pour retourner des modules, ce que l'on appelle des foncteurs. Comme ton projet consiste à afficher des schémas kicad, je vais comparer cela à l'électronique. Quand tu fais un schéma de circuit, certains composants peuvent être remplacés par d'autres tant qu'ils fonctionnement de la même façon : c'est cela un module, un composant. Et ton foncteur, c'est le schéma de ton circuit qui décrit comment les assembler pour fabriquer un nouveau composant. Si dedans tu as un micro contrôleur, tu peux opter lors de la réalisation entre des modèles de différents fabricants (qui peuvent différer sur leur structure interne) tant qu'ils réalisent la même fonction et exposent la même interface.
Si je reprends mon interface de coordonnées en lui ajoutant quelques fonctions :
On peut l'implémenter avec des couples ou des paires (enregistrements) :
Comme ils définissent un type
t
et une fonction de comparaisoncompare
, tu peux obtenir directement un module pour gérer des ensembles de coordonnées, en utilisant le foncteur du module Set de la bibliothèque standard :Tu peux voir ça comme si ton module offrait plusieurs pins en interface et que tu routes certains d'entre eux (le type
t
et la fonctioncompare
) vers une partie de ton circuit pour avoir des ensembles. Mais dans la pratique, tu peux choisir un modèle de composant plutôt qu'un autre pour des raisons de performance (bien que dans mon exemple bateau, les deux doivent être sensiblement identiques une fois compilés).Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Module et type abstrait
Posté par serge_sans_paille (site web personnel) . Évalué à 6.
j'ai ri :-)
[^] # Re: Module et type abstrait
Posté par kantien . Évalué à 3. Dernière modification le 15 janvier 2017 à 14:19.
Intéressant, je ne savais pas qu'il y avait une différence entre les deux écritures au niveau de la représentation mémoire. Je croyais qu'au niveau du compilateur, il y avait juste des passes d'optimisation au niveau des phases de constuction-deconstruction pour réduire le nombre de suivi de pointeurs. Et cette « curryfication » des constructeurs, elle est faite pour tous les types de tuples ?
Edit : c'est bon, j'ai ma réponse dans ton commentaire en réponse à Aluminium.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Module et type abstrait
Posté par gasche . Évalué à 3.
Je pense qu'il est souvent prématuré de se poser des questions de représentation mémoire quand on écrit un programme—à moins de savoir d'avance que le type sera impliqué dans les parties les plus coûteuses en performance.
Par ailleurs, comme Permhmâd l'a mentionné, un constructeur à plusieurs argument
a la même représentation qu'un typetype t = Foo of bar * baz * foobar
(bar * baz * foobar)
. Du coup on a une indirection seulement avec un constructeur à un seul argument
et depuis OCaml 4.04 (Novembre 2016), on peut écriretype t = Foo of bar
pour supprimer l'indirection dans ce cas. (C'est utile pour packer des existentiels sans indirection.)type t = Foo of bar [@@unboxed]
[^] # Re: Module et type abstrait
Posté par kantien . Évalué à 2.
C'est vrai, d'autant que j'ai parlé trop vite sur le coup mémoire. Là, s'il veut réduire les coûts, il peut garder son code actuel, enlever les parenthèses autour du couple dans sa définition de type et utiliser des fonctions de constructions là où il construisait en partant d'une paire existante.
Je ne connaissais pas cette nouveauté, c'est intéressant.
Par contre, j'ai une question. Lorsque dans le journal, il s'interroge sur :
Ce contrôle statique ressemble à des types dépendants (un type paramétré par une valeur du langage, ici un
int
pour la dimension des matrices). Pour ce cas, ça doit pouvoir se faire avec des GADT comme dans les exemples du cours de Jeremy Yallop; mais c'est un usage assez avancé du système de type. Me trompe-je ?Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Module et type abstrait
Posté par octachron . Évalué à 2.
Cela dépend beaucoup ce que tu entends par "ce cas" et pouvoir se faire:
il est possible d'encoder les entiers naturels dans le système de type d'OCaml, avec des GADTs ou des types fantômes; cependant la complexité de l'encodage a tendance à s'accroître rapidement avec l'expressivité dudit encodage.
Par exemple, l'encodage le plus simple
fonctionne mais à plusieurs limitations majeures:
la taille du type augmente linéairement avec l'entier, ce qui peut créer des problèmes pour le compilateur assez rapidement ( il avait tendance à planter vers 65000 lors de mes derniers tests? )
les opérations que l'on peut effectuer sont très limitées.
Mais il peut être suffisant pour encoder un certain nombre d'invariants en algèbre linéaire (par exemple, on peut vérifier que les dimensions des matrices dans le produit matriciel soient correctes). Par contre, si je souhaite concaténer deux vecteurs, j'aurai
besoin d'encoder l'addition d'entier dans mon type
'nat1 t -> 'nat2 t -> ('nat1 + 'nat2) t
?Cependant, avec cet encodage, le système de type n'a pas assez d'information pour construire le type
'nat1 + 'nat2
, il faut soit passer par des types auxiliaires, ou modifier l'encodage des entiers. Un exemple qui marche est d'encoder des propositionsde la forme
a + b = c
:À partir de cet encodage, on peut écrire l'addition
Cependant, le paramètre de type libre
'a
a tendance à créer des problèmes du au fait que le GADT n'est pas covariant, donc la relaxed value restriction ne s'applique plus etil est très (trop) facile de se retrouver avec des types faibles.
Et la complexité ne fait qu'empirer si on essaie d'implémenter d'autres fonctionnalités (représentation binaire, multiplication, comparaison, etc …) sur les entiers dans le système de types.
Un bon exemple de ce qui peut être fait raisonnablement dans le cadre de l'algèbre linéaire est SLAP.
Un exemple pédagogique pour montrer à quel point le budget de complexité peut exploser facilement serait ma bibliothèque expérimentale tensority.
[^] # Re: Module et type abstrait
Posté par kantien . Évalué à 3.
Je pensais effectivement à l'encodage sous la forme des entiers de Peano. Comme c'est une représentation unaire des entiers, leur taille croît bien linéairement. C'est aussi cet encodage qui est illustré dans le cours de Jeremy Yallop.
L'idée est bien de montrer qu'avec les GADT, on peut avoir une forme affaiblie de type dépendant. Pour avoir des types dépendants complets, il faut passer à des langages comme Coq; mais là, c'est pour les fous ! :-P
Merci pour les deux liens, je regarderai cela à tête reposée.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Module et type abstrait
Posté par Michaël (site web personnel) . Évalué à 4.
Dans le cas de Abach j'implémente actuellement le calcul matriciel en adoptant un angle un petit peu plus géométrique. Étant donné des espaces vectoriels de dimension finie
A
etB
munis de bases un foncteur décritHom(A,B)
qui, puisque les espaces ont une base privilégiée, est exactement l'espace vectoriel des matrices représentant une application linéaire deA
dansB
. Puisque le type est abstrait, c'est la signature de l'application de composition qui garantit qu'on ne compose que des applications linéaires d'une manière qui résulte en une multiplication de matrices aux dimensions compatibles.Cette méthode oblige à introduire des notations pour les espaces vectoriels manipulés – ce qui est pour moi précisément le but recherché – avec des choses du genre:
Un “effet de bord” de cette méticulosité est que le système de type permet de contrôler la justesse sémantique des opérations effectuées tout en gardant une notation proche de celles que peuvent utiliser les mathématiciens qui ne fait pas intervenir de notions plus exotiques comme les GADT.
# Type fantôme
Posté par chimrod (site web personnel) . Évalué à 2.
Punaise, j'avais commencé à écrire un commentaire en se basant sur les types fantômes (ajouter une information qui n'est valable que du compilateur pour restreindre un type trop ouvert) mais ça ne marche pas !!
Bon, je poste quand même la tentative pour l'histoire…
le 'a indique ici un type abstrait, qui doit être nécessairement renseigné pour être utilisé, ce que nous allons faire :
Malheureusement, les deux types ne sont pas incompatibles comme on pourrait le croire :
C'est dommage, je me serai attendu à plus de sûreté sur ce plan là de la part du langage !
[^] # Re: Type fantôme
Posté par octachron . Évalué à 3.
Utiliser des types fantômes peut fonctionner, il faut faire cependant attention à quelles égalités de types on rend visible.
Effectivement, si on exporte l'égalité complète
il est possible de jongler entre les différentes valeurs du paramètre fantôme.
Mais c'est du au fait que le système de type se rappelle qu'au final
'a t ≡ int * int
.Pour éviter ce problème, on peut cacher cette égalité de type, soit partiellement
soit complètement
Dans les deux cas, l'égalité de type n'est plus visible, et
est rejetée comme invalide.
[^] # Re: Type fantôme
Posté par JN . Évalué à 1.
Juste une question: Pourquoi déclarer un type fantôme si on utilise déjà les modules et les types masqués ?
[^] # Re: Type fantôme
Posté par kantien . Évalué à 2. Dernière modification le 18 janvier 2017 à 14:18.
Pour rendre deux instances du type
'a P.t
incompatibles, en choisissant des types incompatibles pour la valeur du type fantôme (int
etfloat
dans les exemples de octachron).Dans l'usage des modules que j'ai proposé, on avait deux modules
A
etB
dont les types étaient incompatibles : bien que structurellement identiques, comme ils étaient abstraits, les typesA.t
etB.t
étaient incompatibles.Dans l'approche avec type fantôme, il n'y a qu'un seul module et les types
a P.t
etb P.t
sont rendus incompatibles par un choix adapté du type fantôme. Un des avantages que je vois, au premier abord, par rapport à ma solution, et que cela évite de dupliquer (dans deux modules distincts) les fonctions qui opèrent sur les types en questions. Tu pourrais, par exemple, définir deux type vides :puis faire un module de coordonnées :
et définir tes variables avec des annotations comme cela :
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Type fantôme
Posté par octachron . Évalué à 1.
L'intérêt que je vois au type fantôme, c'est qu'ils permettent de rafiner un type de base, en rajoutant potentiellement de l'information connue à la compilation, et ensuite de définir des jeux de fonctions qui utilisent −optionnellement− cette information supplémentaire, le tout en gardant explicite qu'il s'agit du même type de base.
Par exemple, on pourrait imaginer un type liste augmenté d'une information sur le fait qu'elle soit triée ou non
À partir de là, je peux raffiner les fonctions sur les listes pour rajouter de l'information:
Cela permet aussi de définir des fonctions qui requiert en entrée des listes triées, ce que le type fantôme permet de garantir
Mais la grande différence par rapport à avoir deux types abstraits, c'est qu'il est beaucoup plus simple de partager les fonctions entre les différents sous-types dans les cas où ces fonctions n'ont pas besoin de l'information supplémentaire:
Un autre point sur lesquels des types fantômes peuvent être intéressant, ce sont les bindings avec des bibliothèques extérieures en C. Les types fantômes peuvent permettre d'introduire un typage correct sans trop s'éloigner de la représentation en C. Par exemple, j'avais utilités dans un prototype de bindings OpenGL des types fantômes pour typer les enums et handles opengl, qui sont tous des entiers dans la représentation C. Ce qui permet de transformer
en
et de s'assurer que système de type d'OCaml vérifiera à notre place que seulement des identifiants valides seront passés à l'API OpenGL; tout en pouvant facilement repasser à des entiers non typés au besoin.
[^] # Re: Type fantôme
Posté par gasche . Évalué à 3. Dernière modification le 15 janvier 2017 à 21:16.
Octachron a répondu sur comment éviter ce comportement. Remarque que ce comportement est une bonne chose. Je peux définir
et je suis bien content de pouvoir aussi utiliser la fonction
int_of_bool
à la fois au typebool function_to_int
etint function_from_bool
, donc que ces deux types soient égaux.[^] # Re: Type fantôme
Posté par chimrod (site web personnel) . Évalué à 2.
Merci pour les explications ; c'est vrai que cela fait sens avec l'exemple que tu donnes. Finalement, j'ai bien fait de poster mon commentaire quand même !
L'usage du type fantôme, tel que corrigé par octachron est une solution élégante au problème soulevé dans le journal : puisqu'il s'agit d'un problème qui se pose uniquement à la compilation, autant enrichir le programme avec des annotations, sans pour autant enrichir le format des données.
D'ailleurs, à ce sujet, il est possible de l'exporter dans d'autres langages, ce qui prend l'affirmation donnée dans le journal à contre-pied :
Par exemple, voici un exemple en java dans lequel le type fantôme est transformé en paramètre d'une classe générique :
Le principe est le même, on enrichi notre type (ici notre classe), avec des informations qui n'ont pas de rapport avec les données contenues, mais qui permettent d'indiquer au compilateur ce que l'on autorise ou non. Bizarrement, je vois rarement de code java mettre en œuvre cette pratique, qui me paraît pourtant être une manière presque naturelle…
[^] # Re: Type fantôme
Posté par barmic . Évalué à 3.
Pour le cas présent je me demande s'il faudrait pas plutôt inverser. Avoir un type paramétré
Coord
et utiliser le paramètre pour indiquer dans quel repère il s'applique. J'avoue, j'ai jamais imaginer utiliser la généricité pour ça, mais c'est une bonne idée.Tous les contenus que j'écris ici sont sous licence CC0 (j'abandonne autant que possible mes droits d'auteur sur mes écrits)
[^] # Re: Type fantôme
Posté par Aldoo . Évalué à 2.
Je suis peut-être un peu naïf, mais dans les langages objet, l'idiome naturel pour arriver à cette fonctionnalité c'est d'utiliser l'héritage (à moins que je n'aie pas compris ce qu'on cherchait à faire), exemple en Java :
Clairement, on peut avoir des méthodes acceptant B mais pas C ou vice versa.
B et C ne jouent que le rôle de marqueurs (comme les types fantômes, non ?) et A, étant abstract, ne peut pas être instancié directement tel quel (tout comme les types dépendants en OCaml ou ailleurs).
Bien sûr on peut aussi faire avec des génériques, mais ça me paraît moins naturel d'introduire un paramètre de type qui ne sera jamais utilisé à l'intérieur de la définition du type.
Plus haut, dans le journal, je vois la mention "autrement qu'en faisant des classes". Je ne comprends pas cette remarque. Les classes sont la façon normale, parfois la seule, de définir la structure d'un type dans un langage objet (on pourrait remplacer "classe" par "interface", mais j'imagine que ça ne change rien à la remarque). On ne peut pas reprocher à un langage non-fonctionnel de ne pas disposer de syntaxes de définition de type à la façon "langage fonctionnel".
# Pas mal
Posté par barmic . Évalué à 3.
J'ai déjà fais ce genre de trucs avec des classes, quand je sens que je dois jongler avec des concepts un peu trop proches et que je sens que je vais me planter quelques part. C'est toujours hyper efficace.
Tous les contenus que j'écris ici sont sous licence CC0 (j'abandonne autant que possible mes droits d'auteur sur mes écrits)
# Caclul symbolique en OCaml
Posté par Michaël (site web personnel) . Évalué à 3. Dernière modification le 18 janvier 2017 à 10:41.
Je profite de ta remarque pour mentionner Abach un projet de calcul scientifique en OCaml. Ma motivation est de développer un outil qui permet le calcul formel (polynômes à plusieurs variables, quotients, algèbre linéaire…) sur des objets proches de la formulation mathématique des problèmes – là où la plupart des systèmes de calcul formel demandent de tout transformer en objets basiques du système, ce qui est une opération parfois difficile. Mon but est de pouvoir calculer bientôt des tables de multiplication pour les algèbres de Lie de petit rang puis des choses plus complexes comme les décompositions de Bialinicky-Birula de petites représentations ainsi que de pouvoir travailler sur les corps finis.
Un point sympa du programme est que les structures sont capables de transformer leurs éléments en formules TeX, comme illustré par la capture d'écran ci-dessus (en utilisant MathJax).
Côté code, voici un extrait du programme example générant la sortie ci-dessus:
[^] # Re: Caclul symbolique en OCaml
Posté par gipoisson . Évalué à 1.
Ça me rappelle l'article “Towards an Implementation of a Computer Algebra System in a Functional Language” d'Oleg Lobachev et Rita Loogen qui ont fait le même constat que toi : la majorité des systèmes de calcul formel (SCF) sont au moins diglotte, un langage interne servant à implémenter le SCF tandis que des langages externes constituent le moyen par lequel on interagit avec le SCF.
Les auteurs ont alors émis l'idée de mettre en place des SCF unifiant les dialectes internes et externes dans un langage fonctionnel. Leurs travaux étaient plutôt orientés du côté des algorithmes et sont reflétés dans Eden. Du côté des SCF, leur article m'a fait découvrir GiNaC qui réalise l'unification des dialectes en C++. Par exemple, dans le ginsh, ton premier exemple serait rendu comme ici-bas, cette syntaxe C++ reste la même en interne.
Dans l'article, un autre SCF est mentionné : DoCon qui faisait l'unification en Haskell. Depuis, il a évolué en DoCon-A qui est écrit en Agda. Dans le guide d'utilisation du système, le XVIIe chapitre paraît indiqué pour tes deux derniers exemples. Si tu parles du Haskell, DoCon-A est fait pour s'entendre avec Abach !
[^] # Re: Caclul symbolique en OCaml
Posté par Michaël (site web personnel) . Évalué à 2.
Merci pour toutes ces références, elles me seront très utiles!
[^] # Commentaire supprimé
Posté par mickeya . Évalué à -2. Dernière modification le 06 juillet 2017 à 09:54.
Ce commentaire a été supprimé par l’équipe de modération.
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.