当检查依赖的λ项时,例如λt:*。 λx:t。 x,我需要:
>“输入”外部lambda绑定器,通过将t实例化为某个东西
> Typecheckλx:t。 x,产生∀x:t。 Ť
>抽象t,产生∀t:*。 ∀x:t。 Ť
如果lambda是不依赖的,我可以在步骤1中使用类型实例化t,因为类型是所有我需要知道的变量,而在步骤2中进行类型检查。
但是在步骤3中,我缺少决定哪些变量要抽象出来的信息。
我可以引入一个新的名称供应,并实例化一个包含类型和唯一名称的Bound.Name.Name。但是我觉得用绑定我不需要生成新的名字。
实际上使用索引有点涉及到,因为通过嵌套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以上的定义。我希望我没有把它弄得太糟糕了。
原文地址:https://www.jb51.cc/javaschema/282264.html
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。