Erased data and record types and modules #6294
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
nad
force-pushed
the
issue4743
branch
2 times, most recently
from
7993a7b to
656eff9
Compare
The double-checker does not seem to care too much about erasure, so I don't plan to include any changes to it in this pull request. |
|
The pull request includes the following text in TODO: Explain how the reflection machinery interacts with run-time
irrelevance. |
jespercockx
reviewed
Nov 26, 2022
There was a problem hiding this comment.
Thanks, this looks great to me. Two small remarks:
- The double checker is maintained but is currently too liberal regarding modalities, this should be fixed but not as part of this PR.
- Regarding reflection, I recently added the ability to run erased macros (see Allow running of erased macros #5744). I'm not sure what else we should mention regarding the interaction between erasure and reflection.
The manual contains an incomplete explanation of when Agda switches between compile-time and run-time mode. Switches performed by the reflection machinery are omitted, and should be included. |
jespercockx
approved these changes
Dec 1, 2022
The field envModality was removed in favour of envRelevance and envQuantity, because (according to some comment) cohesion shouldn't be in the environment. The LensModality instance for TCEnv and the lens eModality were also removed. Furthermore the LensRelevance and LensQuantity instances for TCEnv were removed. Now every change of the environment's relevance component is performed using the lens eRelevance, and every change of the environment's quantity component is performed using eQuantity.
Furthermore applyQuantityToJudgementOnly was renamed to applyQuantityToJudgement and generalised.
When the hard compile-time mode is used all constants that are added to the signature are made erased. The hard compile-time mode is entered when an erased definition is checked, but not when a type-signature is checked. This is related to issue #6271: When an erased constructor is type-checked the hard compile-time mode is entered, and all associated definitions become erased.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
See issue #4743.
I also addressed issue #6271: If a constructor is erased, then the corresponding generated definitions are also erased. However, I don't know if this is correct.
I have not modified the double-checker, and I don't know if that is necessary. (Is the double-checker still maintained?)