Salut Simon,
Donc pour clarifier les idées, voici ce à quoi je pensais:
Pour permettre de séparer l'allocation et l'initialisation, on pourrait
ajouter une sorte de ST monad qui pourrait ressembler un peu à du "alias
types" ou qqch du genre. Le type du monad aurait une forme comme
LLT : Store → Store → Type → Type
donc qqch du type `LLT s₁ s₂ τ` est une commande qui attend un Store de
la forme `s₁`, se termine avec un Store de la forme `s₂`, et renvoie une
valeur de type `τ`.
Les primitives pourraient ressembler à:
bind : LLT ?s₁ ?s₂ ?τ₁ → (?τ₁ → LLT ?s₂ ?s₃ ?τ₂) → LLT ?s₁ ?s₃ ?τ₂;
runLLT : LLT emptyStore ?s ?τ → ?τ;
exportPtr : LLTPtr ?ℓ → LLT (?s :: {?ℓ ↦ ?τ}) ?s ?τ;
Il faudra une forme une peu différente, parce que je ne vois pas encore
comment donner un type à "malloc", mais ça devrait pouvoir se faire.
Stefan