By c) do you mean just storing the types as values in the elaborated AST?
Conversation
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.
1
1
Then because they are levels in some captured environment you can move them around / copy them freely without shifting.
Then you can do a readback from values into terms by giving a level that you use to recover the indices.