Ironclad C++

[Timon Gehr]

On 08/04/2013 11:51 AM, Kagamin wrote:
> On Sunday, 4 August 2013 at 02:41:18 UTC, Timon Gehr wrote:
>> D's inout is a somewhat failed attempt
>
> Why?

Off the top of my head:

- No naming or scoping:

// is this ok?
inout(int)* foo(inout(int)* a, inout(int)* delegate(inout(int)*) dg){
     return dg(a);
}

// is this ok?
int b;
const(int) c;
int bar(inout(int)* a, inout(int)* delegate(inout(int)*) dg){
     return *dg(a)+*dg(&b)+*dg(&c);
}

void main(){
     immutable int a;
     // which of those is valid? take your pick.
     assert(foo(&a,(typeof(a)* x)=>x) is a);
     assert(!bar(&a,(inout(int)* x)=>x));
}

(Apparently, currently both crash the compiler in mtype.c:1894.)

Assuming some kind of polymorphic type system allowing at least named 
type constructor parameters, we can express both:

// (details will vary here, eg. if the language is fully dependently 
typed, this concept can likely be expressed within it.)
alias const_immutable_or_mutable TC;

C(int)* foo[TC C](C(int)* a, C(int)* delegate(C(int)*) dg){
     return dg(a);
}

int b;
const(int) c;
int bar[TC A](A(int)* a, B(int)* delegate[TC B](B(int)*) dg){
     return *dg(a)+*dg(&b)+*dg(&c);
}

void main(){
     immutable int a;
     // everything is fine now:
     assert(foo(&a,x=>x) is a);
     assert(!bar(&a,x=>x));
}

(Here [ ] parameters introduce universal quantification: There is only 
one foo function, that works for every such type constructor argument, 
but you cannot find out what that argument was from within the function 
in order to change its behaviour. This is similar to inout except that 
it allows naming and scoping.)



- Only works for parameters or stack based variables:

Tuple!(inout(int)*, inout(int)*) foo(inout(int)* x){
     return tuple(x,x);
}

/usr/include/dmd/phobos/std/typecons.d(363): Error: variable 
std.typecons.Tuple!(inout(int)*,inout(int)*).Tuple._field_field_0 only 
parameters or stack based variables can be inout



- Plain unsoundness of current type checking approach:

The following compiles and runs without errors with DMD:

int* foo(inout(int)* x)@safe{
     inout(int)* screwUp(inout(int)*){ return x; }
     return screwUp((int*).init);
}

void main(){
     immutable x = 123;
     static assert(is(typeof(*&x)==immutable));
     assert(*&x==123);
     immutable(int)* y = &x;
     *foo(y)=456;
     assert(*&x==456);
     assert(x!=*&x); // (!)
}