使用“绑定”对依赖 lambda 抽象进行类型检查的正确方法是什么？答案

【问题标题】：What is the right way to typecheck dependent lambda abstraction using 'bound'?使用“绑定”对依赖 lambda 抽象进行类型检查的正确方法是什么？
【发布时间】：2015-08-06 16:45:57
【问题描述】：

我正在实现一种简单的依赖类型语言，类似于 described by Lennart Augustsson，同时还使用 bound 来管理绑定。

在检查依赖的 lambda 项时，例如 λt:* . λx:t . x，我需要：

“进入”外部 lambda 绑定器，通过将 t 实例化为某物
类型检查λx:t . x，产生∀x:t . t
Pi-抽象t，产生∀t:* . ∀x:t . t

如果 lambda 是非依赖的，我可以在第 1 步用它的 type 实例化 t，因为类型是我在第 2 步进行类型检查时需要知道的关于变量的全部信息. 但是在第 3 步中，我缺乏决定抽象哪些变量的信息。

我可以引入一个新的名称供应并用包含类型和唯一名称的Bound.Name.Name 实例化t。但我认为使用bound 我不需要生成新名称。

是否有我缺少的替代解决方案？

【问题讨论】：

无论你做什么，你都需要保持 t 的独特性。如果你在做 Pi 抽象，这是必要的（如果你不能清楚地看到它，你将如何抽象 t？）但它也需要对 body 进行类型检查（t 是一种类型，与许多其他类型不同）。你可以保留 t de Bruijn，但是你需要更加小心如何在它的活页夹下工作。我会选择一个新名称，并且确实会用它来缓存类型。我有兴趣看到替代方法。

标签： haskell lambda-calculus dependent-type

【解决方案1】：

我们需要某种上下文来跟踪 lambda 参数。但是，我们不一定需要实例化它们，因为bound 为我们提供了 de Bruijn 索引，我们可以使用这些索引来索引上下文。

实际上使用索引有点复杂，因为类型级机制通过Var的嵌套反映了当前范围的大小（或者换句话说，表达式中的当前深度） s。它需要使用多态递归或 GADT。它还阻止我们将上下文存储在 State monad 中（因为上下文的大小和类型在我们递归时会发生变化）。我想知道我们是否可以使用索引状态单子；这将是一个有趣的实验。但我离题了。

最简单的解决方案是将上下文表示为一个函数：

type TC  a = Either String a -- our checker monad
type Cxt a = a -> TC (Type a) -- the context

a 输入本质上是一个 de Bruijn 索引，我们通过将函数应用于索引来查找类型。我们可以通过以下方式定义空上下文：

emptyCxt :: Cxt a
emptyCxt = const $ Left "variable not in scope"

我们可以扩展上下文：

consCxt :: Type a -> Cxt a -> Cxt (Var () a)
consCxt ty cxt (B ()) = pure (F <$> ty)
consCxt ty cxt (F a)  = (F <$>) <$> cxt a

上下文的大小在Var 嵌套中编码。大小的增加在返回类型中很明显。

现在我们可以编写类型检查器了。这里的重点是我们使用fromScope 和toScope 来进入活页夹，并且我们携带了一个适当扩展的Cxt（其类型正好对齐）。

data Term a
  = Var a
  | Star -- or alternatively, "Type", or "*"
  | Lam (Type a) (Scope () Term a)
  | Pi  (Type a) (Scope () Term a)
  | App (Type a) (Term a)  
  deriving (Show, Eq, Functor)

-- boilerplate omitted (Monad, Applicative, Eq1, Show1 instances)

-- reduce to normal form
rnf :: Term a -> Term a
rnf = ...

-- Note: IIRC "Simply easy" and Augustsson's post reduces to whnf
-- when type checking. I use here plain normal form, because it 
-- simplifies the presentation a bit and it also works fine.

-- We rely on Bound's alpha equality here, and also on the fact
-- that we keep types in normal form, so there's no need for
-- additional reduction. 
check :: Eq a => Cxt a -> Type a -> Term a -> TC ()
check cxt want t = do
  have <- infer cxt t
  when (want /= have) $ Left "type mismatch"

infer :: Eq a => Cxt a -> Term a -> TC (Type a)
infer cxt = \case
  Var a -> cxt a
  Star  -> pure Star -- "Type : Type" system for simplicity
  Lam ty t -> do
    check cxt Star ty
    let ty' = rnf ty
    Pi ty' . toScope <$> infer (consCxt ty' cxt) (fromScope t)
  Pi ty t -> do
    check cxt Star ty
    check (consCxt (rnf ty) cxt) Star (fromScope t)
    pure Star
  App f x -> 
    infer cxt f >>= \case
      Pi ty t -> do
        check cxt ty x
        pure $ rnf (instantiate1 x t)
      _ -> Left "can't apply non-function"

这是the working code containing 上述定义。我希望我没有把事情搞砸。

【讨论】：