On 08/05/2013 12:35 AM, Walter Bright wrote:
> 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.
>

I have reported the unsoundness:

http://d.puremagic.com/issues/show_bug.cgi?id=10758

On 8/4/2013 4:03 PM, Timon Gehr wrote:
> On 08/05/2013 12:35 AM, Walter Bright wrote:
>> 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.
>>
>
> I have reported the unsoundness:
>
> http://d.puremagic.com/issues/show_bug.cgi?id=10758
>

Please add all 4, not just the last one.

On Sunday, 4 August 2013 at 22:26:19 UTC, Timon Gehr wrote:
> 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/

Thanks Timon, this looks like a great resource.

On Sunday, 4 August 2013 at 15:04:48 UTC, Timon Gehr wrote:

> - No naming or scoping:

OK, but I'm not sure naming and scoping buys you anything except for being more explicit, but explicity vs implicity is a tradeoff.
I kinda understand the argument about dependent purity, but the problem with purity arises mostly in generic code consuming arbitrary ranges, the problem with delegate purity looks minor.
As to the crash, it looks like it tries to mess with the delegate's signature, which it souldn't do: delegate's signature doesn't participate in const transitivity rules. The cost is probably one if at the right place.

> - Only works for parameters or stack based variables:

Not a failure to not do what is not proved to be possible and acceptable. Const system doesn't interoperate with templates well. You don't have a solution either, even with your universal notation, right?

> - Plain unsoundness of current type checking approach:

Closures were not covered in DIP2 (I agree, that was a major overlook). Closured variables should be treated as external to the closure and either be seen as const or require cast to const. Fix may be non-trivial, but possible.

I was thinking to call for lore about issues with inout and solve them, also for other people, who want to work on the type system to have an estimate of the problem's scale. Am I late?

On Sunday, 4 August 2013 at 16:18:48 UTC, bearophile wrote:
> I am starting to think that to design type system features sometimes you need formal mathematics, otherwise you build a Swiss cheese.

How would you account for yet undefined features like ARC?

On 08/05/2013 10:44 PM, Kagamin wrote:
> On Sunday, 4 August 2013 at 15:04:48 UTC, Timon Gehr wrote:
>
>> - No naming or scoping:
>
> OK, but I'm not sure naming and scoping buys you anything except for
> being more explicit, but explicity vs implicity is a tradeoff.

I thought I had demonstrated that it buys you more. It resolves the problem that scoping is ambiguous and that there can be only one 'inout' substitution per function application.

> I kinda understand the argument about dependent purity, but the problem
> with purity arises mostly in generic code consuming arbitrary ranges,
> the problem with delegate purity looks minor.

Why? It is the same kind of problem.

> As to the crash, it looks like it tries to mess with the delegate's
> signature, which it souldn't do: delegate's signature doesn't
> participate in const transitivity rules. The cost is probably one if at
> the right place.
>
>> - Only works for parameters or stack based variables:
>
> Not a failure to not do what is not proved to be possible and
> acceptable.

Those ideas are more than 40 years old and this is a minor adaptation.

> Const system doesn't interoperate with templates well.
> You don't have a solution either,

Of course. Just push the parameter to the instantiated struct type.

i.e.

struct S(T){
    T field;
}

S!(C(int)*) foo[TC C](C(int)* p){ return typeof(return)(p); }


Would behave like:

struct S[TC C]{ // (template instance)
    C(int)* field;
}

S![C] foo[TC C](C(int)* p){ return typeof(return)(p); }


> even with your universal notation, right?
>
>> - Plain unsoundness of current type checking approach:
>
> Closures were not covered in DIP2 (I agree, that was a major overlook).
> Closured variables should be treated as external to the closure and
> either be seen as const or require cast to const. Fix may be
> non-trivial, but possible.
> ...

The fix is to introduce proper scoping, but then it does not seem sensible to only allow one name for the type constructor parameter.

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

On Tuesday, 6 August 2013 at 02:11:54 UTC, Timon Gehr wrote:
> I thought I had demonstrated that it buys you more. It resolves the problem that scoping is ambiguous and that there can be only one 'inout' substitution per function application.

It may look ambiguous to someone who doesn't know, how the feature works, because it's implicit, which, again, is a tradeoff. Subjective ambiguity should be solvable with better docs, learning resources and tutorials.

> Why? It is the same kind of problem.

They differ in scale. Const overloads are an overwhelming problem in OO design, which is vaguely demonstrated in DIP2.

> Of course. Just push the parameter to the instantiated struct type.
>
> i.e.
>
> struct S(T){
>     T field;
> }
>
> S!(C(int)*) foo[TC C](C(int)* p){ return typeof(return)(p); }
>
>
> Would behave like:
>
> struct S[TC C]{ // (template instance)
>     C(int)* field;
> }
>
> S![C] foo[TC C](C(int)* p){ return typeof(return)(p); }

Ah, an opaque template parameter? It may have value in itself and not require a new syntax or restricted to type qualifiers.

> The fix is to introduce proper scoping, but then it does not seem sensible to only allow one name for the type constructor parameter.

inout already has proper scoping: data external to the function shouldn't be qualified as inout, it just should be checked.

On Tuesday, 6 August 2013 at 03:42:00 UTC, deadalnix wrote:
> The ambiguity lies in the fact that inout in the delegate may stand for foo's inout or delegate's inout.

inout applies to parameters and is transitive, but delegate's signature is not affected by const transitivity rules - it worked this way long before inout was implemented.

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

inout is for functions which return data derived from their parameters, your qux doesn't enforce this semantics: it can return anything which fits int*.

On Tuesday, 6 August 2013 at 15:13:18 UTC, Kagamin wrote:
> Ah, an opaque template parameter? It may have value in itself and not require a new syntax or restricted to type qualifiers.

Though it must be viral in order to work.