[Haskell-cafe] How to walk under binders "for free" in 'bound'?

[Christiaan Baaij]

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