Ironclad C++

[deadalnix]

On Sunday, 4 August 2013 at 15:04:48 UTC, Timon Gehr wrote:
> 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);
> }
>

The ambiguity lies in the fact that inout in the delegate may 
stand for foo's inout or delegate's inout.

However, in both cases, the sample code should pass.

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

As code accepting inout accept to not modify it, it should also 
pass. The exact semantic is still unclear, even if equivalent in 
the sample code above.

For instance, it is unclear what should happen in this case :
int d;
int* qux(int* p) { *p++; return p; }
bar(&d, &qux); // Pass for inout at bar's level, do not for inout 
at delegate level.

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

The last one should pass IMO due to function type conversion 
rules, whatever case is chosen for inout semantic in case of 
delegate/function. It is very unclear to me if the first one 
should pass.

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

Yes, one way or another, we'll need to be able to alias type 
qualifiers (or any similar mechanism).