我正在执行一个简单的依赖类型的语言，类似于一个
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以上的定义。我希望我没有把它弄得太糟糕了。
