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

Benjamin Edwards edwards.benj at gmail.com
Sun Mar 16 17:02:42 UTC 2014

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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140316/b632f8b2/attachment.html>

More information about the Haskell-Cafe mailing list