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.
Conversation
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).
1
i can’t google that, what do you mean?
1
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
You can get away with this because at the time you want to evaluate a term you know the size of the environment, so you cam convert the indices you encounter to levels easily.
Then because they are levels in some captured environment you can move them around / copy them freely without shifting.
1
Then you can do a readback from values into terms by giving a level that you use to recover the indices.