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功能应该如何实施？

在谈话的55分钟内解释了编译功能.

完整代码可从Conor的网页上获得.

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-ÉvaristeDagand在饰品上的合作自动化了这些模式,这些模式将程序引发的额外索引分层叠加在一个类型上,然后再将其擦掉.这是一个通用的定理,如果你擦除计算的索引然后从擦除的版本重新计算它,你得到(GASP!)正好是你擦除的索引.在这种情况下,这意味着run输入同意的代码eval将实际上给你相同的答案eval.