Has anybody seen a type checker for STLC, or even better, a CoC, that uses (in part) something like pull parsing for dealing with ASTs? xmlpull.org/history/index. Super curious about if it could reduce memory allocation overhead for certain parts of the type checker. 🤔
Conversation
I'm interested in both the performance of type checking, but also in allowing for flexibility in the user-facing syntax vs serialization format - and even in projectional/nodal editing later on. Visitors seemed like an interesting option too: lihaoyi.com/post/ZeroOverh
1
1
I'm guessing you'll need places where you allocate trees of nodes as 'checkpoints' but it'd be nice to reduce that as much as possible. It would be also neat to design the core calculus in such a way that is amendable to streaming, but I've got no idea how to do that. 🤔
Replying to
I've done some experiments with elaborating directly off S-Expressions (eg. gist.github.com/brendanzab/d37) but I'm thinking that this is still kind of annoying because it requires you to allocate an intermediate AST…
1
Here's an quick start on a mock-up of pull-based processing for a lambda calculus - takes a stream of nominal term events and yields locally nameless term events:
1
2
As you can see, the traditional 'tree-based' syntax tree is very allocation heavy, and has lots of pointer indirection leading to poor data locality. Maybe using an allocator would help with that somewhat, but it makes me a tad sad. Hoping there is a better way!
2
2
Yeah I've seen Nanopass! Do they cover ways of fusing passes so that you don't have to allocate intermediate data structures?
1
Show replies