我正在执行一个简单的依赖类型的语言，类似于一个
described by Lennart Augustsson，同时也使用
bound来管理绑定。
当检查依赖的λ项时，例如λt：*。 λx：t。 x，我需要：
>“输入”外部lambda绑定器，通过将t实例化为某个东西
> Typecheckλx：t。 x，产生∀x：t。 Ť
>抽象t，产生∀t：*。 ∀x：t。 Ť
如果lambda是不依赖的，我可以在步骤1中使用类型实例化t，因为类型是所有我需要知道的变量，而在步骤2中进行类型检查。
但是在步骤3中，我缺少决定哪些变量要抽象出来的信息。
我可以引入一个新的名称供应，并实例化一个包含类型和唯一名称的Bound.Name.Name。但是我觉得用绑定我不需要生成新的名字。
有没有一个替代解决方案我失踪了？
我们需要某种上下文来跟踪lambda参数。然而，我们不一定需要实例化它们，因为绑定给了我们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输入本质上是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以上的定义。我希望我没有把它弄得太糟糕了。
