[Haskell-cafe] Bound library + recovering de Bruijn indices

[Benjamin Edwards]

On Sun Mar 16 2014 at 17:02:35, Benjamin Edwards <edwards.benj at gmail.com>
wrote:

> Hi Cafe
>
> I am currently experimenting with the excellent bound library. I want to
> implement the simply typed lambda calc from TAPL (no type inference yet).
> When moving under a binder I want to extend my context and then look up
> bound terms by their indices using list indexing. I would have thought I
> could use something like foldMapScope to recover the bound variables, then
> write some function to calculate the depth of the "listy" type value
> returned and thus recover the index. However! The type returned is
> non-regular and I cannot for the life of me figure out anything that
> doesn't involve GHC complaining about infinite types.
>
> Any pointers on how this can be accomplished?
>
> For the record, this is what I have that works at the moment.
>
> http://lpaste.net/101279
>

I am currently trying to write a function using polymorphic recursion to
get around the nested type but not having any luck. This is what I have so
far (+the paste above):

peel :: (forall a. Var () a -> Int) -> Var () r -> Int
peel f x = f x

g n (F (TVar x)) = peel (g (n + 1)) x
g n (B ()) = 0

Var is iso to Either (from the bound library)

And the idea is to count the level of nested Fs in the sum type. Can anyone
give me any pointers?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140318/80ef2fc1/attachment.html>