Re: Implementing typestate

[ûrbûck via Digitalmars-d]

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/

Re: Implementing typestate

[Ola Fosheim Grostad via Digitalmars-d]

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  
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...

Re: Implementing typestate

[Ola Fosheim Grostad via Digitalmars-d]

On Wednesday, 16 September 2015 at 05:51:50 UTC, Tobias Müller 
wrote:

Ola Fosheim Grøstad  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?

Re: Implementing typestate

[Idan Arye via Digitalmars-d]

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  
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.

Re: Implementing typestate

[Ola Fosheim Grøstad via Digitalmars-d]

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.

Re: Implementing typestate

[Idan Arye via Digitalmars-d]

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.

Re: Implementing typestate

[Marc Schütz via Digitalmars-d]

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).

Re: Implementing typestate

[Ola Fosheim Grøstad via Digitalmars-d]

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 :).

Re: Implementing typestate

[Ola Fosheim Grøstad via Digitalmars-d]

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.

Re: Implementing typestate

[Idan Arye via Digitalmars-d]

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.

Re: Implementing typestate

[Ola Fosheim Grøstad via Digitalmars-d]

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.

Re: Implementing typestate

[Ola Fosheim Grøstad via Digitalmars-d]

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 obj = create();

for ... {
  (Object obj, Ref r) = obj.borrow();
  queue.push(r);
  dostuff(queue);
}


On the other hand if you have this:

  for i=0..2 {
(Object obj, Ref r[i]) = obj.borrow();
dostuff(r);
  }

then you can unwind it as (hopefully):

  (Object obj, Ref r[0]) = 
obj.borrow();
  (Object obj, Ref r[1]) = 
obj.borrow();
  (Object obj, Ref 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

  r[1].~this();  // r[1] proven to be Ref
  r[2].~this(); // r[2] proven to be Ref
  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...


?

Re: Implementing typestate

[Marc Schütz via Digitalmars-d]

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 f = open();
(File f, FileRef r) = f.borrow();

dostuff(r);

(File f, FileRef r) = f.unborrow(r);

File 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 = 
}
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 =   // => S<1>
foo(p);   // pass-by-scope doesn't copy or destroy
  // => S<1>
p.~this();// (implicit) => S<0>
}
{
auto p =   // => S<1>
bar(p);   // pass-by-move, no copy or destruction
  // => S<1>
p.~this();// (implicit) => S<0>
}
{
auto p =   // => 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.)

Re: Implementing typestate

[Ola Fosheim Grøstad via Digitalmars-d]

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 f = open();
(File f, FileRef r) = f.borrow();

dostuff(r);

(File f, FileRef r) = f.unborrow(r);

File f = f.close()

Re: Implementing typestate

[Ola Fosheim Grøstad via Digitalmars-d]

On Wednesday, 16 September 2015 at 17:15:55 UTC, Ola Fosheim 
Grøstad wrote:

dostuff(r);

(File f, FileRef 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"...


Sounds non-trivial to bolt onto an existing language.

Re: Implementing typestate

[Freddy via Digitalmars-d]

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 = 
}

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;
}
}
}
---

Re: Implementing typestate

[Tobias Müller via Digitalmars-d]

Ola Fosheim Grøstad  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

Re: Implementing typestate

[Freddy via Digitalmars-d]

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.

Re: Implementing typestate

[Freddy via Digitalmars-d]

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

}
---

Re: Implementing typestate

[BBasile via Digitalmars-d]

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...

Re: Implementing typestate

[Ola Fosheim Grøstad via Digitalmars-d]

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/ovoarcbexpvrrceys...@forum.dlang.org

Re: Implementing typestate

[Freddy via Digitalmars-d]

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).

Re: Implementing typestate

[BBasile via Digitalmars-d]

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...

Re: Implementing typestate

[BBasile via Digitalmars-d]

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 ?

Re: Implementing typestate

[Freddy via Digitalmars-d]

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.

Implementing typestate

[Freddy via Digitalmars-d]

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?

Re: Implementing typestate

[Ola Fosheim Grøstad via Digitalmars-d]

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.

Re: Implementing typestate

[Ola Fosheim Grøstad via Digitalmars-d]

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/ovoarcbexpvrrceys...@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

Re: Implementing typestate

[Tobias Müller via Digitalmars-d]

Tobias Müller  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

Re: Implementing typestate

[Meta via Digitalmars-d]

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/ovoarcbexpvrrceys...@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.

Re: Implementing typestate

[Ola Fosheim Grøstad via Digitalmars-d]

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?

Re: Implementing typestate

[Tobias Müller via Digitalmars-d]

Ola Fosheim Grøstad  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