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

Allow record extension in presence of temporal projections #1129

Merged
merged 6 commits into from
Jul 1, 2022

Conversation

SimonJF
Copy link
Member

@SimonJF SimonJF commented Apr 1, 2022

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.

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.
@SimonJF
Copy link
Member Author

SimonJF commented Apr 1, 2022

Looking at it, this is a bit more complex than I'd thought (was testing on a restricted case -- the cases I was encountering all happened to have record literals, but this is not the case in general since xlate does not in itself normalise terms, merely translate them).

The issue is that Extend needs to have access to a record literal during translation, whereas it doesn't necessarily on an un-normalised term.

@SimonJF SimonJF closed this 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.
@SimonJF SimonJF reopened this Apr 1, 2022
@SimonJF
Copy link
Member Author

SimonJF commented Apr 1, 2022

I've reopened this with the view to partially sorting #1124. Extension may not work in the general case, but we can at least make it work for temporal accessors that operate on record literals.

@SimonJF
Copy link
Member Author

SimonJF commented Jul 1, 2022

Can this go in? I don't think it's too controversial.

@dhil dhil self-requested a review July 1, 2022 15:21
Copy link
Member

@dhil dhil left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM.

@dhil dhil merged commit 1745f2f into links-lang:master Jul 1, 2022
Orbion-J pushed a commit to Orbion-J/links that referenced this pull request 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 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
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Record extension in the context of temporal tables
2 participants