Limitations du polymorphisme à la ML pour une machine à pile

Bonjour,

Dans le cadre de mon travail, je dois encoder une machine à pile. Cette dernière gère une pile que l’on peut manipuler grâce à des commandes. Pour l’exemple que je vais montrer, on va considérer que notre machine ne peut contenir que des entiers et des listes d’entiers que l’on peut manipuler grâce à 4 commandes :

• Empty : créer la pile vide
• Int(n) : empile l’entier n sur la pile
• Nil : empile la liste vide
• Cons : dépile une liste l, dépile un entier n et empile une nouvelle liste n::l

Ainsi le programme suivant :

1
2
3
4
5
6

Empty
Int(2)
Int(5)
Nil
Cons
Cons

contient sur le sommet de la pile la liste [2;5]. Par contre le programme suivant :

1
2
3
4
5
6

Empty 
Int(2)
Nil
Cons
Int(5)
Cons

n’est pas un programme valide. Passons au monde de la programmation, et pour ce cas d’étude on va prendre le langage OCaml. Ce qui m’intéresse ici c’est juste le type des instructions (Empty, Nil, …), pas comment on éxécute le programme. Une première façon de représenter les types est la suivante :

1
2
3
4
5
6
7

type instr = 
| Empty
| Int of int
| Nil
| Cons

type program = instr list

Avec cette représentation, on peut écrire notre premier programme, et ce n’est pas très compliqué de créer une fonction qui évalue ce programme. Cependant, on peut aussi écrire le second premier programme avec ce format, et cette fois l’évaluation dudit programme va planter.

On peut se poser la question cependant, si on ne pourrait pas statiquement détecter que le second programme est incorrect. En fait si on peut, et pour cela on va utiliser les GADTs. Si vous ne savez pas ce que c’est, je vous invite à aller regarder ce lien.

On va donc en utilisant les GADTs encoder ce qu’il y a sur notre pile. Pour cela on se donne deux nouveaux types :

1
2

type empty
type ('a, 'b) stack

empty correspond au type de la pile vide. ('a, 'b) stackcorrrespond au type de la pile qui contient à son sommet un objet de type ’a et le reste de la pile est ’b.

Ainsi la pile vide correspond à empty , la pile qui contient à son sommet les entiers 2 et 5 : (int, (int, 'b) stack) stack. Deux remarques sur ce type :

• la pile qui contient 2 et 5 est indistinguable de la pile qui contient 3 et 4 par exemple. Mais ici c’est attendu car on s’intéresse qu’au type des objets pour savoir si un programme est valide.
• le type est polymorphe en 'b ce qui veut dire que l’on ne sait rien sur ce qu’il y a ensuite

Pour une raison obscure (si quelqu’un veut bien m’expliquer je suis preneur), il faut rajouter un constructeur à succ pour que la suite soit bien typée :

1
2

type empty
type ('a, 'b) stack = Wtf

Maintenant on se donne le type des instructions :

1
2
3
4
5

type 'a instr =
  | Empty : empty instr
  | Int : int * 'a instr -> ((int, 'a) stack) instr
  | Cons : ('b list, ('b, 'a) stack) stack instr -> ('b list, 'a) stack instr
  | Nil : 'a instr -> ('b list, 'a) stack instr

On note que le type instr a maintenant un paramètre polymorphe, le type de notre pile. De plus, tous les constructeurs prennent un paramètre : la pile qui a été construite précédement. En un certain sens, le type 'a instrest une généralisation du type 'a list. Par exemple pour Cons ce dernier mange une pile qui contient à son sommet une liste dont les éléments sont de type 'b et un élément de type 'b et ressort une nouvelle pile qui contient cette fois seulement une liste de type 'b.

Maintenant, je peux encoder mon premier programme comme :

1

let _ = Cons(Cons(Nil(Int(5,Int(2,Empty)))))

Par contre, si j’essaye de faire la même chose pour le second programme :

1

let _ = Cons(Int(5,Cons(Nil(Int(2,Empty)))))

OCaml nous sort une erreur de type. On a donc gagné !

Well…

Essayons de se faire une petite fonction : mk_list. Cette dernière prendrait une liste d’entier OCaml et construirait un programme qui contiendrait les instructions pour créer cette pile. Le prototype de notre fonction serait le suivant :

1

'a instr -> int list -> (int list, 'a) succ instr

Le premier paramètre vient du fait que notre programme est censé fonctionner sur toutes les piles. Vous remarquerez que dans les constructeurs de Nil et Cons je n’ai pas précisé le type des listes. En effet, on pourrait imaginer qu’ensuite notre machine manipule aussi des listes de string par exemple. Donc on pourrait aussi vouloir créer une fonction mk_list de type

1

'a instr -> ('a instr -> 'b -> ('b, 'a) succ instr) -> ('b list, 'a) succ instr

Je vous invite à essayer 5mn de programmer ces prototypes, mais n’essayez pas trop longtemps. Je soupçonne très fortement que ce ne soit pas possible d’implémenter ces fonctions avec ces prototypes.

Si vous avez des idées pour implémenter mk_list (quitte à modifier le prototype) je suis preneur.

Je vous souhaite une bonne journée

Lu’!

Totalement HS : ce serait pas mal de mettre tes tags dans le formulaire correspondant aux tags du sujet plutôt que dans le titre du sujet.

Ok, ça fonctionne car tu changes les types que je propose dès le départ. Pourquoi pas, c’est en effet plus simple que ce que j’avais en tête.

Je regarderai ça à tête reposée, mais cette solution ne fonctionne pas avec le type instr que je propose, en tout cas dans le cas polymorphe.

Ok, c’est plus ou moins la solution à laquelle j’étais arrivée. Après je rejoins tes remarques sur ce que je propose. Mais j’avoue ne pas avoir pris trop de recul sur le code que j’ai écrit plus haut. Au début j’ai appelé ça succ mais ensuite j’ai renommé ça en stack car c’est plus intuitif.

Peut-être pensais-tu à une version à base de deux List.fold_left qui ferait du "n Cons"(Nil("n Int"(s))) ? C’est possible mais ça nécessite l’utilisation de Obj.magic car on aura effectivement des valeurs intermédiaires qui sont non-typables sans types dépendants (leur type dépend de la longueur de la liste). Cela peut se justifier pour des raisons de performance par exemple (la récursion d’Eusèbe n’est pas terminale), et dans la mesure où l’on sait que la valeur finale aura bien le type qu’on lui assigne (noter que le type de la valeur finale, lui, ne dépend pas de la longueur de la liste).

Je ne pense pas qu’il y ait besoin des types dépendants ici car il n’y a pas besoin de connaître la taille de la liste grâce au constructeur Cons.

C’est possible mais ça nécessite l’utilisation de Obj.magic

C’est bien la peine de s’embêter à exprimer des propriétés fortes dans le système de types si c’est pour annuler toutes les garanties avec Obj.magic

car on aura effectivement des valeurs intermédiaires qui sont non-typables sans types dépendants (leur type dépend de la longueur de la liste).

Je n’ai pas en tête la solution dont tu parles, donc je ne sais pas exactement de quelles opérations tu as besoin sur tes longueurs de liste, mais encoder le type « liste de longueur n » dans OCaml, ça se fait assez facilement. Il y a aussi un encodage qui permet de faire une concaténation (donc une addition sur les entiers-types).

Cela peut se justifier pour des raisons de performance par exemple (la récursion d’Eusèbe n’est pas terminale)

Ouais euh, les performances c’est bien, mais là tu fais un peu mal aux mouches D’autant plus que ce serait pas vraiment compliqué de transformer ça en une récursion terminale ici (quitte à ce que la liste soit retournée, de toute façon je ne suis même pas sûr que je l’empile dans le bon ordre).

Edit :

Pour le fun :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

type _ op =
  | Empty : unit op
  | Int : int * 'a op -> (int * 'a) op
  | Cons : ('t list * ('t * 'a)) op -> ('t list * 'a) op
  | Nil : 'a op -> ('b list * 'a) op

let s = Cons (Cons (Nil (Int (5,Int (2,Empty)))))

let start f = f Empty

let finish s = s

let int stack x k =
  k @@ Int (x, stack)

let cons stack k =
  k @@ Cons stack

let nil stack k =
  k @@ Nil stack

let s = start 
  int 3 
  int 2 
  nil
  cons
  finish

(* val s : (int list * (int * unit)) op = Cons (Nil (Int (2, Int (3, Empty)))) *)

Bon ici, il s’agit juste de construire une liste bien typée, donc c’est moins fun que l’exemple habituel qui embarque un langage à pile dans OCaml (avec des opérations qui peuvent dépiler des choses, par exemple add).

Les préoccupations de l’utilisateur d’une fonction sont 1) qu’elle soit sûre ; 2) qu’elle soit optimisée. C’est pourquoi il n’est pas gênant d’utiliser Obj.magic lorsque l’on fournit une fonction, si l’on sait par ailleurs que notre fonction reste sûre (il y a une discussion à ce sujet ici). Selon moi les GADT doivent apporter des garanties supplémentaires à l’utilisateur, sans gêner pour autant la personne qui implémente (Saroupille ici).

L’implémentation ci-dessous me semble être la plus optimisée (récursive terminale) :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17

type unsafe_instr =
  | UEmpty :                       unsafe_instr
  | UInt   : int * unsafe_instr -> unsafe_instr
  | UCons  : unsafe_instr       -> unsafe_instr
  | UNil   : unsafe_instr       -> unsafe_instr

let unsafe_mk_list l =
  let push_ints code =
    List.fold_left (fun top x -> UInt(x, top)) code l
  in
  let push_nil code =
    UNil code
  in
  let cons_all code =
    List.fold_left (fun top _ -> UCons top) code l
  in
  fun code -> cons_all (push_nil (push_ints code))

Cependant la variante utilisant vos GADTs sera mal typée à cause des valeurs intermédiaires produites, bien que l’on puisse prouver que cette fonction produit toujours comme valeur finale une séquence bien formée typable avec vos GADT. D’où la nécessité d’utiliser Obj.magic si l’on souhaite implémenter cette variante.

Je ne dis pas qu’il faut systématiquement privilégier la version avec Obj.magic, mais, étant donné le titre de ce sujet, j’ai cru que c’était à ce genre de fonctions que pensait Saroupille.