Idées pour plus tard

Ici on documente les idées qui ne seront pas implantées tout de suite, en général car la théorie n'est pas prête

Auto et langage de macro

L'existant

An niveau expression, pml a déjà un très faible langage de macro. On l'utilse par exemple pour définir la conjonction et la disjonction dans lib.bool, car on ne veut pas des fonctions qui évalue leur argument.

On peut aussi l'utiliser pour appliquer des lemmes automatiquement sans complexifié le type d'une fonciton: On écrit F<x,y> = use lemma x y; f x y

Pour aller plus loin

• avoir un point-fixe niveau expression
• avoir une analyse de cas qui correspond à l'unification dans equiv.pml

Avec ça, on doit pouvoir implanter la reification. C'est à dire que si on a une epxression arithmétique, on peut la transformer en un polynome que l'on évalue. Avec la refification on peut transformer un programme PML simplifiant un polynome en une tactique de simplification.

Ceci ne pose aucun problème de correction puisque l'on type-check des terms après évaluation des macros. Le seul risque sont les macros qui bouclent.

Pour aller encore plus loin

Il faudrait que les macros puissent stocker des donner dans l'arbre de preuve (le typage du terme donc). Par exemple, si on a une relation d'ordre cmp : a => a => bool. On peut stocker dans l'arbre des preuves toutes les connaissances que l'on accumule et lorsque l'on atteind une contradiction, on peut créer le terme de preuve automatiquement.

Compilateur optimisé

On peut ensuite essayer de récupérer les optimisation de PML1, mais PML2 possède des types vraiment abstrait et on perd la data flow analysis gratuite de PML1. On peut faire quelque-chose en ajoutant des graphes à chaque noeud de type représentant une approximation des types et des relations entre ces graphes (qui deviennent des bi-graphes) représentant le sous typage. On devrait alors récupérer les super optimisations de PML1 qui faisant de l'évaluation partielle piloté par le typage.

Effet algébrique = callcc + exception

On se propose d'avoir des effets algébriques comme en OCaml 5.0 mais sans limitation sur les continuations (ou peut les restorer plusieurs fois) et sans déclaration avant des effets.

try
  ... raise (C[x]) ...
with
  C[x,alpha] -> ... restore t alpha ...

L'idée est que try with marche comme des exceptions usuelles, mais le raise capture la continuation que l'on peut restaurer. Si on n'utilise pas la continuation, on a les exceptions habituelles.

Le type des fonctions et le signe |- du séquent sont alors annotés par C+ si on peut lever l'exception C et C- si on peut encore restaurer une continuation capturée sous un C. C tout court si on a les deux.

La règle importante du delim (les autres sont assez faciles) est alors

|-_C-,⋯ t : u
----------------------
|-_⋯    delim C t : u

si ni t ni u ne mentionne C dans les annotation des flèches (y compris dans les epsilons).

Je suis en train de regarder la sémantique, mais ce n'est pas si simple de justifier cette règle. La régle actuelle du delim utilise vraiment le modèle, en disant que si le type ne contient pas de flèche classique, il ne depend pas de bottom et on peut changer bottom! Là il faut mettre ensemble des bottom_C et pour l'instant j'ai du mal.

Pour exemple la preuve de [ Inl of A; Inl of (non A) ] (tier exclu) est alors

try
  Inl (raise C[x])
with
  C[x,alpha] → Inr (fun a { restore a alpha })

Ce qui donne un code assez clair.

Code impératif

Une première idée est un module style timed dans aucune restriction sur la gestion du temps. On peut voir alors les temps comme une map qui donne la valeur des références, avec une implémentation qui utilise des références.

Ce qu'il faut alors c'est une optimisation qui détecte qu'on ne garde par certains temps et que l'on a donc pas à sauvegarder les temps passé ni à construire la liste de blocs qui permet de restaurer les références.

Il y a aussi un pb de GC si une référence est modifiée deux fois et qu'aucun temps n'est accessible entre les deux modifications, il faudrait raccourcir la liste chaînée, sinon on a une fuite de mémoire.