什么是一个干净的算法,从一个非类型的和它的CC类型恢复一个CC术语?

假设我有一个未输入的术语,例如:

data Term = Lam Term | App Term Term | Var Int

-- λ succ . λ zero . succ zero
c1 = (Lam (Lam (App (Var 1) (Var 0)))

-- λ succ . λ zero . succ (succ zero)
c2 = (Lam (Lam (App (Var 1) (App (Var 1) (Var 0))))

-- λ succ . λ zero . succ (succ (succ zero))
c3 = (Lam (Lam (App (Var 1) (App (Var 1) (App (Var 1) (Var 0)))))

-- λ cons . λ nil . cons 1 (cons 2 (cons 3 nil))
term_untyped = (Lam (Lam (App (App (Var 1) c1) (App (App (Var 1) c2 (App (App (Var 1) c3) Nil) 

其CC类型:

data Type = Set | All Type Type | Var Int

-- ∀ (P : *) -> ∀ (Succ : P -> P) -> ∀ (Zero : P) -> P
nat = All(Set, All(All(Var(0), Var(1)), All(Var(0), Var(1))))

-- ∀ (P : *) -> ∀ (Cons : x -> P -> P) -> ∀ (Nil : P) -> P
list x = All(Set, All(All(x, All(Var(0), Var(1))), All(Var(0), Var(0))))

-- term_type
term_type = list nat

是否有一个干净的算法可以恢复对应于非类型项的cc项?即。,

data CCTerm 
   = Lam CCTerm CCTerm 
   | All CCTerm CCTerm 
   | App CCTerm CCTerm 
   | Set 
   | Var Int

term_typed :: Term -> CCTerm
term_typed = from_untyped term_type term_untyped

-- As the result, typed_term would be:
-- λ (P : *) ->
-- λ (Cons : ∀ (x : (∀ (Q : *) -> (Q -> Q) -> Q -> Q)) -> P -> P) ->
-- λ (Nil : P) ->
-- ( Cons (λ (Q : *) -> λ (Succ : Q -> Q) -> (Zero : Q) -> Succ Zero)
-- ( Cons (λ (Q : *) -> λ (Succ : Q -> Q) -> (Zero : Q) -> Succ (Succ Zero))
-- ( Cons (λ (Q : *) -> λ (Succ : Q -> Q) -> (Zero : Q) -> Succ (Succ (Succ Zero)))
--   Nil)))

我试过一些东西,但很快就注意到如何传递类型并不明显。特别是,林的案子似乎 要求 一个forall类型并将其附加到上下文中,app case的函数似乎 生产 参数使用的forall类型,而var case似乎 查询 上下文上的类型。这种不对称性使我的代码有点混乱,所以我想知道是否有一种明显的方法来实现这一点。