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.

Sign up for GitHub

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

Jump to bottom

take/put unsoundness #61

Open
zilinc opened this issue Jan 30, 2017 · 3 comments
Open

take/put unsoundness #61

zilinc opened this issue Jan 30, 2017 · 3 comments
Labels
bug cogent tc

Comments

@zilinc
Copy link

zilinc commented Jan 30, 2017 •
edited
Loading

Can take a linear field multiple times.
Can put a linear field multiple times.
zilinc pushed a commit that referenced this issue Jan 30, 2017
compiler: add test files for #61
c43767c 
[skip ci]
zilinc pushed a commit that referenced this issue Jan 30, 2017
compiler: add test files for #61
11bd405 
[skip ci]
zilinc pushed a commit that referenced this issue Jan 11, 2018
compiler: add test files for #61
477e0f1 
[skip ci]
zilinc pushed a commit that referenced this issue Jan 22, 2018
compiler: add test files for #61
caa07a8 
[skip ci]
@zilinc
Copy link
Author

zilinc commented Feb 5, 2018

also see 00bbf5a

@zilinc
Copy link
Author

zilinc commented Feb 5, 2018 •
edited
Loading

same for variant types -- can take an alternative more than once. (i.e. overlapping constructor incorrectly allowed)

zilinc pushed a commit that referenced this issue Feb 5, 2018
compiler/tc: wip - #61
ff38b42 
Plan is:
1. we need to generate constraints when we take/put, to guarantee
that in a single take/put expression, the field is not repetitive.
2. in the solver, we check for well-formedness in `whnf' function.

[skip ci]
@zilinc
Copy link
Author

zilinc commented Feb 6, 2018 •
edited
Loading

In the solver, when we whnf a type, we never check if this put/take operation is allowed or not. See here and here.
I think to fix this, we can either emit some constraints, saying a field/tag is taken from a type. For instance, in the solver, if we see multiple occurrences of the same field being taken, we turn that into a Shareable constraint. This requires changes to the constraint solver, and new types of constraints. Alternatively we could check them in Post, which requires us to infer kinds of types in order to determine if the type of a field is linear or not.
There are some similar validity checks, which are performed in the Post stage, e.g. taking a non-existing field, taking from a non-record type, etc. It's questionable that we check for errors in Post -- although this seems easier engineering-wise, it looks ad hoc and doesn't fit so well with the overall constraint-based approach. @liamoc What do you reckon? Can you justify it, say, in your thesis if we do it the current way?

zilinc pushed a commit that referenced this issue Mar 6, 2018
compiler: add test files for #61
cb22a04 
[skip ci]
zilinc pushed a commit that referenced this issue Mar 6, 2018
compiler/tc: wip - #61
a320270 
Plan is:
1. we need to generate constraints when we take/put, to guarantee
that in a single take/put expression, the field is not repetitive.
2. in the solver, we check for well-formedness in `whnf' function.

[skip ci]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug cogent tc
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@zilinc