atm core (the syntax) is inside the syntax module. and domain is in the syntax module too (kind of at odds with nbe). Not sure what to call these modules and where to put them.
Conversation
At least I'm pretty happy with the names I've used for the variants in my core syntax and elsewhere: github.com/brendanzab/rus
2
1
I've found 'level' to be annoying, because it really feels like it should be called an 'index'. Because you're indexing from the start of the environment.
1
ok, so phrased differently: you’re using codebruijn aka “debruijn levels” aka distance from the top for static semantics, and debruijn indices / aka stack offset for dynamic semantics?
2
1
(you mentioned Conor's "codebruijn" work earlier -- if we're thinking of the same thing (arxiv.org/abs/1807.04085), then that, and dB levels, are two *entirely different* things which are in some way dual to dB indices)
1
1
So are you saying that what I'm doing is _not_ co-debruijn? (I had assumed not before Carter mentioned it, but I haven't yet got my head around Conor's paper yet...)
1
I don't know whether "co-debruijn" is an "officially existing" term at all (it could be, for all I know)
all I'm saying is that de-Bruijn indices, de-Bruijn levels, and Conor's paper which I linked are *three* different things
1
Oh, I see he does call it co-de-Bruijn in the abstract :-)
1
I just assumed that given "Co-de-Bruijn representation is even less suited to human comprehension than de Bruijn syntax", what I was doing couldn't possibly be that, because I could sort of understand it? A little?
1
2
yeah in terms of human comprehension I think levels > indices > co-de-bruijn :)
1
1
Yeah, the reason I liked this semantic type checking thing is that it is levels and indicies together, and kinda not too hard to get one's head around, and seems not too terrible perfomance wise...
Yes : Co debrujn is levels. I actually like Co because it means reversed!
Either way, I like it as a way to think of non local variables. The way I sortah think about it is open variables are best as co deb. Local variables as deb. Then Inlinging and cse are happy times