Add `Val` and `Neutral` for NbE

[ice1000]

trafficstars

Neutralization by Elimination

Does that sound like a plan? @re-xyr

[re-xyr]

What is neutralization by elimination?

[ice1000]

What is neutralization by elimination?

It's a meme

[re-xyr]

Then it doesn’t sound like a plan

[ice1000]

Then it doesn’t sound like a plan

So, I actually meant normalization by evaluation. I guess we need to add Value and Neutral, and then implement eval, right? I think it should be like that

[re-xyr]

Yes, and quote. And then we modify all type-inspecting functions (check, unify, etc) to use Vals for types.

[re-xyr]

We may not need to add a dedicated Neutral type even. Neutral can be a constructor for Val, consisting of a neutral head plus a spine.

[ice1000]

We may not need to add a dedicated Neutral type even. Neutral can be a constructor for Val, consisting of a neutral head plus a spine.

What kind of term will be a neutral spine?

[re-xyr]

Any non-canonical term not subject to beta-reduction. In particular, they are prim calls, function calls, meta calls, and local Var applications.

[re-xyr]

For the neutrals subject to delta reduction, I will store a field of type Lazy<Maybe<Val>> for the reduced result.

[ice1000]

Wow, we have LazyValue from kala https://github.com/Glavo/kala-common/blob/main/kala-base/src/main/java/kala/value/LazyValue.java