J'essaie d'ajouter une extension à Typer pour séparer l'allocation de l’initialisation. Une primitive importante pour ça est

Heap_unsafe-store-header : (addr : Int) -> ??? -> ##Heap Unit;

où addr est l'adresse où le bloc a été alloué et ##Heap une sorte de ST pour le tas. Le problème est le deuxième argument, qui doit désigner un constructeur de valeur. En ce moment, on a par exemple

cons : ?α -> List ?α -> List ?α;

qui est impossible de distinguer d'une fonction par son type.

J'aimerais donc introduire un nouveau type primitif,

Datacons : (ℓ : TypeLevel) ≡> (t : Type_ ℓ) -> (arr : Type_ ℓ) -> Type_ ℓ;

On aurait donc

[...]

cons : (ℓ : TypeLevel) ≡> (α : Type ℓ) -> Datacons List (α -> List α -> List α);
cons = datacons List cons;

Je dois admettre que j'aime pas trop l'idée d'avoir un nouveau type pour des sortes particulières de fonctions.

Ça pourrait être utile, par exemple pour trouver les constructeurs dans les branches de `case`, donc c'est peut-être pas une mauvaise idée, mais ça risque d'avoir des conséquences un peu trop vastes pour ton projet.

Par contre, je vois deux façon d'ajouter ça à Typer. La première est de ne pas toucher à datacons et d'introduire une nouvelle forme spéciale pour avoir le Datacons lui-même plutôt que la fonction.

Je crois que c'est préférable. Et Heap_unsafe-store-header pourrait même utiliser un type qui n'est "pas typé". Je propose donc d'utiliser un nouveau type simple `HeapObjectLabel` (n'hésite pas à raccourcir à ta convenance, par exemple `Tag`) et les objets de ce type pourraient être construits en leur passant simplement peut-être une chaîne de caractère ou un petit entier.

Ça aura aussi l'avantage de ne pas affecter le reste du code de Typer.

Stefan