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
perso.ens-lyon.fr/pierre.lescann / semanticscholar.org/paper/Explicit
looks like co-debruijn as for as I know ?
1
1
Ooh that might be it. I’d need to investigate more deeply. Thanks!
That random paper I linked and the more recent Conor one might be more intelligible terminology wise.
1
I think I've seen this one before, and tbh it looks a bit easier, but I dunno!
1
Show replies
I find the levels vs indices or syntax vs domain vs terms to be kinda fuzzy descriptively
1
syntax vs domain comes up a bit in NbE
1
Show replies