On Sunday, 4 August 2013 at 09:52:01 UTC, Kagamin wrote:
> On Sunday, 4 August 2013 at 02:41:18 UTC, Timon Gehr wrote:
>> D's inout is a somewhat failed attempt
>
> Why?

It only work for qualifiers. The same issue arise in much for various form where inout can't do anything.

What a bout a function which is pure depending on if a function passed as parameter is pure or not ? or return a function the same way ?

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

Timon Gehr:

> Off the top of my head:

Thank you.

Is it right to add 'inout' the list of D2 features that will be deprecated and later removed?

There are "simple" features, like a support for structurally typed tuples, that maybe can be designed well enough with the traditional method. But perhaps when we/you want to modify/add something in the D type system it's better to first find a person able to write down a formal proof of soundness of the idea, and only later decide if it's worth implementing. I am starting to think that to design type system features sometimes you need formal mathematics, otherwise you build a Swiss cheese.

Bye,
bearophile

On 8/4/2013 3:48 AM, Araq wrote:
>>
>> Consider the canonical example:
>>
>>     void* foo(void *p) { return p; }
>>
>> Do you write an overload for each kind of pointer?
>
> Doesn't D already have that problem with its immutable/const pointers?

Yes, and we've gone to considerable effort to deal with it, and there are still issues like using the same function for shared vs unshared pointers.

Introducing more pointer types makes things exponentially worse.

On 8/4/2013 7:04 AM, deadalnix wrote:
> What a bout a function which is pure depending on if a function passed as
> parameter is pure or not ? or return a function the same way ?

This is where attribute inference comes into play.

On 08/04/2013 08:35 PM, Walter Bright wrote:
> On 8/4/2013 7:04 AM, deadalnix wrote:
>> What a bout a function which is pure depending on if a function passed as
>> parameter is pure or not ? or return a function the same way ?
>
> This is where attribute inference comes into play.

(He is talking about runtime parameters.)

On 08/04/2013 06:18 PM, bearophile wrote:
> Timon Gehr:
>
>> Off the top of my head:
>
> Thank you.
>
> Is it right to add 'inout' the list of D2 features that will be
> deprecated and later removed?
> ...

Maybe, but this is not my decision, and if it is removed it should be replaced.

> There are "simple" features, like a support for structurally typed
> tuples, that maybe can be designed well enough with the traditional
> method. But perhaps when we/you want to modify/add something in the D
> type system it's better to first find a person able to write down a
> formal proof of soundness of the idea, and only later decide if it's
> worth implementing.

Formal proofs require a formalization of language semantics. It's not just a matter of finding someone to carry out the proof. (Anyone can learn online how to do this.)

> I am starting to think that to design type system
> features sometimes you need formal mathematics, otherwise you build a
> Swiss cheese.
> ...

This is not only true for type checkers, but for also for other kinds of programs. Yet most programming languages do not allow expressing a significant amount of checkable non-trivial correctness properties.

Timon Gehr:

> Formal proofs require a formalization of language semantics. It's not just a matter of finding someone to carry out the proof. (Anyone can learn online how to do this.)

I think you have too much faith in people intelligence (or just in my intelligence) :-)

Bye,
bearophile

On 08/04/2013 11:55 PM, bearophile wrote:
> Timon Gehr:
>
>> Formal proofs require a formalization of language semantics. It's not
>> just a matter of finding someone to carry out the proof. (Anyone can
>> learn online how to do this.)
>
> I think you have too much faith in people intelligence (or just in my
> intelligence) :-)
>
> Bye,
> bearophile

In case someone wants to try anyway, eg. the following course is quite enjoyable:

http://www.cis.upenn.edu/~bcpierce/sf/

On 8/4/2013 8:04 AM, Timon Gehr wrote:
> Off the top of my head:

If these are not in bugzilla, please add them.