Type case operator that gets stuck on unsolved metas (i.e. THE DREAM ACHIEVED) #53
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
This is the equivalent of Racket's make-syntax-introducer and generate-temporaries.
This makes debugging much easier.
Some examples relied on this bug - it's now fixed. Fixes #48.
This commit contains the final bits of run-time and expander support for a monadic type-case operator that gets stuck on unsolved metas. The which-problem example has been updated with a demonstration that the type checker's order of traversal is independent of the availability of type information to the macro expander.
|
|
||
| (m) | ||
|
|
||
| (example (case (unit) | ||
| ((m) (true)))) | ||
|
|
||
| (define-macros |
There was a problem hiding this comment.
This is so cool 😄
There was a problem hiding this comment.
We could try to imlement something like Cryptol's zero operator using this. That'd be fun :-)
gelisam
reviewed
May 6, 2020
| @@ -15,6 +15,7 @@ dependencies: | |||
| - lens | |||
| - megaparsec | |||
| - mtl | |||
| - n-ary-functor | |||
There was a problem hiding this comment.
wow, you used my n-ary-functor package! I'm so proud! but... where are you using it? I don't see any import NAryFunctor.
|
I used it and then unused it again - will fix!
…On Tue, May 5, 2020, 21:18 Samuel Gélineau ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In package.yaml
<#53 (comment)>:
> @@ -15,6 +15,7 @@ dependencies:
- lens
- megaparsec
- mtl
+ - n-ary-functor
wow, you used my n-ary-functor package! I'm so proud! but... where are you
using it? I don't see any import NAryFunctor.
—
You are receiving this because you modified the open/close state.
Reply to this email directly, view it on GitHub
<#53 (review)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AAA4FAWQ2IZ3Q4INS766Q3LRQDQIHANCNFSM4MWQT7KQ>
.
|
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 is based on #47, because of the various bug fixes and such in it. On top of #47's changes, it has the following:
expressionconstructor ofProblemhas been given a primitive representation of types at the next phase as an argument (the new built-in typeType)type-caseoperator allows matching on aTypein a monadic context, getting stuck if that type is not yet determined. Type patterns are expansion positions, just like data patterns.Things to be improved over time:
type-casenever gets un-stuck, the error message is quite bad. We probably need some provenance tracking for metas to tell it where they are from, at the very least.