haskell – 使用“bound”来对依赖的lambda抽象进行类型检查的正确方法是什么？

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

haskell – 使用“bound”来对依赖的lambda抽象进行类型检查的正确方法是什么？

相关文章