On Sun Mar 16 2014 at 17:02:35, Benjamin Edwards
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?