notes.txt

Notre système :

Règles de déduction de la forme :

Γ |- e: m

avec e une expression, m un mode, Γ un environnement.
Γ est la fonction qui associe à chacune des variables libres de e le mode
dans lequel elle doit être utilisée pour que e soit utilisée dans le mode m.

m est l'entrée, Γ est la sortie.

L'idée serait que pour chaque expression de la forme
let rec x1 = e1 and ... and xn = en (in e)? qui apparait dans l'arbre, on
calcule les environnements :
Γi |- ei: Unguarded
et qu'on vérifie que les variables x1, ..., xn sont utilisée en mode
Guarded, Delayed ou Unused dans les environnements Γ1, ..., Γn.

Je pense que ceci pourrait être étendu, en ne vérifiant qu'une seule fois
l'expression.
L'idée serait qu'à chaque let rec, on type l'expression ainsi :

Γ1 |- e1: Unguarded
...
Γn |- en: Unguarded
(règle pour e)?
-------------------
... |- let rec ...: m

En même temps qu'on calcule les environnements Γ1, ..., Γn, on vérifie la bonne
utilisation des variables x1, ..., xn.

Ça permetrait de n'effectuer le calcul qu'une seule fois pour toute une
expression, et d'éviter de faire plusieurs fois les mêmes calculs pour les
mêmes let rec imbriqués.

Pour l'instant, le type-checker d'OCaml ne fonctionnant pas ainsi, on ne s'en
préoccupera pas.

Joindre des environnements :

On peut classer les modes du plus fort au plus faible :
Deref > Unguarded > Guarded > Delayed > Unused

On définit alors pour deux environnements Γ1 et Γ2 :
(Γ1 + Γ2): x -> max(Γ1(x), Γ2(x))

Composition d'environnements :
Si une expression e est utilisée dans l'expression e' avec le mode m', laquelle
est utilisée avec le mode m, dans quel mode est utilisée e ?
On dit que e est utilisée dans le mode m[m'].

Définition actuelle :
Si m € {Deref, Unguarded, Guarded, Delayed}
et m' & {Deref, Guarded, Delayed} :
Delayed[m'] = Delayed
Deref[m'] = Deref
Guarded[m'] = m'
Unguarded[m'] = m'

On remarque donc que m[m'] prend ses valeurs parmi {Deref, Guarded, Delayed}.

Cela nous donne les premières règles de déduction :

---------
ø |- c: m

------------
x: m |- x: m

Γ1 |- e1: m[Deref]
Γ2 |- e2: m[Deref]
-------------------
Γ1 + Γ2 |- e1 e2: m

Γ, x: m' |- e: m[Delayed]
-------------------------
Γ |- (fun x -> e): m

Γ1 |- e1: m[Guarded]
...
Γ2 |- en: m[Guarded]
-----------------------------------
Γ1 + ... + Γn |- K(e1, ..., en): m

Le cas des règles let et let rec :

d'après Gabriel, la règle pour let devrait être la suivante :

Γ1 |- e1: let mx in m
Γ2, x: mx |- e2: m
---------------------------
Γ1 + Γ2 |- let x = e1 in e2

la question est la suivante : quel est le mode let mx in m ?

1- Si m = Delayed :

On veut avoir la règle suivante : si Γ |- e: Delayed, alors pour toute variable
libre x de e, Γ(x) = Delayed.

Pour que cette règle soit respectée dans le cas de let, il nous faut donc :
let mx in m = Delayed.

2- Si m = Deref :

Similairement, on veut que si Γ |- e: Deref, alors pour toute variable libre de
e, Γ(x) = Deref.

Il nous faut donc, let mx in Delayed = Deref.

3- Si mx = Deref :
Si on réfléchit, lorsqu'on a besoin de connaitre la valeur de notre
let ... in ..., on va d'abord « évaluer » e1, mettre le résultat en e2, puis
« évaluer » e2.

Je met « évaluer » entre guillemets puisqu'on n'a pas forcément besoin de
déréférencer les variables de e1.

Par exemple, l'expression suivante est acceptée :
let rec z = (let x = z in 1 :: x);;

Si l'expression z dans let x = z in ... nécessitait que les variables soient
déréférencées, cette expression ne serait pas compilée.

En revanche, cette remarque ne s'applique pas si mx = Deref.
On peut donc ajouter : let mx in m = Deref.

4- Si m = Guarded :
On va regarder au cas par cas.

4.1
Si mx = Deref, let mx in m = Deref par la remarque précédente
4.2
Si mx = Guarded, alors m = Guarded.

Exemple : let z = 2 :: (let x = z in 2 :: x).
Il me parait clair que z est utilisé en mode Guarded.

4.3
Si mx = Delayed, il me semble que let mx in m = Guarded.
    
Exemple :
type foo = K of (unit -> foo);;
let rec z = K(let x = z in fun() -> x)

On a bien m = Guarded et mx = Delayed.

L'expression e[z] est évaluée, puis placée en en x, puis fun() -> x est
évaluée.

Si on type l'expression, on a :
z: let mx in m |- z: let mx in m
x: Delayed |- fun() -> x
--------------------------------------------------
z: let mx in m |- let x = z in fun() -> x: Guarded
-------------------------------------------------------
z: let mx in m |- K(let x = z in fun() -> x): Unguarded

Il me semble que l'on évalue d'abord x = z, que x est en gros un pointeur
pointant vers les données de z, que même si x l'experssion x est en mode
Delayed dans fun() -> x, x a déjà été évaluée. Comme tout est placé dans un
constructeur, z est Guarded.

Poser let mx in m = Guarded est cohérent avec le système actuel de typage.
Poser let mx in m = Unguarded ne l'est pas, puisque cette expression serait
rejetée.
Poser let mx in m = Delayed ne l'est pas, puisqu'un experssion de la forme
let z = K(let x = f z in fun() -> x) serait acceptée, alors qu'on
aurait besoin de déréférencer z pour évaluer cette expression.

Poser let mx in m = Guarded me parait le choix le plus raisonable.

4.4
Si mx = Unused, alors let mx in m = Guarded.

Raisons :
il nous faut refuser l'expression :
let rec z = Some(let x = do_something_with z in 1).
On ne peut donc pas avoir let mx in m <= Delayed

Par croissance (à définir), on doit donc avoir let mx in m = Guarded.

4.5
Je pense qu'on n'a pas besoin de définir le cas mx = Unguarded.

Il nous faudrait définir notre système de telle sorte que si
Γ |- e: Guarded, alors pour toute variable libre x de e, Γ(x) ≠ Unguarded.

5- Si m = Unguarded
Encore une disjonction de cas :

5.1 - Si mx = Deref
Par la remarque 3, let mx in m = Unguarded

5.2 - Si mx = Unguarded
On a let mx in m = Unguarded.

Exemple :
let rec z = (let x = e[z] in x)

Si on effectue le test, on a les dérivations :

z: m' |- e[z]: let mx in m
x: Unguarded |- x: Unguarded
-------------------------------------
z: m' |- let x = e[z] in x: Unguarded

Si on prend e[z] = z, alors on a z: let mx in m |- let mx in m, donc
z: let mx in m |- let x = z in x: Unguarded.
Cette définition récursive devant être refusée par le compilateur, il nous
faut donc que let mx in m soit égal à Deref ou Unguarded.

Or, il ne faut pas que let mex in m soit égal à Deref, cela reviendrait à
refuser l'expression lorsque e[z] = 1 :: z.

Update : cette expression est actuellement refusée par le compilateur, il me
faut enquêter dessus.

Update : comme il me semblait, cette expression est refusée puisque le
compilateur considère que la taille de l'expression n'est pas connue à la
compilation.

Plus généralement, les seules expressions de cette forme autoriée sont les
expressions avec e[z] = a, et a l'identificateur d'une variable dont la taille
est considérée comme connue.

Je pense donc qu'il faut avoir let mx in m = Unguarded pour des raisons de
cohérence, c'est-à-dire que le résultat de test récursif pour de Jeremy doit
être le même que pour notre check recursif, à définiton de
Guarded/Delayed/Unused près.

5.3- mx = Guarded
Je crois que rien ne nous empêche de poser let mx in m = Guarded.

Exemple :
let rec z = (let x = e1[z] in 1 :: x)

5.4- mx = Delayed

Exemple (avec l'option -rectypes) :
let rec z = (let x = z in fun() -> x)

Comme l'exemple précédent, je poserais let mx in m = Guarded, et ça devrait
être bon. Cependant, j'ai quelques scrupules. En effet, comme on observe dans
l'exemple précédent, e1 = z est évalué dans le mode Guarded alors qu'aucun
constructeur n'intervient.

Cela veut dire qu'il faut peut-être changer notre définition de Guarded.

En effet, intuitivement, si l'on évalue e1 en mode Guarded, ce n'est pas parce
que e1 va être placé dans un constructeur, c'est parce qu'on ne fait pas
référérence aux variables de portée supérieures directement comme ce serait
le cas avec let x = z in x, on n'accède pas directement à ces variables.

D'un autre côté, e1 est évalué avant e2 qui l'est en Unguarded, e1 ne peut
donc pas être évalué en mode Delayed.

De plus, c'est le seul choix cohérent possible si l'on tient à ce que
let ... in ... soit une fonction croissante.

5.5- mx = Unused

Pour un peu les mêmes raisons, je définirais let mx in m = Guarded, avec les
mêmes réserves.

Tableau récapitulatif :

let mx in m -> | Deref     | Unguarded | Guarded   | Delayed   |
    |          |           |           |           |           |
    v          |           |           |           |           |
--------------- ----------- ----------- ----------- -----------
Deref          | Deref     | Deref     | Deref     |     /     |
--------------- ----------- ----------- ----------- -----------
Unguarded      |     /     | Unguarded |     /     |     /     |
--------------- ----------- ----------- ----------- -----------
Guarded        |     /     | Guarded   | Guarded   |     /     |
--------------- ----------- ----------- ----------- -----------
Delayed        |     /     | Guarded   | Guarded   | Delayed   |
--------------- ----------- ----------- ----------- -----------
Unused         | Deref     | Guarded   | Guarded   | Delayed   |
--------------- ----------- ----------- ----------- -----------

Cela nous donne (enfin !) une fonction let ... in ..., elle est presque
continue, c'est-à-dire continue sur tout son intervalle de définition. On
peut s'amuser à étendre cette fonction, mais on aurait des cas qui n'auraient
pas beaucoup de sens.

Remarque esthétique : on perd un peu en simplicité.

Règle let rec ?

Γ1, x: _ |- e1: let mx in m
Γ2, x: mx |- e2: m
---
|- let rec x = e1 in e2: ms

est-ce que ça convient ? Je ne vois pas d'objection. Un let a le même effet
qu'un let rec sur les variables de portée supérieure. La seule différence est
que x doit être bien formée, mais ce test est effectué récursivement, on ne
s'en préoccupe pas.

L'extension pour let rec ... and ... est directe :

Γ1, x1: _, ..., xn: _ |- e1: let mx1 in m
...
Γn, x1: _, ..., xn: _ |- en: let mxn in m
Γ, x1: mx1, ..., xn: mxn |- e: m
----------------------------------------------------------------
Γ1 + ... + Γn + Γ |- let rec x1 = e1 and ... and xn = en in e: m

Remarque : si on a let p = e, avec p un pattern detructif (pas dans un let rec,
ceci est actuellement refusé par le compilateur), ne suffit-il pas de calculer
Γ1 dans le contexte Deref ?

Cas de match ... with, en supposant que tous les patterns sont destructifs :

Γ1, {x: _, x € fv(p1)} |- e1: m?
...
Γn, {x: _, x € fv(pn)} |- en: m?
Γ |- e: m[Deref]
---
|- match e with p1 -> e1 | ... | pn -> en: m

27/06/2018 :

On peut donner une expression plus simple de let ... in ... que le tableau.
Il nous suffit de dire que :
let mx in m = m[mx + Guarded]

De plus, si on a un pattern destructif, on remplace le tout par :
m[mx + Deref] = m[Deref].

Ça veut dire qu'il nous faudrait plutôt définir un opérateur :
let mx in m with mode m,
avec m = Guarded si le pattern est destructif, m = Deref sinon.

28/06/2018 :

Je viens de me rendre compte que j'ai complètement oublié de parler de la règle
match !

Actuellement, il y a une subtilité. On pourrait s'attendre à ce que les
expressions let p = e1 in e2 et match e1 with p -> e2 se comportent pareil, ce
qui n'est pas le cas dans le système de Jeremy.

En effet, on a les règles :

Γ |- e1: A
Γ + {x: A, x € vars(p)} |- e2: B
--------------------------------
Γ |- let p = e1 in e2: A' + B

et 

Γ |- e1: A
Γ + {x: A', x € vars(p)} |- e2: B
----------------------------------
Γ |- match e1 with p -> e2: A' + B

avec dans les deux cas A' = discard(A) * mode(p), mode(p) valans Deref si
p est destructif, Guarded sinon.

J'ai essayé de voir dans quel cas ces deux règles diffèrent.
Je me suis convaincu que si mode(p) = Deref, toutes les variables apparaissant
dans A sont en Deref, ce qui peut avoir une inflence sur B dans l'expression
match ... with.
Or, dans tous les cas, le type final est A' + B, avec toutes les variables
de A en Deref, donc ça semble rien changer.

Si mode(p) = Guarded, le seul changement est si l'une des variables est
utilisée en mode Unguarded dans e1.
Il faut que ce soit une variable définie par le let rec que l'on est en train
de vérifier. De plus, si elle intervient dans une experssion déréférencée,
délayée ou placée dans un constructeur, son mode passe en Guarded, ce qui est
la même chose que A.

Ce que je dit est confus, voici un exemple :
let rec z = (let rec x = z in x)  (1)
let rec z = (match z with x -> x) (2)

Pour la ligne (1), le type de l'expression entre parenthèses sertai :
(z: (z -> Unguarded))
Pour la ligne (2), le type de l'experssion entre parenthèses serait :
(z: (z -> Guarded))

La ligne (1) est refusée puisque z est Unguarded, la ligne (2) est refusée
puisque la taille de z n'est pas connue à la compilation (il faudrait utiliser
le hack du compilateur pour vérifier).

Il semblerait juste que la règle match ... with ... soit un peu plus
permissive, mais que ça ne change rien au final.

Je vais donc décider d'ignorer cette subtilité.

Un règle pour match serait :

Γ1, {x: m1(x), x € vars(x)} |- e1: m
...
Γn, {x: mn(x), x € vars(x)} |- en: m
Γ |- e: m'1 + ... + m'n
----------------------------------------------------------
Γ1 + ... + Γn + Γ |- match e with p1 -> e1 ... pn -> en: m

avec pour tout i entre 1 et n :
m'i = let Unused in m si p est le pattern « _ »
m'i = let mi(x) in m  si p est le pattern « x », x un identifieur
m'i = m[Deref]        si p est un pattern destructif

Remarque : je ne gère pas encore les patterns de la forme p | p', ni de la
forme p as x.

15/06/2018:
J'ai pour la première fois lancé la suite de tests.

Dans le dossier testsuite/tests/letrec, 15 tests sur 19 échouent.
Les 4 tests exécutés avec succès sont :
class_1.ml, lists.ml, mixining_value_closures_1.ml et pr4989.ml.

Tous les tests qui échouent le font avec la sortie -2, mais je ne sais pas s'il
s'agit de mon « failwith "TODO" ».

Le test « class_1.ml » passe alors que je n'ai pas implémenté les classes, c'est
étrange. Peut-être qu'il s'agit d'un test vérifiant qu'une exception est levée,
il me faut vérifier.

16/06/2018:
Je vais légèrement changer ma définition de la composition, en définissant :
m[Unguarded] = m
Guarded[m'] = m' si m' <> Unguarded

Cela ne change la définition que pour le cas Guarded[Unguarded], qui vaut
maintenant Guarded et non Unguarded.

Intuitivement, cela se justifie 

L'une des raisons de ce chagement et que dans les règles de typage, je fait
plusieurs fois des disjonctions de cas, avec un mode m' qui vaut m dans certain
cas et m[Delayed]/m[Deref]/m[Guarded] dans d'autres cas.

Écrire une règle de typage est un peu pénible. C'est plus simple de dire que ce
mode m' vaut m[m''], avec m'' valant Unguarded dans certains cas, ce qui permet
d'avoir m = m'.

Si ce que je viens de dire est peu clair, voir les règles de typage pour `lazy`
ou `record` dans typing/rec_check.ml.

Il y a une deuxième raison, pour laquelle j'avais pensé à ce changement plus
tôt, mais je ne m'en rappelle plus. Il se pourrait qu'elle soit très proche de
la raison précédemment évoquée.

17/07/2018:
Quelque chose que j'essaie de comprendre est le comportement des records et des
tableaux avec des flottants, et en quoi cela diffère de l'utilisation avec des
valeurs non flottantes.

Prenons par exemple les tableaux. 3 sous-cas sont distingués :
- le tableau est un tableau dépendant d'un type générique
- le tableau est un tableau de flottants
- le tableau est un tableau de type concret non flottants

Dans les premiers cas, la règle (dans notre système) est la suivante :

G0 |- x0: m[Deref]
...
Gn |- xn: m[Deref]
-------------------------------
G0 + ... Gn |- [|x0; ...; xn|]: m

Alors que dans le dernier cas, la règle est la suivante :

G0 |- x0: m[Guarded]
...
Gn |- xn: m[Guarded]
-------------------------------
G0 + ... Gn |- [|x0; ...; xn|]: m

Cette dernière règle est facilement explicable, elle est très similaire aux 
règles concernant les tuples et les constructeurs (incluant notamment les
listes).

La question est : pourquoi une différence de comportement pour les flottants et
les types génériques ?

Pour les flottants, cela doit venir d'une optimisation du compilateur. En règle
générale, un tableau est représenté en mémoire par le tableau des valeurs.

Il y a une exception pour les flottants. En effet, représenter comme ceci un
tableau de flottants reviendrait à utiliser un tableau d'adresses. Au lieu, un
tableau de flottants est un tableau de flottants unboxés, ce qui permet plus
d'efficacité. Or, ceci change la 

J'essaie de voir quelles sont les différences. Le code suivant n'est pas
accepté :

let f x = let rec y = x and a = [|y|] in a

Alors que celui-ci l'est :

let f (x: int) = let rec y = x and a = [|y|] in a

Et étrangement, celui-ci passe (je n'aurais pas pensé à cause du cas spécial
pour les tableaux de flottants) :

let f (x: float) = let rec y = x and a = [|y|] in a

EDIT : j'ai fait mes tests sur OCaml 4.05, version pour laquelle des expressions
dangereuses avec des flottants été autorisées. Il faut que je refasse des tests.

19/07/2018:
Actuellement, je bloque sur le typage des modules.
Il me faut pouvoir typer les expressions de modules : struct ... end.

On peut considérer, en faisant une grosse approximation, que l'expression :
struct
let x1 = e1
...
let xn = en
end

doit se typer de la même façon que :
let x1 = e1 in
...
let xn = en in
K(x1, ..., xn)

Ce qui donne :

...
--------------------------------------
G |- K(x1, ..., xn): m
avec G = x1: Guarded, ..., xn: Guarded

Gn |- en: m[Guarded] G |- ...
---
Gn + G-xn |- let xn = en in K(x1, ..., xn): m

G{n-1} |- e{n-1}: m[m' + Guarded]   (Gn + G) - {x{n-1}, xn}, x{n-1}: m' |- ...
------------------------------------------------------------------------------
G{n-1} + (Gn + G) - {x{n-1}, xn} |- let x{n-1} = e{n-1} in ...: m

...

G1 |- e1: m[m' + Guarded] (G2 + ... + Gn + G)-{x2, ..., xn} |- ...
------------------------------------------------------------------
(G1 + ... + Gn + G) - {x1, ..., xn} |- let x1 = e1 in ...: m

Remarque : il me semble qu'on n'a pas besoin de faire let ... in K(x1, ..., xn).
Une expression dans laquelle x1, ..., xn sont utilisés en mode Delayed ou
Unused semble donner la même chose.

Cela nous donne donc la règle :

G1 |- x1: (G2 + ... + Gn) = e1 in m
G2 |- x2: (G3 + ... + Gn) = e2 in m
...
Gn |- x1: ø = e1 in m
------------------------------------------------------------------------
(G1 + ... + Gn) - {x1, ..., xn} |- struct let x1 = e1 ... xn = en end: m

Cela donne déjà une base, on pourra généraliser ensuite.