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