什么是从无类型术语及其 CC 类型中恢复 CC 术语的干净算法？答案

【问题标题】：What is a clean algorithm to recover a CC term from an untyped one and its CC type?什么是从无类型术语及其 CC 类型中恢复 CC 术语的干净算法？
【发布时间】：2018-07-16 00:16:54
【问题描述】：

假设我有一个未键入的术语，例如：

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)))

我尝试了一些东西，但很快注意到如何传递类型并不明显。具体来说，Lam 案例似乎需要一个 forall 类型并将其附加到上下文中，App 案例的功能似乎产生一个由参数使用的 forall 类型， Var 案例似乎查询上下文类型。这种不对称性让我的代码有点乱，所以我想知道是否有明显的方法来实现它。

【问题讨论】：

“抄送”是什么意思？微积分？

标签： haskell lambda-calculus type-theory

【解决方案1】：

您不能在输入中包含 beta redex，因为您主要不能推断 lambda 的类型，否则它只是标准的双向类型检查。如果知道输入的类型是正确的，那么您可以跳过转换检查。伪代码：

check : Term → Type → Cxt → CCTerm
check (λ x. t) ((x : A) → B) Γ = λ (x : A). check t B (Γ, x : A)
check t        A             Γ = fst (infer t Γ) -- no conv check

infer : Term → Cxt → (CCTerm, Type)
infer (λ x.t) Γ = undefined
infer x       Γ = (x, lookup x Γ)
infer (t u)   Γ = (t' u', B[x ↦ u'])
  where (t', ((x : A) → B)) = infer t Γ
        u' = check u A Γ

（将其转换为 de Bruijn 索引并可能更快地All 替换）。我觉得Star 和All 不在Term 中有点奇怪，但它们也可以在infer 中包含。

【讨论】：

【解决方案2】：

您似乎在询问比 System F 更具表现力的系统中的类型推断，即 known to be undecidable。

【讨论】：