Guilty as charged, the type of the run
function from Part4Done.agda
is
run : forall {ts ts'} -> List Inst ts ts' -> List Elt ts [] -> List Elt ts' []
run [] vs = vs
run (PUSH v , is) vs = run is (E v , vs)
run (ADD , is) (E v2 , E v1 , vs) = run is (E 0 , vs)
run (IFPOP is1 is2 , is) (E tt , vs) = run is (run is2 vs)
run (IFPOP is1 is2 , is) (E ff , vs) = run is (run is1 vs)
which amounts to saying "Given code which starts from stack configuration ts
and finishes in stack configuration ts'
and a stack in configuration ts
, you will get a stack in configuration ts'
. A "stack configuration" is a list of the types of the things pushed on the stack.
In Part5Done.agda
, the code is indexed not only by the types of what the stack holds initially and finally but also by the values. The run
function is thus woven into the definition of the code. The compiler is then typed to require that the code produced must have a run
behaviour which corresponds to eval
. That is, the run-time behaviour of compiled code is bound to respect the reference semantics. If you want to run that code, to see with your own eyes what you know to be true, type the same function along the same lines, except that we need to select the types alone from the types-and-values pairs which index the code.
run : forall {ts ts' vs vs'} -> List Inst (ts & vs) (ts' & vs') ->
List Elt ts [] -> List Elt ts' []
run [] vs = vs
run (PUSH v , is) vs = run is (E v , vs)
run (ADD , is) (E v2 , E v1 , vs) = run is (E (v1 + v2) , vs)
run (IFPOP is1 is2 , is) (E tt , vs) = run is (run is1 vs)
run (IFPOP is1 is2 , is) (E ff , vs) = run is (run is2 vs)
Alternatively, you can apply the obvious erasure function which maps the types-and-values-indexed code to types-indexed code, then use the old run
function. My work with Pierre-Évariste Dagand on ornaments automates these patterns of layering an extra index induced by a program systematically over a type then rubbing it out later. It's a generic theorem that if you erase the computed index then recompute it from the erased version, you get (GASP!) exactly the index you erased. In this case, that means run
ning the code which is typed to agree with eval
will actually give you the same answer as eval
.