Agda: run function for Conor's stack example

Question

At ICFP 2012, Conor McBride gave a keynote with the tile "Agda-curious?".

It featured a small stack machine implementation.

The video is on youtube: http://www.youtube.com/watch?v=XGyJ519RY6Y

The code is online too: http://personal.cis.strath.ac.uk/conor.mcbride/ICFP12Code.tgz

I am wondering about the run function of Part 5 (i.e. "Part5Done.agda" if you downloaded the code). The talk stops before the run function is explained.

data Inst : Rel Sg SC Stk where
  PUSH  : {t : Ty} (v : El t) -> forall {ts vs} ->
            Inst (ts & vs) ((t , ts) & (E v , vs))
  ADD   : {x y : Nat}{ts : SC}{vs : Stk ts} ->
            Inst ((nat , nat , ts) & (E y , E x , vs))
              ((nat , ts) & (E (x + y) , vs))
  IFPOP : forall {ts vs ts' vst vsf b} ->
          List Inst (ts & vs) (ts' & vst)  -> List Inst (ts & vs) (ts' & vsf)
          -> Inst ((bool  , ts) & (E b , vs)) (ts' & if b then vst else vsf)

postulate
  Level : Set
  zl : Level
  sl : Level -> Level

{-# BUILTIN LEVEL Level #-}
{-# BUILTIN LEVELZERO zl #-}
{-# BUILTIN LEVELSUC sl #-}

data _==_ {l : Level}{X : Set l}(x : X) : X -> Set l where
  refl : x == x

{-# BUILTIN EQUALITY _==_ #-}
{-# BUILTIN REFL refl #-}


fact : forall {T S} -> (b : Bool)(t f : El T)(s : Stk S) ->
         (E (if b then t else f) , s) ==
         (if b then (E t , s) else (E f , s))
fact tt t f s = refl
fact ff t f s = refl

compile : {t : Ty} -> (e : Expr t) -> forall {ts vs} ->
   List Inst (ts & vs) ((t , ts) & (E (eval e) , vs))
compile (val y)     = PUSH y , []
compile (e1 +' e2)  = compile e1 ++ compile e2 ++ ADD , []
compile (if' e0 then e1 else e2) {vs = vs}
  rewrite fact (eval e0) (eval e1) (eval e2) vs
  = compile e0 ++ IFPOP (compile e1) (compile e2) , []

{- 
-- ** old run function from Part4Done.agda
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)
-}

run : forall {i j} -> List Inst i j -> Sg Stack (λ s -> s == i) → (Sg SC Stk)
run {vs & vstack} [] _
   = (vs & vstack)
run _ _ = {!!} -- I have no clue about the other cases...

--Perhaps the correct type is:
run' : forall {i j} -> List Inst i j -> Sg Stack (λ s -> s == i) → Sg (Sg SC Stk) (λ s → s == j)
run' _ _ = {!!}

What is the correct type signature of the run function? How should the run function be implemented?

The compile function is explained about 55 minutes into the talk .

The full code is available from Conor's webpage.

Answer 1

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 running the code which is typed to agree with eval will actually give you the same answer as eval.