Bonjour,
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
nil : (ℓ : TypeLevel) ≡> (α : Type ℓ) -> Datacons List (List α); nil = datacons List nil;
cons : (ℓ : TypeLevel) ≡> (α : Type ℓ) -> Datacons List (α -> List α -> List α); cons = datacons List cons;
Et la primitive présentée plus haut aurait le type
Heap_unsafe-store-header : (addr : Int) -> Datacons ?τ ?τ-arr -> ##Heap Unit;
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.
La seconde est de changer datacons pour retourner un Datacons. Ça implique par contre qu'il faut ajouter à l'élaboration une coercition automatique du Datacons vers une fonction.
Qu'est-ce que vous en pensez?
Simon