Ooh, and just don't store the synthesized type when they are omitted, right! Gotcha! 🙂
Conversation
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!
2
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
Syntax is the thing you are evaluating from - the 'terms', domain are what you evaluate to - the 'values'. I think. But it's still kinda confusing why they ended up being called that.
1
I know the concepts. I just think it’s terrible jargon that fails to communicate unless everyone first syncs up on nbe.
1
1
Show replies