Type Checker

[TheoWinterhalter]

J'ai commencé à implémenter un type checker pour le langage de script.

Depuis mon dernier commit, le script de @VLanvin type correctement ! \o/

• Il reste néanmoins à gérer proprement le polymorphisme (pour l'instant le polymorphisme type mais en conséquence je suis trop permissif).
• Il me manque à préciser le type de retour de Init et Attack.
• La gestion des erreurs est minimaliste : si une variable n'est pas bound, le message donnera son nom, mais une erreur d'unification n'est pas plus précise que ça pour le moment... Il me reste donc à utiliser les locations.

Je pense par ailleurs que les term_types de l'arbre de syntaxe abstraite sont inutiles. Je suis prêt à en discuter, mais aussi prêt à les retirer.

[TheoWinterhalter]

J'ai enlevé le o ligne 13 du script pour pouvoir tester le message d'erreur avec les locations, mais le résultat est plutôt décevant :

Error in , from line 0 characters 0--1 to line 0 characters 0--1: variable/function dijkstra_t is unbound

Vraisemblablement, tout vaut 0 ou -1... @VLanvin est-ce normal ?

[VLanvin]

C'est réglé, j'utilisais les fonctions ocamlyacc au lieu de menhir... Je n'ai pas encore push, j'ai un autre souci avec les scripted_player pour le moment.

[VLanvin]

Maintenant que self/map/players/etc.. ne sont liées qu'à l'environnement du script et non à l'environnement global, le type checker lance des "unbound variable". Il faudra qu'on en parle pour trouver une solution, peut-être serait-il possible d'envoyer au type checker la liste de toutes les variables qui seront liées plus tard, et ce avec leur type ?

[TheoWinterhalter]

On ne peut pas les traiter comme "selected_unit" ?

[VLanvin]

Si on peut, de toute façon, qu'on envoie les variables en paramètres ou qu'on hardcode ça dans le checker, ça revient au même, ça sera forcément codé quelquepart.

[TheoWinterhalter]

J'attends que tu aies terminé ce que tu fais pour m'attaquer au polymorphisme ? Ou peut-être que je dois d'abord essayer de régler cette histoire de self etc. ? (Je pensais que j'avais ajouté manuellement self quelque part pourtant…)

[VLanvin]

J'ai réglé l'ajout de self/players/map/etc..., c'est tout hardcodé dans le type checker. Je pense que tu peux t'occuper du polymorphisme, je n'ai plus grand chose à faire de mon côté, à part peut-être quelques modifications de la syntaxe (rien de gênant pour toi). Au passage, le type de retour attendu pour le point d'entrée init est unit (pas soldier), et celui pour attack est Soldier.

EDIT -- Et c'est là que je me rend compte qu'on a un problème. Que doit-on retourner si on ne veut pas attaquer ? On peut peut-être exposer une fonction do_nothing qui finit le tour de l'unité (je pensais déjà faire ça pour terminer le tour du joueur).

[TheoWinterhalter]

Ça marche. Je vais faire ça.

Par contre, les locations sont pas encore correctes au niveau des caractères, j'ai :

Error in src/script/test.script, from line 15 characters 328-658 to line 15 characters 328-705: variable/function dijkstra_t is unbound

Il n'y a pas autant de caractères dans tout le fichier…

[EDIT : Okay, la doc était incorrecte, j'ai interprété un terme comme la taille alors qu'il correspondait à la fin, toujours est-il que le caractère indiqué correspond au nombre de caractères depuis le début du fichier.]

D'ailleurs, pourquoi est-ce un coupe de Lexing.position ?

[TheoWinterhalter]

Sinon, les tqui se trouvent dans l'arbre de syntaxe abstraite n'ont (pour moi) un intérêt que s'il y a des annotations de type, à priori on décide de s'en passer non ?

[VLanvin]

Le couple c'est pour avoir le début et la fin du terme qui pose problème (mais peut-être ai-je mal interprété la doc aussi ?) En fait je pensais que tu faisais l'unification en place dans l'AST, mais effectivement, si tu t'y es pris autrement tu peux tout aussi bien enlever les étiquettes.

[TheoWinterhalter]

Non, a priori je suis d'accord, mais pour le moment, sur mes tests, les deux valeurs sont toujours égales. Il faudrait que l'erreur concerne plusieurs lignes j'imagine.

Oui, en place j'ai l'impression que c'est difficile de faire linéaire. De cette manière, je parcours chaque noeud uniquement une fois.

Pour ce qui est des Soldiers, c'est plutôt embêtant, je laisse unit pour le moment car ton script d'exemple renvoie ça pour le moment.

[TheoWinterhalter]

J'ai rajouté la gestion des erreurs précises au langage de script dans la typechecker (et avec le If, j'ai réussi à avoir une erreur qui prenait plusieurs lignes !).

EDIT : Par contre, est-ce qu'on veut que ce soit affiché via un log ?

[TheoWinterhalter]

J'ai ajouté une gestion du polymorphisme pour les fonctions (leur type est donc exposé explicitement avec des _alphai, il n'y a pas d'inférence de type polymorphe).

Je ne suis pas sûr que ça fonctionne avec de l'ordre supérieur, si j'ai une fonction polymorphe qui prend en paramètre une fonction polymorphe, il y a peut-être un conflit (à réfléchir à tête reposée et réveillée).

En gros, le type checker est terminé à quelques petits détails près. Dès que le type de retour de tous les blocs est fixé on peut envisager un merge dans master non ? @VLanvin

[OlivierMarty]

Pourquoi il n'y a pas d'inférence de type polymorphe ? Je ne vois pas le problème... Pareil pour les fonctions d'ordre supérieur.

Est-ce que les problèmes soulevés sur le commit 5821635eff509eb5122f3027babeaaeeccfc13e0 sont résolus ? Par exemple le fait que la fonction print ne doit pas être spécialisée définitivement (en fait, toute fonction polymorphe...)

Je trouve que l'inférence de type ressemble beaucoup à ce qu'on avait pu faire en dm de programmation 2 l'année dernière (prolog), par exemple pour le polymorphisme je mettrais les alpha sous des lambdas (je me souviens d'un "le meilleur polymorphisme possible c'est les lambdas") ce qui permet de rafraîchir l'entier pour unifier une fonction polymorphe avec autre chose sans la spécialiser, et qui permet d'avoir le bon comportement quand l'alpha apparaît plusieurs fois dans le type. C'est le TODO de la fonction vt_to_tt

  | `Alpha_t i    -> ref `Alpha_tc (*TODO*)

Par exemple pour

let y = f 2 x

avec f : alpha -> beta -> alpha on a int <= alpha type de x <= beta alpha <= type de y Le tc peut produire une liste d'inéquations de sous-typage à résoudre...

[TheoWinterhalter]

Tu regardes quelle version du code @OlivierMarty ? Le TODO n'est plus présent maintenant.

Je fais le point :

Actuellement, le polymorphisme est géré pour les fonctions exposées de ocaml qui ont des types avec des alpha. Et je peux appeler deux fois la même fonction avec des alpha différents normalement. En revanche j'émettais des réserve sur ma gestion du polymorphisme concernant des fonctions d'ordre supérieur, mais normalement tout devrait bien se passer. (Mais ce n'est pas testé).

Sinon, la fonction print n'est quand même pas implémentée telle quelle. On pourrait l'envisager, quitte à afficher une string standard quand on ne sait pas afficher un objet. Son typage serait quand même possible.

Pour l'inférence de type polymorphe, je vois comment faire, mais je m'étais dit que c'était vraiment pas la peine de faire ce genre de truc dans l'IA.

Et oui, j'ai fait comme le projet de l'an dernier. ;)

[OlivierMarty]

D'accord j'étais sur une ancienne version...

Je ne comprends pas pourquoi il y a autant de références... Seul les `None visent à être modifiés non ?

Sachant qu'on utilise les toujours les mêmes entiers pour les fonctions polymorphiques (Alpha_t 0), qui sont directement traduit enAlpha_tc 0 on risque de vérifier que deux choses qui n'ont rien à voir ont le même type non ?

[TheoWinterhalter]

C'est là mon inquiétude sur l'ordre supérieur (et par là, j'entends, on a une fonction polymorphe en argument d'une autre), mais je pense que ça ne devrait pas poser de problème.

Justement, ici, alpha pointe sur une référence, on l'unifie peut-être, donc une autre variable de type peut la garder, même quand je supprime après la référence de alpha (pour détacher alpha du type unifié par l'appel).

[VLanvin]

Je viens de pusher un test pour l'ordre supérieur (quoi de mieux que les fonctions List.map et List.iter) et... ça ne passe pas.

Déjà, la fonction fun addone a = { a + 1 } type en any_type -> unit (j'ai l'impression), au lieu de int -> int. Du coup, le checker ne rale pas sur list_iter addone ["a";"b";"c"].

Ensuite, il lance une erreur sur list_map fst [(1,2);(4,5);(9,8)] qui pourtant est tout à fait correct.

Finalement (mais c'est un bug assez mineur), j'ai l'impression qu'il y a un problème de parenthésage quand tu affiches un type d'ordre supérieur.

[francoisthire]

Pourquoi tu fais pas un test avec oUnit ? Il y a une option pour spécifier qu'un test doit être vérifié mais que ce n'est pas encore le cas. C'est sur la page d'oUnit : documentation oUnit 2.0.

[TheoWinterhalter]

Tu peux me montrer un mauvais affichage ? Pour l'instant, je fais type1 -> (le reste).

Sinon, en effet, le type inféré pour addone est incorrect, je vais me pencher là-dessus. Merci.

[VLanvin]

Je regarde pour oUnit.

Pour le problème d'affichage, il y a alpha_0 -> (alpha_1) -> (alpha_0 list -> (alpha_1 list)) qui devrait plutôt être (alpha_0 -> alpha_1) -> alpha_0 list -> alpha_1 list.

[TheoWinterhalter]

Ah oui, il me faut aussi mettre entre parenthèses la gauche de la flèche.

[OlivierMarty]

Ça m'a l'air assez foireux. Moi j’enlèverais toutes les ref, et dans la fonction deref on va chercher ce qui correspond à un Alpha_tc. LesNone sont en fait des alpha frais ? Avec les `Pointer ça fait en fait une redondance de code par rapport à ce qui est géré maintenant avec les aplha ?

Dans vt_to_tt, il faut forcement attribuer des alpha frais... Je le ferais dans une fonction auxiliaire qui prend un environnement int -> int qui associe à un apha du type un alpha du type checker. Ou alors, un type polymorphe est mis sous un lambda int -> value_type qui permet de raffraichir l'identifiant.

[TheoWinterhalter]

Une variable de type est un pointeur sur une variable avec laquelle elle est unifié. Une fois unifié c'est à vie. C'est pour ça que je ne peux pas choisir le même système pour les alphas. En revanche, les None peuvent être assimilés à des alphas frais si tu veux (mais il s'agit plutôt des _alpha d'ocaml), je pourrais facilement en déduire un type polymorphe d'une fonction.

[TheoWinterhalter]

Et aussi les références sont, j'ai l'impression, nécessaires si je veux unifier deux variables. Comment la modifier sinon ?

De plus, cela a beau s'agir de pointeurs, il n'est pas possible de dire que deux variables indépendamment définies pointent vers la même case mémoire. D'où l'astuce du pointeur dans le type variant. Comme tu le remarquais @OlivierMarty, c'est ce qui était fait dans le projet l'an dernier.

Sinon, il y a clairement un bug, je le reconnais. C'est à priori une unification qui ne se fait pas (ou pas comme il faut). Je chasse cette erreur quand j'ai le temps.

[TheoWinterhalter]

Bon, maintenant la fonction addone est typée correctement, il reste un bug sur le polymorphisme. J'y retourne.

EDIT : Cette fois-ci le problème est celui que je mentionnais plus tôt. Si une fonction polymorphe est argument d'une autre fonction polymorphe, il y a quelques soucis. Je vais essayer de régler ça rapidement.

(@VLanvin, il n'y a pas de commentaires dans le script si ? Parce que là on empêche master de tourner).

[TheoWinterhalter]

J'avais oublié de préciser que maintenant c'est corrigé. Le polymorphisme est géré d'un point de vue des fonctions qui sont étiquetées comme telles (les exposées), en revanche, l'inférence polymorphe ne sera pas gérée (ce n'est pas aussi simple qu'il n'y paraît).