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
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!
The older paper.