Tracking control-flow linearity for effect handlers #1173
Conversation
1. handlers now count the usage of variables correctly 2. linear variables bound outside are not allowed in deep handlers 3. handler clauses deal with the usage of linear parameters correctly
…in the usage counting. Now it passes all tests!
1. linlet & unlet (no parser yet) 2. lindo & lincase by op names 3. swap the meaning of Any and Unl for effect row types
1. parser for unlet & linlet 2. correctly deal with cont_lin NOTE: a lot of cases are not considered! Only consider the body of programs & only consider creating new cont_lin in function abstraction and handle.
linearity: 1. more comments & documents 2. correctly deal with type_bindings 3. more test examples
1. add ldo syntax for linear operation invocation 2. non-linear operation invocation is implicitly followed by unlet 3. fix the type checking of linlet and unlet
| @@ -87,7 +87,8 @@ object (o : 'self_type) | |||
| let ty = | |||
| Types.fresh_type_variable (CommonTypes.lin_any, CommonTypes.res_any) in | |||
| let with_pos x = SourceCode.WithPos.make ~pos x in | |||
| let doOp = DoOperation (with_pos (Operation failure_op_name), [], Some (Types.empty_type)) in | |||
| (* FIXME: WT: I don't know whether should it be lindo or not *) | |||
There was a problem hiding this comment.
Though, I see that you have changed the signature of SessionFail below... I would be inclined not to change any of the session exceptions stuff.
There was a problem hiding this comment.
I have to change the SessionFail operation to be linear to make the functions in prelude.links well-typed. Otherwise we would get a type error because we use the unlimited operation SessionFail with linear channels. I also need to change some signatures of functions in lib.ml, because by default e::Row is e::Row(Unl,Any), which can only be unified with linear operations.
This is also a challenge for hiding this feature behind a new flag; it is not entirely compatible with the current Links syntax.
There was a problem hiding this comment.
I see... The settings logic does allow you specify transitive dependencies, so if session exceptions are toggled, then you can forcibly toggle linear continuations too.
There was a problem hiding this comment.
Actually it is fine to not toggle control_flow_linearity, but we still need to make sure that the existing library code is compatible with it. FOr example, using unlimited row variable e::Row(Any, Any) by default and use the linear operation signature =@ for SessionFail.
|
You'll also have to address the CI failures. |
|
Another thing is that you should hide this feature behind a new flag, e.g. |
Co-authored-by: Daniel Hillerström <[email protected]>
…ich eventually restores the compatibility with polymorphic operations
thwfhk
changed the title
|
@thwfhk there are a couple of failures now. I will merge this PR once the regressions have been fixed. |
Ah yes. That's because I forgot to add the files of some new tests. They should be fixed now. |
|
I'll merge after the CI has run successfully to completion. |
|
So... does this close #544? |
No as per the meeting yesterday. We keep the issue open for a potentially fun gimmick. We will close it during POPL. |
This PR will track the control-flow linearity for effect handlers, which will resolve issue #544.
It is very incomplete and full of hacks. More explanation to be added. Currently I just want to create a PR to be able to sync with the main branch.