Agda:Conor 堆栈示例的运行函数

Question

在 ICFP 2012 上，Conor McBride 发表了主题演讲，主题为“Agda-curious？”。

它具有小型堆栈机器实现。

视频在 youtube 上:
http://www.youtube.com/watch?v=XGyJ519RY6Y

代码也在线:
http://personal.cis.strath.ac.uk/conor.mcbride/ICFP12Code.tgz

我想知道 run第 5 部分的功能(即“Part5Done.agda”，如果您下载了代码)。谈话在 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' _ _ = {!!}

run 的正确类型签名是什么？功能？ run应该怎么做功能实现？

编译功能解释 about 55 minutes into the talk .

完整代码是 available from Conor's webpage .

Answer 1

被指控的有罪，run 的类型函数来自 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)

这相当于说“给定从堆栈配置 ts 开始并在堆栈配置 ts' 和配置 ts 中完成的代码，您将在配置 ts' 中获得一个堆栈。“堆栈配置”是压入堆栈的事物的类型列表。

在 Part5Done.agda ，代码不仅由堆栈最初和最终保存的类型索引，而且由值索引。 run因此，函数被编织到代码的定义中。然后键入编译器以要求生成的代码必须具有 run对应于 eval 的行为.也就是说，编译代码的运行时行为必然要尊重引用语义。如果您想运行该代码，以亲眼看看您知道什么是正确的，请沿相同的行键入相同的函数，除了我们需要从索引的类型和值对中单独选择类型代码。

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)

或者，您可以应用明显的删除功能，将类型和值索引的代码映射到类型索引的代码，然后使用旧的 run功能。我与 Pierre-Évariste Dagand 在装饰品上的工作使这些模式自动化，即在一个类型上系统地分层由程序诱导的额外索引，然后将其擦掉。这是一个通用定理，如果您删除计算的索引然后从删除的版本重新计算它，您会得到(GASP!)您删除的索引。在这种情况下，这意味着 run输入与 eval一致的代码实际上会给你与 eval 相同的答案.