Fix assert error with relational lenses #1143
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
dhil
approved these changes
Jun 22, 2022
|
Yes. I have been meaning to review and refactor the lens subsystem at some point before my memories (and ability to armtwist @rudihorn) fade. We had been holding off in the hope of figuring out what a good general-purpose language extensibility capability that could express lenses would look like but didn't get there (Rudi's thesis has a chapter showing how to embed lenses in Haskell though, so if we just added type classes, families and GADTs then I think we would be mostly there.) This should be recorded as an enhancement issue. |
Open
|
Thanks for the quick merge! For the avoidance of doubt, I think splitting a lot of the lens code was a reasonable decision at the time and in keeping with best practices if we wanted a fully modular design for Links extensions. I just don't think this is the direction we ended up going for other extensions, so I agree that it's probably better to merge into the main codebase at some point. My point was mainly that the nature of Lens types (and 'sorts', in RL terminology) is sufficiently different from Links types (since it needs to track, for example, predicates) that it's not appropriate to extend the general Types visitor to support lens sorts. Rather, it's reasonable to expect someone wanting to do a lens-specific type traversal to implement their own visitor over lens sorts for that purpose. |
Orbion-J
pushed a commit
to Orbion-J/links
that referenced
this pull request
Jun 30, 2022
The `Lens` type traversal was unimplemented and filled in with an `assert false`. As a result, all RL code fails. I don't think there is any really sensible default traversal due to the complexity of the Lens types, so I have just filled it in with the identity. This doesn't stop someone implementing a traversal -- they'll just need to write one for `Lens.Type.t` type and plug it in as usual.
Orbion-J
pushed a commit
to Orbion-J/links
that referenced
this pull request
Jul 8, 2022
The `Lens` type traversal was unimplemented and filled in with an `assert false`. As a result, all RL code fails. I don't think there is any really sensible default traversal due to the complexity of the Lens types, so I have just filled it in with the identity. This doesn't stop someone implementing a traversal -- they'll just need to write one for `Lens.Type.t` type and plug it in as usual.
Orbion-J
added a commit
to Orbion-J/links
that referenced
this pull request
Jul 8, 2022
desalias inline alias = effectname and typename | init merge into 1 construct ok; still 2 contexts merge type and effect aliases contexts effectname body desugared into effectname allow better printing Revert "desalias inline" This reverts commit 49a9a61. Revert "effectname body desugared into effectname" This reverts commit 5150615. "effectname" in links-mode.el cleaning before pr re-cleaning effectname -> typename _::Kind Update bin/repl.ml Co-authored-by: Daniel Hillerström <[email protected]> Update bin/repl.ml Co-authored-by: Daniel Hillerström <[email protected]> Update bin/repl.ml Co-authored-by: Daniel Hillerström <[email protected]> Update bin/repl.ml Co-authored-by: Daniel Hillerström <[email protected]> Update bin/repl.ml Co-authored-by: Daniel Hillerström <[email protected]> Update core/desugarDatatypes.mli Co-authored-by: Daniel Hillerström <[email protected]> Update bin/repl.ml Co-authored-by: Daniel Hillerström <[email protected]> Update core/defaultAliases.ml Co-authored-by: Daniel Hillerström <[email protected]> Update core/desugarDatatypes.ml Co-authored-by: Daniel Hillerström <[email protected]> Update core/desugarDatatypes.ml Co-authored-by: Daniel Hillerström <[email protected]> rename alias_env -> tycon_env as originally Update core/desugarDatatypes.ml Co-authored-by: Daniel Hillerström <[email protected]> idem fixes & add primary kind in aliases new error kind mismatch fix : embeded errors fixes fix : underscore in effect app various fixes short type in effectname + short fun non desugar comment Attempted workaround for links-lang#1136 (links-lang#1138) always desugar op type with type application correction tests default arg in repl Effect aliasing (links-lang#1141) I added the possibility to write effect aliases, similarly as what already exists for types. - there is a new keyword `effectname` - to write an alias for an effect row : `effectname MyEffectRow(a, ... ,e::Eff, ...) = { Op1 : type, ... | e }` the arguments being type variable of any kind (kinds other than type must be explicit) - we can have, as above, an open row (the row variable is a parameter of the effect alias) or a closed one (just do not write the `| e` - To use it in a signature or in another type or effect alias just apply it with the right arguments as for `typename` things. - In arrows, we can use them as row variables: `() -MyEffectRow(args)-> ()` (idem with `~>`) - However, due to lack of kind inference, row variables and aliases have to be used carefully so that links does not think they are of kind type. We need to write them most of the time between braces ` { | ... }`. For instance, if you have `effectname E(a::Eff) = {X : ... | a }` and a row variable `e::Eff`, you will have to write `E({ |e})`. (Idem for another effect alias instead of the variable). This makes the usage of several nested aliases a bit messy, it would be nice if we could avoid it. - We cannot write recursive effect aliases for now. In the branch `visitor`, I added another transformer that makes possible simple recursion by inlining a mu type in one pass. - For now the aliases are replaced by the row they correspond to : we do not keep aliases. - In the repl, effect alias definitions are printed but without the braces ! Rows are in general printed without braces and the alias body is a row. => this might need to be enhanced About implementation, I copied and then merged most of the time what existed for `typename`. Co-authored-by: Daniel Hillerström <[email protected]> Fix assert error with relational lenses (links-lang#1143) The `Lens` type traversal was unimplemented and filled in with an `assert false`. As a result, all RL code fails. I don't think there is any really sensible default traversal due to the complexity of the Lens types, so I have just filled it in with the identity. This doesn't stop someone implementing a traversal -- they'll just need to write one for `Lens.Type.t` type and plug it in as usual. Make `custom_js_runtime` a multi option (links-lang#1146) Added the ability to link multiple custom js runtime files. Co-authored-by: s1908422 <[email protected]> Co-authored-by: Daniel Hillerström <[email protected]> Allow 'default' as an argument to settings in the REPL (links-lang#1147) Some settings has the value 'default'. Prior to this patch the value 'default' could not be written in the REPL, because it is token. This patch rectifies this problem by allowing the token 'default' to appear in settings argument position in the REPL. Co-authored-by: Daniel Hillerström <[email protected]> Allow record extension in presence of temporal projections (links-lang#1129) * Allow record extension in presence of temporal projections This allows record extension to play nicely with temporal projections. I was forgetting that all arguments to reduce_artifacts are already eta-expanded, so we can work with record literals. Fixes links-lang#1124. * Allow extension to work with (shallow) temporal projections We don't have the full generality due to links-lang#1130, but this patch should allow record extension to be used on temporal projections on variables / record literals. Removal of unused headless testing (links-lang#1152) The headless testing has been unused for about a year, because it is unmaintained. Even though it is not used, it generates a ton of security warnings here on GitHub. I am not interested in dealing with those, therefore this patch removes the headless testing directory from the source tree. Attempted workaround for links-lang#1136 (links-lang#1138) always desugar op type with type application correction tests default arg in repl Option -> Maybe fix (links-lang#1142) The `Option -> Maybe` refactoring patch links-lang#1131 missed one instance: the `max` function. This patch changes the type signature of `max` to use `Maybe` rather than `Option`. Effect aliasing (links-lang#1141) I added the possibility to write effect aliases, similarly as what already exists for types. - there is a new keyword `effectname` - to write an alias for an effect row : `effectname MyEffectRow(a, ... ,e::Eff, ...) = { Op1 : type, ... | e }` the arguments being type variable of any kind (kinds other than type must be explicit) - we can have, as above, an open row (the row variable is a parameter of the effect alias) or a closed one (just do not write the `| e` - To use it in a signature or in another type or effect alias just apply it with the right arguments as for `typename` things. - In arrows, we can use them as row variables: `() -MyEffectRow(args)-> ()` (idem with `~>`) - However, due to lack of kind inference, row variables and aliases have to be used carefully so that links does not think they are of kind type. We need to write them most of the time between braces ` { | ... }`. For instance, if you have `effectname E(a::Eff) = {X : ... | a }` and a row variable `e::Eff`, you will have to write `E({ |e})`. (Idem for another effect alias instead of the variable). This makes the usage of several nested aliases a bit messy, it would be nice if we could avoid it. - We cannot write recursive effect aliases for now. In the branch `visitor`, I added another transformer that makes possible simple recursion by inlining a mu type in one pass. - For now the aliases are replaced by the row they correspond to : we do not keep aliases. - In the repl, effect alias definitions are printed but without the braces ! Rows are in general printed without braces and the alias body is a row. => this might need to be enhanced About implementation, I copied and then merged most of the time what existed for `typename`. Co-authored-by: Daniel Hillerström <[email protected]> Fix assert error with relational lenses (links-lang#1143) The `Lens` type traversal was unimplemented and filled in with an `assert false`. As a result, all RL code fails. I don't think there is any really sensible default traversal due to the complexity of the Lens types, so I have just filled it in with the identity. This doesn't stop someone implementing a traversal -- they'll just need to write one for `Lens.Type.t` type and plug it in as usual. Make `custom_js_runtime` a multi option (links-lang#1146) Added the ability to link multiple custom js runtime files. Co-authored-by: s1908422 <[email protected]> Co-authored-by: Daniel Hillerström <[email protected]> wip Allow 'default' as an argument to settings in the REPL (links-lang#1147) Some settings has the value 'default'. Prior to this patch the value 'default' could not be written in the REPL, because it is token. This patch rectifies this problem by allowing the token 'default' to appear in settings argument position in the REPL. Co-authored-by: Daniel Hillerström <[email protected]> Allow record extension in presence of temporal projections (links-lang#1129) * Allow record extension in presence of temporal projections This allows record extension to play nicely with temporal projections. I was forgetting that all arguments to reduce_artifacts are already eta-expanded, so we can work with record literals. Fixes links-lang#1124. * Allow extension to work with (shallow) temporal projections We don't have the full generality due to links-lang#1130, but this patch should allow record extension to be used on temporal projections on variables / record literals. Removal of unused headless testing (links-lang#1152) The headless testing has been unused for about a year, because it is unmaintained. Even though it is not used, it generates a ton of security warnings here on GitHub. I am not interested in dealing with those, therefore this patch removes the headless testing directory from the source tree.
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.
The
Lenstype traversal was unimplemented and filled in with anassert false. As a result, all RL code fails.I don't think there is any really sensible default traversal due to the complexity of the Lens types, so I have just filled it in with the identity. This doesn't stop someone implementing a traversal -- they'll just need to write one for
Lens.Type.ttype and plug it in as usual.