Dear list, I'm trying to implement a small dependently typed language (based on [1]) using the generalised De Bruijn indices from the 'bound' library [2]. My main two datatypes are:
data Binder n a = Lam {binder :: Name n a} | Pi {binder :: Name n a}
Representing my two types of binders, and:
data Term n a = Var !a | Universe Integer | App !(Term n a) !(Term n a) | Bind !(Binder n (Term n a)) !(Scope (Name n ()) (Term n) a)
Representing terms. My problem lies with implementing type-inference for lambda-binders. Originally I started with:
inferType1 :: Eq a => (a -> Term n a) -- ^ Context -> Term n a -- ^ Term -> Term n a -- ^ Inferred type inferType1 ctx (Var a) = ctx a inferType1 ctx (Bind (Lam b) s) = Bind (Pi b) s' where s' = toScope . inferType1 ctx' . fromScope $ s ctx' = unvar bCtx fCtx bCtx _ = fmap F $ extract b fCtx = fmap F . ctx
Where `toScope . inferType1 ctx' . fromScope` entails doing three subsequent traversals: - `fromScope` traverses the term in `s`, which quotients placements of 'F' distributing them to the leaves - `inferType ctx'` then traverses the result of `fromScope` to infer the type - `toScope` transforms the inferred type to a generalised De Bruijn form, requiring a full tree traversal. Also, the new context, `ctx'`, is defined in term of a traversal (fmap). Also note that, for every Scope I walk under, `ctx'` gets an additional traversal. Doing so many traversals seems/is expensive, so after some thinking I improved `inferType2` to:
inferType2 ctx (Bind (Lam b) s) = Bind (Pi b) s' where s' = Scope . inferType2 ctx' . unscope $ s ctx' = unvar bCtx fCtx bCtx _ = fmap (F . Var) . extract $ b fCtx = fmap (F . Var) . inferType2 ctx
Where the only traversal needed to get `s'` is done by `inferType ctx'`. However, the new context, `ctx'`, remains defined in terms of traversals (fmap). Again, note that, for every Scope I walk under, `ctx'` gets an additional traversal. I could get rid of the remaining traversals in `ctx'` by implementing `inferType3` as:
inferType3 ctx (Bind (Lam b) s) = Bind (Pi b) s' where s' = Scope . inferType3 ctx' . unscope $ s ctx' = unvar bCtx fCtx bCtx _ = Var . F . extract $ b fCtx = Var . F . inferType3 ctx
But if I do that I start running into problems elsewhere, because the context is now returning lifted expressions. These problems arise for example in `inferPi`, which checks if the type of a term is a pi-binder:
inferPi :: Eq a => (Term n a -> Term n a) -- ^ Type inference function -> Term n a -> (n,Term n a,Scope (Name n ()) (Term n) a) inferPi inferTy tm = case inferTy tm of Bind (Pi b) s -> (name b, extract b, s) t -> error "Function expected"
Let's assume that I'm doing type inference for the term:
\(a:*).\(b:*).\(f:(pi(_:a).b).\(x:a).f x
Where `*` is `Universe 0`. In the application `f x`, I need to determine if `f` has a pi-type. When using either `inferType` or `inferType2`, I will see that `f` has the shape:
Bind (Pi {binder = Name "_" (Var (F (Var (F (Var (F (Var (B (Name "a" ())))))))))}) (Scope (Var (F (Var (F (Var (F (Var (B (Name "b" ()))))))))))
And so, `inferPi` will have no problems seeing that `f` has a pi-type. However, when using `inferType3`, where the context, `ctx`, returns lifted expressions , `f` has the shape:
Var (F (Var (F (Bind (Pi {binder = Name "_" (Var (F (Var (B (Name "a" ())))))}) (Scope (Var (F (Var (B (Name "b" ()))))))))))
Now `inferPi` will have problems seeing that `f` has a pi-type, it will need to quotient out and distribute the (Var . F) first. The (non-)solution is to quotient and distribute on demand, by defining `inferType4`:
inferType4 :: Eq a => (a -> Term n a) -- ^ Context -> (Term n a -> Term n a) -- Quotient and distribute (Var . F) -> Term n a -- ^ Term -> Term n a -- ^ Inferred type inferType4 ctx dist (Var a) = dist (ctx a) inferType4 ctx dist (Bind (Lam b) s) = Bind (Pi b) s' where s' = Scope . inferType4 ctx' dist' . unscope $ s ctx' = unvar bCtx fCtx bCtx _ = Var . F . extract $ b fCtx = Var . F . inferType4 ctx dist
dist' (Var (F a)) = fmap (F . Var) . dist $ a dist' e = e
However, `inferType4` simply moves the traversal from one place to the other, giving us no improvement over `inferType2`. What we do however see is that, after having descended two Scopes, we would get a `dist'` function that does:
fmap (F . Var) . fmap (F . Var) . dist
This gives me hope that instead of having to do two traversals using `fmap`, we could get one traversal of the form:
fmap (F . Var . F . Var) . dist
According to the Functor law. I have absolutely no idea how to achieve this single traversal solution though. This leads me to have several, quite general, questions: - Is there a way to get a `dist` function, as defined in `inferType4`, that does a single traversal? - Would it be possible to even get rid of the traversal for the context `ctx`? Perhaps by approaching the `inferType` function completely differently? - Or is there simply no way to implement `inferType` for free (without traversals) using generalised De Bruijn indices? The complete code can be found at: https://gist.github.com/christiaanb/4e0fd1777aee927999aa Cheers, Christiaan Baaij [1] http://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/ [2] http://hackage.haskell.org/package/bound-1.0.3