Prevent accidental Cthulhu summons #1760
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
isovector
changed the title
isovector
commented
Apr 19, 2021
jneira
approved these changes
Apr 20, 2021
Ailrun
reviewed
Apr 20, 2021
| cthulhu (First fp') = _ | ||
| cthulhu (Second fp') = _ | ||
| cthulhu (Alongside fp' fp_rca'b') = _ | ||
| cthulhu (Fanout fp' fp_rcab') = _ |
There was a problem hiding this comment.
This means if we have a constructor like R'lyeh :: FreePro r c x y -> FreePro r c (Either a x) (Either b y) -> FreePro r c a b (or more complex second argument) then we can still summon one, right?
There was a problem hiding this comment.
The _<blah> bit only shows up if all of your type arguments are variables, which prevents arbitrarily long terms. I think we're still safe.
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.
This PR makes Wingman pick more idiomatic identifiers when generating new variables.
Before, the situation was quite bad for complicated types:
But now, Wingman uses a bunch of rules to find acceptable names. It categorizes variables by their purpose, correlating roughly with intended semantic meaning. Right now, that means we can find things like monadic actions, functions, and predicates. For each purpose, we give a preferred ordering of variable names, and Wingman uses the first one that is available.
For long type constructors, Wingman will attempt to split them by camel case, turning eg
HelloWorldintohw. if that fails, it uses the first syllable of the constructor.This is not yet a perfect solution to naming, which should constrain names based on the relationship. But it's a significant step forward.