Features/linear #207
Merged
Features/linear #207
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This commit adds the possibility to mark a class (passive or active) as
`linear`. This means that all references to an object of that type must
be treated linearly, i.e. cannot be copied. Reference transfer is done
using the `consume` keyword. Here is an example program that shows most
of the current functionality:
```
linear passive class Foo
f : Foo
def foo() : void
print "Foo"
class Main
def main() : void
let x = new Foo
y = new Foo
arr = [consume x, consume y]
in{
x = consume arr[0];
x.f = consume arr[1];
y = consume x.f;
y.foo(); -- No consume needed for method calls
}
```
The checking that linearity is preserved is done using an additional
pass, implemented in the file `src/typechecker/Capturechecker.hs`. This
keeps the changes made to `Typechecker.hs` to a minimum, which is nice.
Basically, the capturechecker figures out where references are captured
and when a linear reference is safe to capture.
The linear references **should** be interoperable with all the features
currently in Encore, but testing is very welcome! I will keep this in a
feature branch (and try to keep it rebased on `master`) until the
exclusive capabilities find their way into the type system.
It should be noted that consumes are currently not atomic (the value is
read and nullified sequentially), but this shouldn't matter in a
race-free program. Linear streams are possible but not very useful,
since both `get` and `getNext` require you to consume the stream. For
any useful patterns we would need a way to `get` and move the stream
forward in one go (maybe `consume s` should be the way to do this?).
This commit moves the linearity property from classes to traits. An
included trait must have a mode, either given at inclusion time, or
given in the trait header (this works as a default). There are currently
two modes; `linear` whose references must be treated linearly, and
`unsafe` which works just like a regular type (no restrictions on
aliasing). A value of class type may be cast into a trait type (like in
`master`) or a (composite) capability type. All modes must match
exactly. Here is a small example program to show what is currently
possible:
```
-- Foo defaults to unsafe
unsafe trait Foo<t>
require f : t
def foo() : void
print "Foo!"
-- Inclusion of Bar requires specifying a mode
trait Bar
-- C can be aliased freely
passive class C<t> : Foo<t> + unsafe Bar
f : t
-- D must be treated linearly unless upcast to Foo<int>
passive class D : Foo<int> + linear Bar
f : int
class Main
def main() : void
let x = new D
y = consume x : linear Bar + unsafe Foo<int>
z = consume y : Foo<int>
w = z
in
w.foo()
```
This commit adds support for declaring parameters as
stackbound (`S(Foo)`). A linear reference can be passed as a stack bound
parameter without consuming, as the linear alias is buried for the
duration of the call (borrowing requires a synchronous call). A
stackbound may not be aliased (except through borrowing), and cannot be
used in parallel (so far this means that it may not be passed to an
active object). The following program exemplifies most uses of
borrowing:
```
def borrow(x : S(Token)) : void{
let thief = new Thief<Token>
-- y = consume x -- Stackbounds cannot be bound to new variables
in{
-- thief.steal(x); -- Stackbounds cannot be passed to active objects
x.foo(); -- You can call methods on stackbound objects
}
}
trait Foo
def foo() : void
print "Foo!"
passive class Token : linear Foo
class Thief<t>
def steal(x : S(t)) : void
()
class Main
-- f : S(Foo<int>) -- Fields cannot be stackbound
def borrow(x : S(Token)) : void
borrow(x) -- Stackbounds can be passed to other borrowing functions/methods
def main() : void
let x = new Token
thief = new Thief<Token>
in{
-- thief.steal(x); -- Linear values cannot be borrowed by active objects
this.borrow(x); -- Synchronous method calls can borrow linear values
}
```
Borrowing is so far very conservative with respect to what kind of
aliasing is allowed. Programming with it should show where additional
programming conveniences is needed.
|
Merging this on my own since it's not going into master. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The current work in progress on linear types. Parts of the type system is starting to resemble Kappa, but there are still too many things missing to call it
features/capabilities. More info is available in each individual commit.