[Haskell-cafe] How to walk under binders "for free" in 'bound'?
Christiaan Baaij
christiaan.baaij at gmail.com
Mon Jul 14 15:51:14 UTC 2014
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
More information about the Haskell-Cafe
mailing list