10

在 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 的网页获得。

4

1 回答 1

9

被指控有罪，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。

于 2013-01-12T08:06:08.500 回答