Get rid of --large-indicies using higher levels
#33
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
ibbem
force-pushed
the
no-large-indicies-by-level-generalization
branch
from
8fab9ea to
8a264c1
Compare
Agda disables this option by default because it can cause inconsistencies (especially with `--forced-argument-recursion`, which is enabled by default). Hence, it's better to disable it as well. Unfortunately, `MonadWriter` cannot handle different `Level`s for the Value and the Result type. Hence, `ignore-value` and `return-value` hack is required to shift the `Level`s as required. There are still some cases in `IndexedSet` where the `Level`s could be generalized even more. I know of at least the `Transitive` laws. However, the standard library doesn't provide a `Trans` definition allowing different indices as for homogeneous transitivity. We don't need this generality yet, so I just left it out for now.
ibbem
force-pushed
the
no-large-indicies-by-level-generalization
branch
from
8a264c1 to
bc95fea
Compare
|
As discussed in our meeting, I will merge this now. |
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.
Agda disables the option
--large-indiciesby default because it can cause inconsistencies (especially with--forced-argument-recursion, which is enabled by default). Hence, it's better to disable it as well.Unfortunately,
MonadWritercannot handle differentLevels for the Value and the Result type. Hence, theignore-valueandreturn-valuehack is required to shift theLevels as required.There are still some cases in
IndexedSetwhere theLevels could be generalized even more. I know of at least theTransitivelaws. However, the standard library doesn't provide aTransdefinition allowing different indices as for homogeneous transitivity. We don't need this generality yet, so I just left it out for now.