-
Notifications
You must be signed in to change notification settings - Fork 43
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Record extension does not work for non-literals in query #1130
Comments
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.
Hmm. I'm not sure whether this is a bug per se, in the sense that record extension isn't included in the formalizations of how this is supposed to work, but it seems likely that it would work if we normalized the rest-of-record and added some commutation laws (e.g. if the subject of an "if" is true or false we can just reduce it, but otherwise seems like the extension could be pushed into both branches.) Relatedly @vcgalpin has asked for record field discarding (i.e. an operation _\l : (l:A|r) -> (r) for every field name l, that does what its polymorphic type says it must do if it terminates). It would be good to add this to the theory / implementation too. A short term (not requiring additional research) fix could be to make proper occurrences of record extension "wild", so that they are not (for now) allowed in queries. So at least we don't get mysterious run-time errors. |
* 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 #1124. * Allow extension to work with (shallow) temporal projections We don't have the full generality due to #1130, but this patch should allow record extension to be used on temporal projections on variables / record literals.
…g#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.
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.
While looking at #1124, I noticed that record extension only works for record literals in the query evaluator.
The issue is that there is no representation of record extension in the query IR; it gets translated away during the IR -> Query IR pass.
However, this is not safe in general since there's nothing guaranteeing that the subject of the extension is actually a record literal. Indeed, translation does not even normalise the argument, so there are a large class of terms that should work that don't. See, for example:
Even if we did try to compile away
Extend
on normalised terms, we still couldn't guarantee that this is a record; for example, if theif
statement referred to a field in the table.To fix, I think we will need an explicit representation of
Extend
, work out the necessary normalisation rules / normal forms, and the appropriate SQL implementation.The text was updated successfully, but these errors were encountered: