使用'bound'进行类型检查依赖lambda抽象的正确方法是什么？

Question

我正在实现一种简单的依赖类型语言,类似于Lennart Augustsson描述的语言,同时还使用绑定来管理绑定.

当检查依赖的lambda术语时,例如?t:* . ?x:t . x,我需要:

1. "Enter"键外的λ粘结剂,通过实例t来的东西
2. Typecheck ?x:t . x,屈服?x:t . t
3. Pi抽象t,屈服?t:* . ?x:t . t

如果lambda是非依赖的,我可以在步骤1中t使用它的类型实例化,因为类型是我在第2步的类型检查时需要知道的变量.但是在第3步我缺乏决定哪些变量的信息摘要.

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

有缺点的替代解决方案吗？

Answer 1

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

实际上,使用索引有点涉及,因为类型级机制通过Var-s 的嵌套反映当前范围的大小(或者换句话说,表达式中的当前深度).它需要使用多态递归或GADT.它还阻止我们将状态存储在状态monad中(因为大小因此上下文的类型随着我们的递归而改变).我想知道我们是否可以使用索引状态monad; 这将是一个有趣的实验.但我离题了.

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

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

该a输入本质德布鲁因指标,我们通过应用函数索引查找一个类型.我们可以通过以下方式定义空上下文:

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"

这是包含上述定义的工作代码.我希望我没有把它弄得太糟糕.