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.
Conversation
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.
2
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).
I dunno any other name for it. It’s what I use in rust-nbe-for-mltt and I think it’s used in mini-tt. You use indices in the terms and levels in the values. Avoids you having to do all the shifting you’d need to do with pure indices.
2
Show replies