finish up nbe, add tests

[jonsterling]

• [x] need to generate open environments from contexts
• [x] define nbe functions for terms and types
• [x] write some quick tests; I have no doubt that there are bugs in the code which has never been run. For instance, maybe there is some mistake mediating between use of be druijn indices in the syntax, and de bruijn levels in the semantics. (This is part of Abel's style which I didn't quite understand, but I followed it.)

[jonsterling]

I started restructuring the language a bit in terms of explicit substitutions; this seems crucial (?) for efficient normalization and typechecking.

I still haven't exactly decided how I want to implement coe and friends. These operators are a bit strange, since they really behave like a kind of generic element of the (Pi, Sigma, etc.) types, and their operational behavior is usually a kind of eta expansion. So, this suggests to me that the right place to "implement" their behavior is during readback, but I'm not sure.

[ghost]

I started restructuring the language a bit in terms of explicit substitutions; this seems crucial (?) for efficient normalization and typechecking.

I've been thinking about this in general for awhile and it seems to me that hash-consing with memoization will be superior to explicit substitutions strictly as far as efficiency is concerned because you will get maximal sharing and caching of repeated operations like substitution. If the goal is primarily to build an interpreter, it seems hard to beat that.

Explicit substitutions and similar machinery seem more interesting if the goal is to build an abstract machine with an eye toward compilation and some sort of RTS.

[jonsterling]

Hmm, that’s very interesting. My one concern about hashconsing is it seems to make the code a bit more gnarly, but I’d be open to it for sure. Re explicit subst, another thing I like about them is that it is easy to implement simple mindedly, and I never need to implement the substitution function for my language.

Let’s keep the hashconsing approach on the table, and maybe we should switch to it once the rest of the thing is a bit more solidified!

On Feb 9, 2018, at 3:53 PM, Darin Morrison notifications@github.com wrote:

I started restructuring the language a bit in terms of explicit substitutions; this seems crucial (?) for efficient normalization and typechecking.

I've been thinking about this in general for awhile and it seems to me that hash-consing with memoization will be far superior to explicit substitutions strictly as far as efficiency is concerned because you will get maximal sharing and caching of repeated operations like substitution. If the goal is primarily to build an interpreter, it seems hard to beat that.

Explicit substitutions and similar machinery seem more interesting if the goal is to build an abstract machine with an eye toward compilation and some sort of RTS.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

[jonsterling]

I've now implemented the NBE roundtrip, so I'm closing this ticket; discussion of alternative syntactic representation and memoization is moved to #8.