www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Implementing typestate

reply Freddy <Hexagonalstar64 gmail.com> writes:
Would it be worth implementing some kind of typestate into the 
language?
By typestate I mean a modifiable enum.

For example:
---
enum FState
{
     none,
     read,
     write
}

struct File
{
     //maybe another keyword other than enum
     enum state = FState.none;

     void openRead(string name)
     {
         //evalutaed in a way similar to static if
         state = FState.read;
         //...
     }

     void openWrite(string name)
     {
         state = FState.write;
         //...
     }

     ubyte[] read(size_t) if (state == FState.read)
     {
         //...
     }

     void write(ubyte[]) if (state == FState.write)
     {
         //...
     }
}

unittest
{
     File f;
     static assert(f.state == FState.none);
     f.openRead("a.txt");
     static assert(f.state == FState.read);
     auto data = f.read(10);
}
---

We could use this "typestate" to implement:
  Rust style memory management in a library
  Safer Files (as shown)
  Possibly other ideas

Thoughts?
Sep 15 2015
next sibling parent reply BBasile <bb.temp gmx.com> writes:
On Tuesday, 15 September 2015 at 17:45:45 UTC, Freddy wrote:
 Would it be worth implementing some kind of typestate into the 
 language?
 By typestate I mean a modifiable enum.

 For example:
 ---
 enum FState
 {
     none,
     read,
     write
 }

 struct File
 {
     //maybe another keyword other than enum
     enum state = FState.none;

     void openRead(string name)
     {
         //evalutaed in a way similar to static if
         state = FState.read;
         //...
     }

     void openWrite(string name)
     {
         state = FState.write;
         //...
     }

     ubyte[] read(size_t) if (state == FState.read)
     {
         //...
     }

     void write(ubyte[]) if (state == FState.write)
     {
         //...
     }
 }

 unittest
 {
     File f;
     static assert(f.state == FState.none);
     f.openRead("a.txt");
     static assert(f.state == FState.read);
     auto data = f.read(10);
 }
 ---

 We could use this "typestate" to implement:
  Rust style memory management in a library
  Safer Files (as shown)
  Possibly other ideas

 Thoughts?
This won't work in D. Everything that's static is common to each instance. What's possible however is to use an immutable FState that's set in the ctor. --- struct File { immutable FState state, this(string fname, FState st){state = st} } --- Than you're sure that your file state can't be changed by error. Otherwise just hide the state to set it as a private variable...
Sep 15 2015
parent reply Freddy <Hexagonalstar64 gmail.com> writes:
On Tuesday, 15 September 2015 at 17:57:10 UTC, BBasile wrote:
 This won't work in D. Everything that's static is common to 
 each instance.
 What's possible however is to use an immutable FState that's 
 set in the ctor.

 ---
 struct File
 {
     immutable FState state,
     this(string fname, FState st){state = st}
 }
 ---

 Than you're sure that your file state can't be changed by error.
 Otherwise just hide the state to set it as a private variable...
No, I'm talking about adding a new feature to the language, modifable enums(typestate).
Sep 15 2015
parent reply BBasile <bb.temp gmx.com> writes:
On Tuesday, 15 September 2015 at 17:59:19 UTC, Freddy wrote:
 On Tuesday, 15 September 2015 at 17:57:10 UTC, BBasile wrote:
 This won't work in D. Everything that's static is common to 
 each instance.
 What's possible however is to use an immutable FState that's 
 set in the ctor.

 ---
 struct File
 {
     immutable FState state,
     this(string fname, FState st){state = st}
 }
 ---

 Than you're sure that your file state can't be changed by 
 error.
 Otherwise just hide the state to set it as a private 
 variable...
No, I'm talking about adding a new feature to the language, modifable enums(typestate).
Ok, sorry I didn't know this concept so far. So there would be a kind of 'compile-time instance' of File with a modifiable member ?
Sep 15 2015
parent reply Freddy <Hexagonalstar64 gmail.com> writes:
On Tuesday, 15 September 2015 at 18:10:06 UTC, BBasile wrote:
 Ok, sorry I didn't know this concept so far.
 So there would be a kind of 'compile-time instance' of File 
 with a modifiable member ?
A simplified version of this: https://en.wikipedia.org/wiki/Typestate_analysis Where types can have compile time state(enum) that change as they are used.
Sep 15 2015
parent reply BBasile <bb.temp gmx.com> writes:
On Tuesday, 15 September 2015 at 18:15:46 UTC, Freddy wrote:
 On Tuesday, 15 September 2015 at 18:10:06 UTC, BBasile wrote:
 Ok, sorry I didn't know this concept so far.
 So there would be a kind of 'compile-time instance' of File 
 with a modifiable member ?
A simplified version of this: https://en.wikipedia.org/wiki/Typestate_analysis Where types can have compile time state(enum) that change as they are used.
Ok, I see. So type states can be used in static analysis to find possible bugs if certain states-pattern are not found. In the file example if after FState.open, fState.close is never found then a compiler could emitt a warn about a possible leak or something...wow that's pretty edgy...
Sep 15 2015
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= writes:
On Tuesday, 15 September 2015 at 18:25:51 UTC, BBasile wrote:
 On Tuesday, 15 September 2015 at 18:15:46 UTC, Freddy wrote:
 On Tuesday, 15 September 2015 at 18:10:06 UTC, BBasile wrote:
 Ok, sorry I didn't know this concept so far.
 So there would be a kind of 'compile-time instance' of File 
 with a modifiable member ?
A simplified version of this: https://en.wikipedia.org/wiki/Typestate_analysis Where types can have compile time state(enum) that change as they are used.
Ok, I see. So type states can be used in static analysis to find possible bugs if certain states-pattern are not found. In the file example if after FState.open, fState.close is never found then a compiler could emitt a warn about a possible leak or something...wow that's pretty edgy...
It is the same type of concept. Typestate, effect system, linear typing, behavioural typing. It is no doubt the future for type systems, but also demanding. I've tried to raise awareness about it before, but no takers: http://forum.dlang.org/post/ovoarcbexpvrrceysnrs forum.dlang.org
Sep 15 2015
parent reply Meta <jared771 gmail.com> writes:
On Tuesday, 15 September 2015 at 18:30:34 UTC, Ola Fosheim 
Grøstad wrote:
 It is the same type of concept. Typestate, effect system, 
 linear typing, behavioural typing. It is no doubt the future 
 for type systems, but also demanding. I've tried to raise 
 awareness about it before, but no takers:

 http://forum.dlang.org/post/ovoarcbexpvrrceysnrs forum.dlang.org
If I remember correctly Rust *did* have a typestate system very early on but it was done away with in favour of the borrow checker.
Sep 15 2015
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= writes:
On Tuesday, 15 September 2015 at 20:01:16 UTC, Meta wrote:
 On Tuesday, 15 September 2015 at 18:30:34 UTC, Ola Fosheim 
 Grøstad wrote:
 It is the same type of concept. Typestate, effect system, 
 linear typing, behavioural typing. It is no doubt the future 
 for type systems, but also demanding. I've tried to raise 
 awareness about it before, but no takers:

 http://forum.dlang.org/post/ovoarcbexpvrrceysnrs forum.dlang.org
If I remember correctly Rust *did* have a typestate system very early on but it was done away with in favour of the borrow checker.
Yeah, I've seen the Rust creator write about how they started out with all whistles and bells with the intent of having a full blow effect system. Then realized that they had to make things simpler and focus on memory management because that was the most critical feature. Probably a wise strategy to go for simplicity and hit version 1.0 sooner. Having a simple core language is usually a good idea. I see now in the rust forums that people use the borrow checker for other things than memory, like tracking what thread you are in: https://users.rust-lang.org/t/my-gamedever-wishlist-for-rust/2859/7
Sep 15 2015
next sibling parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= writes:
On Tuesday, 15 September 2015 at 20:14:11 UTC, Ola Fosheim 
Grøstad wrote:
 Having a simple core language is usually a good idea. I see now 
 in the rust forums that people use the borrow checker for other 
 things than memory, like tracking what thread you are in:

 https://users.rust-lang.org/t/my-gamedever-wishlist-for-rust/2859/7
Not actually sure if that does depend on the borrow checker though... My knowledge of Rust is superficial... But nevertheless, it will be interesting to see how people use the rust type system for other things than memory.
Sep 15 2015
prev sibling parent reply =?UTF-8?Q?Tobias=20M=C3=BCller?= <troplin bluewin.ch> writes:
Ola Fosheim Grøstad <ola.fosheim.grostad+dlang gmail.com> wrote:
 On Tuesday, 15 September 2015 at 20:01:16 UTC, Meta wrote:
 [...]
 If I remember correctly Rust *did* have a typestate system very > early
 on but it was done away with in favour of the borrow > checker.
Yeah, I've seen the Rust creator write about how they started out with all whistles and bells with the intent of having a full blow effect system. Then realized that they had to make things simpler and focus on memory management because that was the most critical feature. Probably a wise strategy to go for simplicity and hit version 1.0 sooner.
I think they settled for a simpler library solution using a marker type (I think it was called Phantom type) as template parameter and then using local shadowing to emulate mutable type state. Multiple variables with same name but different (marker) type. There's a Blog post somewhere but I can't find it atm. Maybe that's also possible for D? Tobi
Sep 15 2015
parent reply =?UTF-8?Q?Tobias=20M=C3=BCller?= <troplin bluewin.ch> writes:
Tobias Müller <troplin bluewin.ch> wrote:
 I think they settled for a simpler library solution using a marker type (I
 think it was called Phantom type) as template parameter and then using
 local shadowing to emulate mutable type state. Multiple variables with same
 name but different (marker) type.
 There's a Blog post somewhere but I can't find it atm.
Ok found it: http://pcwalton.github.io/blog/2012/12/26/typestate-is-dead/ Tobi
Sep 15 2015
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= writes:
On Tuesday, 15 September 2015 at 20:34:43 UTC, Tobias Müller 
wrote:
 There's a Blog post somewhere but I can't find it atm.
Ok found it: http://pcwalton.github.io/blog/2012/12/26/typestate-is-dead/
But that is for runtime detection, not compile time?
Sep 15 2015
parent reply =?UTF-8?Q?Tobias=20M=C3=BCller?= <troplin bluewin.ch> writes:
Ola Fosheim Grøstad <ola.fosheim.grostad+dlang gmail.com> wrote:
 On Tuesday, 15 September 2015 at 20:34:43 UTC, Tobias Müller wrote:
 There's a Blog post somewhere but I can't find it atm.
Ok found it: > http://pcwalton.github.io/blog/2012/12/26/typestate-is-dead/
But that is for runtime detection, not compile time?
Not as far as I understand it. The marker is a type, not a value. And it's used as template param. But you need non-copyable move-only types for it to work. In D it would probably look like: File!Open file = open(...); File!Closed file = close(file); Tobi
Sep 15 2015
parent reply Ola Fosheim Grostad <ola.fosheim.grostad+dlang gmail.com> writes:
On Wednesday, 16 September 2015 at 05:51:50 UTC, Tobias Müller 
wrote:
 Ola Fosheim Grøstad <ola.fosheim.grostad+dlang gmail.com> wrote:
 On Tuesday, 15 September 2015 at 20:34:43 UTC, Tobias Müller 
 wrote:
 There's a Blog post somewhere but I can't find it atm.
Ok found it: > http://pcwalton.github.io/blog/2012/12/26/typestate-is-dead/
But that is for runtime detection, not compile time?
Not as far as I understand it. The marker is a type, not a value. And it's used as template param. But you need non-copyable move-only types for it to work.
Yes... But will it prevent you from doing two open() in a row at compiletime?
Sep 15 2015
next sibling parent Ola Fosheim Grostad <ola.fosheim.grostad+dlang gmail.com> writes:
On Wednesday, 16 September 2015 at 06:25:59 UTC, Ola Fosheim 
Grostad wrote:
 On Wednesday, 16 September 2015 at 05:51:50 UTC, Tobias Müller 
 wrote:
 Ola Fosheim Grøstad <ola.fosheim.grostad+dlang gmail.com> 
 wrote:
 But you need non-copyable move-only types for it to work.
Yes... But will it prevent you from doing two open() in a row at compiletime?
Nevermind, it needs linear typing, not only move semantics...
Sep 15 2015
prev sibling parent reply Idan Arye <GenericNPC gmail.com> writes:
On Wednesday, 16 September 2015 at 06:25:59 UTC, Ola Fosheim 
Grostad wrote:
 On Wednesday, 16 September 2015 at 05:51:50 UTC, Tobias Müller 
 wrote:
 Ola Fosheim Grøstad <ola.fosheim.grostad+dlang gmail.com> 
 wrote:
 On Tuesday, 15 September 2015 at 20:34:43 UTC, Tobias Müller 
 wrote:
 There's a Blog post somewhere but I can't find it atm.
Ok found it: > http://pcwalton.github.io/blog/2012/12/26/typestate-is-dead/
But that is for runtime detection, not compile time?
Not as far as I understand it. The marker is a type, not a value. And it's used as template param. But you need non-copyable move-only types for it to work.
Yes... But will it prevent you from doing two open() in a row at compiletime?
What's wrong with two `open()`s in a row? Each will return a new file handle.
Sep 16 2015
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= writes:
On Wednesday, 16 September 2015 at 10:31:58 UTC, Idan Arye wrote:
 What's wrong with two `open()`s in a row? Each will return a 
 new file handle.
Yes, but if you do it by mistake then you don't get the compiler to check that you call close() on both. I should have written "what if you forget close()". Will the compiler then complain at compile time? You can't make that happen with just move semantics, you need linear typing so that every resource created are consumed exactly once.
Sep 16 2015
parent reply Idan Arye <GenericNPC gmail.com> writes:
On Wednesday, 16 September 2015 at 14:34:05 UTC, Ola Fosheim 
Grøstad wrote:
 On Wednesday, 16 September 2015 at 10:31:58 UTC, Idan Arye 
 wrote:
 What's wrong with two `open()`s in a row? Each will return a 
 new file handle.
Yes, but if you do it by mistake then you don't get the compiler to check that you call close() on both. I should have written "what if you forget close()". Will the compiler then complain at compile time? You can't make that happen with just move semantics, you need linear typing so that every resource created are consumed exactly once.
Move semantics should be enough. We can declare the destructor private, and then any code outside the module that implicitly calls the d'tor when the variable goes out of scope will raise a compilation error. In order to "get rid" of the variable, you'll have to pass ownership to the `close` function, so your code won't try to implicitly call the d'tor.
Sep 16 2015
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= writes:
On Wednesday, 16 September 2015 at 15:34:40 UTC, Idan Arye wrote:
 Move semantics should be enough. We can declare the destructor 
 private, and then any code outside the module that implicitly 
 calls the d'tor when the variable goes out of scope will raise 
 a compilation error. In order to "get rid" of the variable, 
 you'll have to pass ownership to the `close` function, so your 
 code won't try to implicitly call the d'tor.
Sounds plausible, but does this work in C++ and D? I assume you mean that you "reinterpret_cast" to a different type in the close() function, which is cheating, but ok :).
Sep 16 2015
parent reply Idan Arye <GenericNPC gmail.com> writes:
On Wednesday, 16 September 2015 at 15:57:14 UTC, Ola Fosheim 
Grøstad wrote:
 On Wednesday, 16 September 2015 at 15:34:40 UTC, Idan Arye 
 wrote:
 Move semantics should be enough. We can declare the destructor 
 private, and then any code outside the module that implicitly 
 calls the d'tor when the variable goes out of scope will raise 
 a compilation error. In order to "get rid" of the variable, 
 you'll have to pass ownership to the `close` function, so your 
 code won't try to implicitly call the d'tor.
Sounds plausible, but does this work in C++ and D? I assume you mean that you "reinterpret_cast" to a different type in the close() function, which is cheating, but ok :).
No need for `reinterpret_cast`. The `close` function is declared in the same module as the `File` struct, so it has access to it's private d'tor.
Sep 16 2015
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= writes:
On Wednesday, 16 September 2015 at 16:24:49 UTC, Idan Arye wrote:
 No need for `reinterpret_cast`. The `close` function is 
 declared in the same module as the `File` struct, so it has 
 access to it's private d'tor.
True, so it might work for D. Interesting.
Sep 16 2015
prev sibling next sibling parent Freddy <Hexagonalstar64 gmail.com> writes:
On Tuesday, 15 September 2015 at 17:45:45 UTC, Freddy wrote:
 ...
I just thought of some corner cases and how to solve them. --- Disallow global variable with typestate (there might be a better solution down the line). The evaluated typestate of variables after going through branches (if,for,etc...) must be the same. Example --- void func(){ File f; if(someVar){ f.openWrite("a.txt"); } //error here one branch where f is none, another branch where f is open } ---
Sep 15 2015
prev sibling next sibling parent reply Freddy <Hexagonalstar64 gmail.com> writes:
On Tuesday, 15 September 2015 at 17:45:45 UTC, Freddy wrote:
  Rust style memory management in a library
Wait nevermind about that part, it's harder than I thought.
Sep 15 2015
next sibling parent Freddy <Hexagonalstar64 gmail.com> writes:
On Tuesday, 15 September 2015 at 21:44:25 UTC, Freddy wrote:
 On Tuesday, 15 September 2015 at 17:45:45 UTC, Freddy wrote:
  Rust style memory management in a library
Wait nevermind about that part, it's harder than I thought.
All hope might not be lost, something like this MIGHT work,but i'm am sure I am missing some kind of detail. --- //doesn't actually compile struct MutBorrow(T, bool usable_ = true) { private T** ptr; enum usable = usable_; static if (usable) { disable this(); ref T use() { return **ptr; } } //... } struct Unique(T) { private T* ptr; alias user = null; ~this() { static assert(user is null); free(ptr); } auto giveMut(alias local)() { static assert(is(user : null))); user = local; local.usable = true; local.ptr = &ptr; } auto takeMut(alias local)() { static assert(local == user); //is there a proper way to compare alias? user = null; local.usable = false; } static if ( /+user not null+/ ) { ref T use() { return *ptr; } } } ---
Sep 15 2015
prev sibling parent reply Marc =?UTF-8?B?U2Now7x0eg==?= <schuetzm gmx.net> writes:
On Tuesday, 15 September 2015 at 21:44:25 UTC, Freddy wrote:
 On Tuesday, 15 September 2015 at 17:45:45 UTC, Freddy wrote:
  Rust style memory management in a library
Wait nevermind about that part, it's harder than I thought.
Yeah, I thought about type-states as a way of implementing borrowing, too. I think the biggest difficulty is that the state of one object (the owner) can be affected by what happens in other objects (i.e., it becomes mutable again when those are destroyed).
Sep 16 2015
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= writes:
On Wednesday, 16 September 2015 at 17:03:14 UTC, Marc Schütz 
wrote:
 On Tuesday, 15 September 2015 at 21:44:25 UTC, Freddy wrote:
 On Tuesday, 15 September 2015 at 17:45:45 UTC, Freddy wrote:
  Rust style memory management in a library
Wait nevermind about that part, it's harder than I thought.
Yeah, I thought about type-states as a way of implementing borrowing, too. I think the biggest difficulty is that the state of one object (the owner) can be affected by what happens in other objects (i.e., it becomes mutable again when those are destroyed).
If the borrowed reference itself follows move semantics, can't you just require it to be swallowed by it's origin as the "close" operation? pseudocode: File<Open> f = open(); (File<OpenLending> f, FileRef<Ready> r) = f.borrow(); dostuff(r); (File<Open> f, FileRef<Void> r) = f.unborrow(r); File<Closed> f = f.close()
Sep 16 2015
next sibling parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= writes:
On Wednesday, 16 September 2015 at 17:15:55 UTC, Ola Fosheim 
Grøstad wrote:
 dostuff(r);

 (File<Open> f, FileRef<Void> r) = f.unborrow(r);
Of course, files are tricky since they can change their state themselves (like IO error). Doing that statically would require some kind of branching mechanism with a try-catch that jumps to a different location where the file type changes to "File<Error>"... Sounds non-trivial to bolt onto an existing language.
Sep 16 2015
prev sibling parent reply Marc =?UTF-8?B?U2Now7x0eg==?= <schuetzm gmx.net> writes:
On Wednesday, 16 September 2015 at 17:15:55 UTC, Ola Fosheim 
Grøstad wrote:
 On Wednesday, 16 September 2015 at 17:03:14 UTC, Marc Schütz 
 wrote:
 On Tuesday, 15 September 2015 at 21:44:25 UTC, Freddy wrote:
 On Tuesday, 15 September 2015 at 17:45:45 UTC, Freddy wrote:
  Rust style memory management in a library
Wait nevermind about that part, it's harder than I thought.
Yeah, I thought about type-states as a way of implementing borrowing, too. I think the biggest difficulty is that the state of one object (the owner) can be affected by what happens in other objects (i.e., it becomes mutable again when those are destroyed).
If the borrowed reference itself follows move semantics, can't you just require it to be swallowed by it's origin as the "close" operation? pseudocode: File<Open> f = open(); (File<OpenLending> f, FileRef<Ready> r) = f.borrow(); dostuff(r); (File<Open> f, FileRef<Void> r) = f.unborrow(r); File<Closed> f = f.close()
But the `unborrow` is explicit. What I'd want is to use the implicit destructor call: struct S { static struct Ref { private typestate alias owner; private S* p; disable this(); this() typestate(alias owner) { this.owner := owner; // re-alias operator this.owner.refcount++; } body { this.p = &owner; } this(this) { this.owner.refcount++; } ~this() { this.owner.refcount--; } } typestate size_t refcount = 0; S.Ref opUnary(string op : "*")() { // overload address operator (not yet supported) return S.Ref( typestate this); } ~this() static if(refcount == 0) { } } void foo(scope S.Ref p); void bar(-> S.Ref p); // move void baz(S.Ref p); S a; // => S<0> { auto p = &a; // => S<1> foo(p); // pass-by-scope doesn't copy or destroy // => S<1> p.~this(); // (implicit) => S<0> } { auto p = &a; // => S<1> bar(p); // pass-by-move, no copy or destruction // => S<1> p.~this(); // (implicit) => S<0> } { auto p = &a; // => S<1> baz(p); // compiler sees only the copy, // but no destructor => S<2> p.~this(); // (implicit) => S<1> } a.~this(); // ERROR: a.refcount != 0 The first two cases can be analyzed at the call site. But the third one is problematic, because inside `baz()`, the compiler doesn't know where the alias actually points to, because it could be in an entirely different compilation unit. I guess this can be solved by disallowing all operations modifying or depending on an alias type-state. (Other complicated things, like preserving type-state through references or array indices, probably shouldn't even be attempted.)
Sep 16 2015
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= writes:
On Wednesday, 16 September 2015 at 18:01:29 UTC, Marc Schütz 
wrote:
             typestate(alias owner) {
                 this.owner := owner; // re-alias operator
                 this.owner.refcount++;
             }
I don't think this is possible to establish in the general case. Wouldn't this require a full theorem prover? I think the only way for that to work is to fully unroll all loops and hope that a theorem prover can deal with it. Either that or painstakingly construct a proof manually (Hoare logic). Like, how can you statically determine if borrowed references stuffed into a queue are all released? To do that you must prove when the queue is empty for borrowed references from a specific object, but it could be interleaved with references to other objects.
Sep 16 2015
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= writes:
On Wednesday, 16 September 2015 at 18:41:33 UTC, Ola Fosheim 
Grøstad wrote:
 I don't think this is possible to establish in the general 
 case. Wouldn't this require a full theorem prover? I think the 
 only way for that to work is to fully unroll all loops and hope 
 that a theorem prover can deal with it.
For example: Object<ready> obj = create(); for ... { (Object<lend#> obj, Ref<Object,lend#> r) = obj.borrow(); queue.push(r); dostuff(queue); } On the other hand if you have this: for i=0..2 { (Object<lend#> obj, Ref<Object,lend#> r[i]) = obj.borrow(); dostuff(r); } then you can unwind it as (hopefully): (Object<lend1234> obj, Ref<Object,lend1234> r[0]) = obj.borrow(); (Object<lend4324> obj, Ref<Object,lend4324> r[1]) = obj.borrow(); (Object<lend5133> obj, Ref<Object,lend5133> r[2]) = obj.borrow(); x += somepurefunction(r[0]); x += somepurefunction(r[1]); x += somepurefunction(r[2]); r[0].~this(); // r[0] proven unmodified, type is Ref<Object,lend1234> r[1].~this(); // r[1] proven to be Ref<Object,lend4324> r[2].~this(); // r[2] proven to be Ref<Object,lend5133> r.~this(); If the lend IDs always are unique then you sometimes can prove that all constructors have a matching destructor... Or something like that... ?
Sep 16 2015
prev sibling parent =?UTF-8?B?w7tyYsO7Y2s=?= <v nowhere.ke> writes:
On Tuesday, 15 September 2015 at 17:45:45 UTC, Freddy wrote:
 Would it be worth implementing some kind of typestate into the 
 language?
 By typestate I mean a modifiable enum.

 [...]
Article about this in C# and F#: http://enterprisecraftsmanship.com/2015/09/28/c-and-f-approaches-to-illegal-states/
Sep 29 2015