What is the right way to typecheck dependent lambda abstraction using 'bound'?

Question

I am implementing a simple dependently-typed language, similar to the one described by Lennart Augustsson, while also using bound to manage bindings.

When typechecking a dependent lambda term, such as λt:* . λx:t . x, I need to:

1. "Enter" the outer lambda binder, by instantiating t to something
2. Typecheck λx:t . x, yielding ∀x:t . t
3. Pi-abstract the t, yielding ∀t:* . ∀x:t . t

If lambda was non-dependent, I could get away with instantiating t with its type on step 1, since the type is all I need to know about the variable while typechecking on step 2. But on step 3 I lack the information to decide which variables to abstract over.

I could introduce a fresh name supply and instantiate t with a Bound.Name.Name containing both the type and a unique name. But I thought that with bound I shouldn't need to generate fresh names.

Is there an alternative solution I'm missing?

Answer 1

We need some kind of context to keep track of the lambda arguments. However, we don't necessarily need to instantiate them, since bound gives us de Bruijn indices, and we can use those indices to index into the context.

Actually using the indices is a bit involved, though, because of the type-level machinery that reflects the size of the current scope (or in other words, the current depth in the expression) through the nesting of Var-s. It necessitates the use of polymorphic recursion or GADTs. It also prevents us from storing the context in a State monad (because the size and thus the type of the context changes as we recurse). I wonder though if we could use an indexed state monad; it'd be a fun experiment. But I digress.

The simplest solution is to represent the context as a function:

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

The a input is essentially a de Bruijn index, and we look up a type by applying the function to the index. We can define the empty context the following way:

emptyCxt :: Cxt a emptyCxt = const $ Left "variable not in scope" 

And we can extend the context:

consCxt :: Type a -> Cxt a -> Cxt (Var () a) consCxt ty cxt (B ()) = pure (F <$> ty) consCxt ty cxt (F a)  = (F <$>) <$> cxt a 

The size of the context is encoded in the Var nesting. The increase in the size is apparent here in the return type.

Now we can write the type checker. The main point here is that we use fromScope and toScope to get under binders, and we carry along an appropriately extended Cxt (whose type lines up just perfectly).

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" 

Here's the working code containing the above definitions. I hope I didn't mess it up too badly.