Agda: funkcja run dla przykładu stosu Conora

Question

Podczas ICFP 2012, Conor McBride wygłosił przemówienie z pytaniem "Agda-curious?".

Zawierała implementację małego stosu maszyn.

Film jest na youtube: http://www.youtube.com/watch?v=XGyJ519RY6Y

Kod jest zbyt online: http://personal.cis.strath.ac.uk/conor.mcbride/ICFP12Code.tgz

Zastanawiam o funkcji run części 5 (czyli "Part5Done.agda" jeśli pobrać kod). Dyskusja zatrzymuje się przed wyjaśnieniem funkcji run.

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' _ _ = {!!} 

Jaki jest poprawny typ podpisu funkcji run? W jaki sposób należy zaimplementować funkcję run?

Funkcja kompilacji została wyjaśniona about 55 minutes into the talk. Pełny kod to available from Conor's webpage.

Answer 1

Winny jak oskarżony, rodzaj funkcji run z Part4Done.agda jest

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) 

co sprowadza się do stwierdzenia „Biorąc pod uwagę kod, który rozpoczyna się od konfiguracji stosu ts a kończy w konfiguracji stosu ts' i stos w konfiguracji ts, otrzymasz stos w konfiguracji ts'. "Konfiguracja stosu" jest listą typów rzeczy pchanych na stosie:

W Part5Done.agda kod znajduje się w zszokowany nie tylko rodzajami początków i wartości stosu, ale także wartościami. Funkcja run jest wpleciona w definicję kodu. Kompilator jest następnie wpisywany, aby wymagać, aby wygenerowany kod miał zachowanie run, które odpowiada eval. Oznacza to, że zachowanie skompilowanego kodu w czasie działania musi respektować semantykę odniesienia. Jeśli chcesz uruchomić ten kod, aby na własne oczy zobaczyć, co wiesz, że jest prawdziwe, wpisz tę samą funkcję wzdłuż tych samych linii, z tą różnicą, że musimy wybrać typy z par typów i wartości, które indeksują kod.

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) 

Alternatywnie można zastosować oczywistą funkcję wymazywania który mapuje typów-i-wartości indeksowanych kod typów indeksowane kodem, a następnie użyć starego run funkcję. Moja praca z Pierre-Évariste Dagand na ornamentach automatyzuje te wzorce nakładania dodatkowego indeksu wywołanego przez program systematycznie nad typem, a następnie pociera go później. Jest to generyczne twierdzenie, że jeśli skasujesz obliczony indeks, a następnie przeliczysz go z usuniętej wersji, otrzymasz (GASP!) Dokładnie skasowany indeks. W tym przypadku oznacza to, że run ns kod, który został wpisany w celu uzgodnienia z eval, faktycznie da taką samą odpowiedź, jak eval.