This is the main part that does the work of elaborating items: github.com/brendanzab/rus - I'm thinking it might be worth limiting the the `read_back_value` line to lookup variables in my implementation of nbe?
Conversation
So you want to weaken forward declared types to the scope of their definitions. Readback is not good because you don't want normal forms in elab output. I can think of several solutions varying in simplicity and generality.
1
1
a) Implement weakening directly on core syntax, store plain elaborated types in forward_declarations, weaken them as needed. This is pretty efficient because you only need to weaken each forward declared type once.
1
1
b) Distinguish "top" and "local" contexts already in syntax, use de Bruijn levels for top variables, thereby making weakening free.
1
2
c) Just don't weaken forward decl types. You only ever lose scoping information by weakening, you can still do everything if forward types stay in their original scope.
1
1
c) seems nicest and easiest to me for your current impl, a) is OK and simple but I'd generally avoid weakening, b) is not so simple but you may need it anyway if you also want non-bloated meta solutions.
1
By c) do you mean just storing the types as values in the elaborated AST?
1
I mean, when you elaborate a forward type, it's valid in the current context, and then you leave the type in that context, so check_items returns something which contains forward types and definitions interleaved (or in any way which remembers scopes).
2
1
Ooh, and just don't store the synthesized type when they are omitted, right! Gotcha! 🙂
2
What’s a good microcosm of what you mean by forward decls and back references here? Is this really just a matter of ensuring sharing ?
1
a forward decl is something like
forward : Bool;
bar : Bar;
forward = true;
Note that when I elaborate the type annotation `Bool` into the core syntax it is using debruijn indices, meaning I can't freely copy that term around and use it in nested scopes.
My value syntax on the other hand uses De Bruijn levels, which can be moved around between scopes easily, but can't be as easily compared for alpha equivalence as the core syntax.
1
Not sure if that really answers your question though! And I'm still figuring this stuff out.
conor has a cute recent paper that kinda makes a nice case for using co-debruijn for toplevel stuff
1
1
Yeah, I really need to figure out that co-debruijn stuff, and how/if it relates to the nifty 'semantic type checking' that let me know about (that I'm currently rewriting my stuff to use).
1
Show replies