Skip to content
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

Open
SimonJF opened this issue Apr 1, 2022 · 1 comment
Open

Record extension does not work for non-literals in query #1130

SimonJF opened this issue Apr 1, 2022 · 1 comment

Comments

@SimonJF
Copy link
Member

SimonJF commented Apr 1, 2022

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:

var db = database "links";
var test_table = table "test_table" with (
                   id: Int,
                   integer: Int)
                 where id readonly from db;
query { for (x <-- test_table)  [( a=x.id | (if (true) { ( b=x.integer | x ) } else { ( b=x.integer | x ) }))]}

***: Error: Links_core.QueryLang.DbEvaluationError("Error adding fields: non-record") 

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 the if 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.

SimonJF added a commit to SimonJF/links that referenced this issue Apr 1, 2022
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.
@jamescheney
Copy link
Contributor

jamescheney commented Apr 6, 2022

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.

dhil pushed a commit that referenced this issue Jul 1, 2022
* 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.
Orbion-J pushed a commit to Orbion-J/links that referenced this issue Jul 8, 2022
…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.
Orbion-J added a commit to Orbion-J/links that referenced this issue 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
Projects
None yet
Development

No branches or pull requests

2 participants