S. Doaitse Swierstra wrote:
This problem of dynamically transforming grammars and bulding parsers out of it is addressed in:
@inproceedings{1411296, author = {Viera, Marcos and Swierstra, S. Doaitse and Lempsink, Eelco}, title = {Haskell, do you read me?: constructing and composing efficient top-down parsers at runtime}, [...] }
Indeed, it looks as if you solved exactly the problem that vexed me! I had just found the presentation that corresponds to the paper you mention, and I also found a preprint for "Typed transformations of Typed Abstract Syntax" which I am studying at the moment. I must say your construction is, well, involved... Not that I want to belittle this really astounding and clever achievement... but one disadvantage of your approach (which it shares with almost all examples I have seen for dependently typed or heterogeneous collections) is that (IIUC) the typed map from references to abstract syntactic terms is operationally an association list, indexed by unary numbers. I would expect this to scale poorly if the number of references (e.g. nonterminals) gets large. I think it would make for quite an interesting research project to study whether it is possible to achieve the same level of precise static typing with more efficient data structures. I imagine that using some 'fake dependent type' variant of [Bit] for the key and the equivalent of a patricia tree for the map could perhaps be made to work??? Cheers Ben