Introduce Lifetimes #642

Merged
merged 2 commits into from Apr 26, 2016

Projects

None yet

2 participants

@SebastianS90
Contributor

This pull request introduces a concept of lifetimes into Whiley.

A lifetime describes a region in the source code.
Possible regions are method bodies and named blocks.
Each lifetime has a name. The lifetime for method bodies is named this.
The lifetime of named blocks have the block’s name.
Furthermore, the special lifetime * describes the region covering the whole program.

Each reference type is annotated with a lifetime.
It states when the memory pointed to by that reference should be alive, i.e. not yet freed.

Affected parts of the compiler are:

  • lexer and parser
    • new keyword this
    • backwards-compatible syntax extension for references, new expressions, method declarations, method invocation, and lambda expressions
  • type system
    • reference types now carry a lifetime
    • method types now carry lifetime parameters and context lifetimes
  • lambda expressions
    • introduce lifetime parameters as for any other normal method
    • introduce a concept of context lifetimes
  • flow typing
    • keep track of how lifetimes relate to each other
    • check that dereferenced lifetimes in lambda expressions are declared as context lifetimes
  • method invocation
    • infer suitable lifetime arguments
    • substitute lifetime parameters in parameter types with inferred or explicitly specified lifetime arguments before checking whether the arguments are subtypes of parameters
    • apply the substitution also to the method's return type
  • subtyping / type intersection
    • for references: subtype's lifetime must outlive the supertype's lifetime
    • for methods:
      • apply a proper substitution of lifetime parameters
      • compare context lifetimes
@SebastianS90
Contributor

@DavePearce you can have a look through everything if time permits. I've just posted the pull request that you have everything in your repository.

You could merge it as a new feature branch in Whiley/WhileyCompiler or directly into develop, whatever you prefer.

Feedback is appreciated 😄

And sorry for the huge commit, I squashed everything before rebasing. There were so many conflicts with 05df043 such that squashing made conflict resolution and refactoring much easier for me.

@DavePearce
Member

Yeah, it's big. I pulled it into a separate feature branch for now ...
and will have a play around.

D

On 26/04/16 15:04, Sebastian Schweizer wrote:

@DavePearce https://github.com/DavePearce you can have a look through
everything if time permits. I've just posted the pull request that you
have everything in your repository.

You could merge it as a new feature branch in Whiley/WhileyCompiler or
directly into develop, whatever you prefer.

Feedback is appreciated 😄

And sorry for the huge commit, I squashed everything before rebasing.
There were so many conflicts with 05df043
05df043
such that squashing made conflict resolution and refactoring much easier
for me.


You are receiving this because you were mentioned.
Reply to this email directly or view it on GitHub
#642 (comment)

Senior Lecturer in Computer Science,
School of Engineering and Computer Science
Victoria University of Wellington,
PO Box 600,
Wellington,
New Zealand.

Office: Cotton 231
Telephone: +64 (0)4 463 5833
URL: http://ecs.victoria.ac.nz/~djp

@DavePearce
Member
DavePearce commented Apr 26, 2016 edited

Found an interesting test case:

method f() -> &int:
    &this:int p = new 1
    return p

This seems to compile which I wasn't expecting!

I'd guess it's got something to do with flow typing, and maybe we need to fix it separately.

@SebastianS90
Contributor

It's due to flow typing. You initialize p with *:new 1 (* is implicit if no lifetime is specified), therefore the flow type checker knows that type of p is actually &*:int.

@DavePearce
Member
DavePearce commented Apr 26, 2016 edited

Here's another interesting question:

type func is method(int)->int
method  f(&l:int p) -> method[l](int)->int:
    return &[l](int x -> x + *p)

So, at the moment, there's no way to move methodl->int into a named type? I guess we'll have to figure out how to fix that at some point ...

@DavePearce
Member

Overall, it looks pretty good!! I wonder how many merge-conflicts I'll have with my other feature branch ...

@SebastianS90
Contributor
method f(bool b) -> &int:
    &this:int p
    if b:
        p = this:new 1
    else:
        p = new 3
    return p

That one does not compile, as expected.

This one does compile, too:

method f():
    any x = true
    bool y = x
@DavePearce
Member

Hey,

Yeah, I figured it was something like that. In fact, I am going to
remove this feature of flow typing later down the track ... so that will
help no doubt.

D

On 26/04/16 16:47, Sebastian Schweizer wrote:

It's due to flow typing. You initialize |p| with |:new 1| (|| is
implicit if no lifetime is specified), therefore the flow type checker
knows that type of |p| is actually |&*:int|.


You are receiving this because you were mentioned.
Reply to this email directly or view it on GitHub
#642 (comment)

Senior Lecturer in Computer Science,
School of Engineering and Computer Science
Victoria University of Wellington,
PO Box 600,
Wellington,
New Zealand.

Office: Cotton 231
Telephone: +64 (0)4 463 5833
URL: http://ecs.victoria.ac.nz/~djp

@SebastianS90
Contributor

Regarding named types with context lifetimes: Keep in mind that it's actually the way how safety is ensured. You cannot have the method somewhere without writing its type. And you cannot write the type without having those lifetimes still in scope.

OK, you can always put the method into an any typed variable, but then you cannot call it anymore.
You'll read more about that in my thesis.

@DavePearce
Member

You'll read more about that in my thesis.

Looking forward to it!!

Actually I've got feedback on the rest I read over the weekend...

Senior Lecturer in Computer Science,
School of Engineering and Computer Science,
Victoria University of Wellington,
PO Box 600,
Wellington,
New Zealand.

Office: Cotton 231
Phone: +64 (0)4 4635833
URL: http://ecs.victoria.ac.nz/~djp

On 26/04/2016, at 4:58 pm, Sebastian Schweizer notifications@github.com wrote:

Regarding named types with context lifetimes: Keep in mind that it's actually the way how safety is ensured. You cannot have the method somewhere without writing its type. And you cannot write the type without having those lifetimes still in scope.

OK, you can always put the method into an any typed variable, but then you cannot call it anymore.
You'll read more about that in my thesis.


You are receiving this because you were mentioned.
Reply to this email directly or view it on GitHub

@DavePearce DavePearce merged commit ccbf8ac into Whiley:develop Apr 26, 2016

1 check passed

continuous-integration/travis-ci/pr The Travis CI build passed
Details
@DavePearce
Member

Great ... my feature branch rebased without any conflicts!! Obviously, you did all the heavy lifting already rebasing against my last merge into develop :)

@SebastianS90 SebastianS90 deleted the unknown repository branch Apr 26, 2016
@SebastianS90
Contributor

Thanks for merging it so quickly.
Yeah I took a lot of care to not introduce unnecessary whitespace or formatting changes that would provoke further conflicts. I'm glad that it doesn't disturb your own branches.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment