[Haskell-cafe] Bound library + recovering de Bruijn indices
edwards.benj at gmail.com
Tue Mar 18 09:28:32 UTC 2014
On Sun Mar 16 2014 at 17:02:35, Benjamin Edwards <edwards.benj at gmail.com>
> 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.
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...
More information about the Haskell-Cafe