Typage de cinglé

Je préviens tout de suite, ceux qui ne programme pas ne seront pas intéressé par ce billet. Ceux qui ne connaissent aucun programme ML, (oCaml, Caml Light, Haskell,...) vous risquez d'être largué.

Il y a des cinglés, qui vouent une vénération au typage. Par exemple, un de mes ancien professeurs a écrit sur sa page I see a future where all programming is done in type safe languages or in assembly supplemented with safety proofs..

Le typage doit permettre de garantir certaine propriété. Je vais vous donner l'exemple le plus cinglé que j'ai, trouvé récemment. Je me demande si ça ne mériterait pas un dailyWTF peut être.

Là où je travaille, on a des termes, qui sont soit des variables (exemple: x, y, taille, etc.) soit des constantes (exemple: 42, pi, "hello world"), soit des application, i.e. un symbole de fonction appliqué à des termes (exemple: f(42), +(1,3), print("hello world").

On appelle ground term un term qui ne contient aucune variable. Il est très simple de typé un ground terme, c'est simplement, soit une constante, soit un symbol et une liste de ground terme (ses arguments)

Il est aussi simple de typer un terme quelconque, qui est soit une variable, soit une constante, soit une application.

Maintenant, vient le problème suivant: on veut des termes avec au moins une variable, comment s'assurer le respect de cette propriété par le typage?

Réponse: On crée un type supplémentaire: variable-term, qui est: soit une variable, soit un quadruplet composé d'un symbol de fonction, d'un entier, d'un variable-term et d'une liste de terme.

Si l'entier est i, alors, moralement, cela signifie que le ième terme est le variable-term, ce qui nous assure qu'on ait bien une variable quelque part. (Preuve triviale par récursion sur le terme). Et on décale de 1 la position de tous les termes au delà du ième, dans la liste.

Donc f,2,taille,("hello world",42,pi) signifie moralement f("hello world",42,2,pi).

Alors, c'est bien joli, mais ça devient très moche à utiliser. Mais le typage est sauf! Les cinglés sont contents, et moi je pense bientôt aller à l'asile si je continue à voir des choses comme ça.

Arthur Rainbow

PS: Le cinglé qui a eu l'idée de faire comme ça, c'est moi, mais le pire c'est que mon maitre de stage a trouvé que c'était une bonne idée, et a songé à effectivement implémenté les variables-terms comme ça maintenant.

PPS:Il y a quand même un problème qui reste, que seul le typage dépendant pourrait résoudre, mais pas le typage des langages ML, quelqu'un saura t'il me le trouver?

Commentaires

1. Le dimanche 12 juillet 2009, 21:28 par jjrousseau

Effectivement, ce genre de post me largue ...

JJR, largué

PS : vous êtes le héros de mon prochain post

2. Le dimanche 12 juillet 2009, 23:16 par N

Je te comprends. Ceci dit, je suis fan des langages fortement typés : l'exigence est forte mais permet de faire du bon boulot, et je me repère mieux dans des typages rigides. Je ne me suis encore jamais trouvé dans une position où j'étais obligé de bidouiller comme tu le fais.

En fait, je ne vois pas bien ce qu'est un 'variable-term'. En Ocaml, il y a un typage pour quelque chose de «non-évalué»... Et si je veux l'utiliser comme tu le proposes, alors je crée une structure qui me semble moins moche visuellement, comme un objet qui contient nécessairement une donnée de ce type. En gros, je m'arrange pour que ce soit agréable, quitte à créer une surcouche à mon code. Niark. Quitte à reformuler le problème ensuite, pour éviter ça justement.

À ta question : il faut que le typage de f soit cohérent avec le reste ?

3. Le lundi 13 juillet 2009, 01:30 par Arthur Rainbow

ce que j'appelle variable-term, c'est simplement un term dont un des sous-terme est une variable

f(42) serait ground terme, il n'y a pas de variable, alors que f(x) serait variable-term, puisque x est une variable.

Les deux sont des termes.

On peut faire une structure plutôt qu'un quadruplet, c'est moralement équivalent. La question est juste de s'assurer qu'il y a quelque part une variable.
Plus précisément, avoir un type qui type toutes les variables-terms, et qui ne type rien d'autre que les variables-terms

Pour information, la réponse à la question de mon PPS, c'est que si on dit que l'argument qui est de type variable-term est en 42 ème position, et que la liste des autres arguments contient uniquement 17 argument, on a un terme bien typé, mais qui n'ait pas bien construit.
On aurait besoin des types dépendants pour s'assurer que la position du variable-term est inférieur au nombre de terme de la liste. (Quoi que un tableau serait peut-être plus pratique)

Ta réponse n'était pas bonne dans mon cas, car f est simplement une chaine de caractère, sans type ni sémantique au niveau où je travaille.

4. Le lundi 13 juillet 2009, 11:30 par jjrousseau

Qaund je vous lis, j'ai l'impression que j'aurais du forcer un peu les traits de votre personnage dans mon histoire.

JJR

5. Le lundi 13 juillet 2009, 15:24 par Arthur RAINBOW

Je pense que ce n'est pas la peine JJR, en plus vous m'attribuez des connaisances dans des domaines où mon niveau s'arrête au livre de vulgarisation.

SInon, j'ai fini par trouver une solution plus belle, qui évite le problème dont je parlais
J'ai un quadruplet (ou une structure) composé de
Un symbol, une liste de ground-terme, un variable-terme et une liste de terme.

Moralement, c'est le symbole appliqué à la concaténation des ground-termes, du variable terme et des termes, et je m'assure que la position du variable terme qu'on a est aussi à gauche que possible.

Cela me donne l'équivalence entre égalité physique et sémantique, ce qui est génial, puisque j'utilise beaucoup de partage de mémoire (hashconsing)

6. Le mardi 14 juillet 2009, 12:40 par N

OK. Et effectivement, ta solution semble être nécessairement aussi compliqué, au vu des limites du problèmes.

Je n'ai jamais vu 'moralement' utilisé en français, c'est assez amusant à entendre/lire. Tu connais des gens qui disent ça en France ?

7. Le mardi 14 juillet 2009, 16:52 par Arthur Rainbow

Mon maitre de stage, à l'Inria de Saclay, n'arrête pas de dire ce que "moralement" les valeurs signifient

Et je crois que je lui ai piqué ce tic, tout comme dire sans arrêt "typiquement".

Typiquement, ceci est une phrase où je pourrais dire "typiquement", sans vraiment de raison.

Ajouter un commentaire

Le code HTML est affiché comme du texte et les adresses web sont automatiquement transformées.

La discussion continue ailleurs

URL de rétrolien : http://www.milchior.fr/blog/index.php?trackback/117

Fil des commentaires de ce billet