Conversation

Yeah, I really need to figure out that co-debruijn stuff, and how/if it relates to the nifty 'semantic type checking' that

@jonsterling

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

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

1

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

Replying to

2:33 AM · Apr 23, 2019Twitter Web Client

Agreed. I'm definitely interested in figuring out something better, even just for NbE. Let me know if you have any ideas!

Replying to

and

I'm trying to figure out a better way to organise my modules in my core crate: github.com/brendanzab/rus

1