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

Experimental support for linear types #192

Merged
merged 1 commit into from
Jul 24, 2015
Merged

Experimental support for linear types #192

merged 1 commit into from
Jul 24, 2015

Conversation

EliasC
Copy link
Contributor

@EliasC EliasC commented Jul 24, 2015

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 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?).
@EliasC
Copy link
Contributor Author

EliasC commented Jul 24, 2015

I'm going to merge this myself since it's not going into master. A proper review can be done when we're merging it into the master branch.

EliasC added a commit that referenced this pull request Jul 24, 2015
Experimental support for linear types
@EliasC EliasC merged commit f727ff5 into parapluu:features/linear Jul 24, 2015
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.

1 participant