tis heartening to know I am not the only one
Conversation
how does your naive version work? just brute force shift everything under binders?
This Tweet was deleted by the Tweet author. Learn more
This Tweet was deleted by the Tweet author. Learn more
Ahh, cool beans. Yeah, I think globals are stored as values in the internship report's one too, going off the repository. Part of my challenge has been figuring out how to do that with my current scheme, where I store things as values.
1
This Tweet was deleted by the Tweet author. Learn more
I've been trying to avoid globals because partly I want to try to head more towards something like 1ML, but perhaps that's a fool's effort. 😬
1
1
I think one of the issues with how I'm shifting neutrals (by putting it as a shift on the var constructor) is that I don't know whether to either accumulate the shift, or forget about it. In the NbE rules given in the thesis they don't shift through variables.
1
s/thesis/report/
1
We seem to only want to accumulate shift onto the neutral term if the _value_ is accessible in the environment
1
If it's a binder then we discard it. At least that's how it seems to work for functions. Not sure about dependent sums/records.
The type of the identity function is a good example (sorry, I'm abusing the Id identifier here):
> let Id = (Fun (A : Type) -> A -> A) in Id^1
Fun (A : Type^1) -> A -> A : Type^2
We want to shift through `Id^1`, because it has a definition in the environment. But not the `A`s.