On 5/16/2014 1:54 AM, Araq wrote:
>>
>> Yes, the VRP has been a nice win for D. No other language does it.
>
> I don't know why you keep saying things like that, you don't know all the
> languages out there. Nimrod does it too fwiw...

I having trouble finding it in the spec:

    http://nimrod-lang.org/manual.html

Can you please point me to it?

Walter Bright:

> Yes, the VRP has been a nice win for D.

There are ways to improve it in very useful ways, that increase static safety and cut down the number of useless casts required. Some currently refused examples:

---------------

int[100] array;
void main() {
    foreach (immutable idx, const x; array)
        ubyte y = idx;
}

---------------

void foo(immutable uint x)
in {
    assert(x <= ubyte.max);
} body {
    ubyte y = x;
}
void main() {}


https://issues.dlang.org/show_bug.cgi?id=10751



More on contracts:

uint foo()
in {
} out(result) {
    assert(result < 100);
} body {
    return 20;
}
void bar(immutable ubyte x) {}
void main() {
    bar(foo());
}

---------------

D immutability is under-utilized, it avoids the need for flow analysis:


void main(in string[] args) {
    immutable ushort x = args.length % 5;
    immutable ubyte y = x;
}



uint x;
void main() {
    immutable uint y = x;
    if (y <= ubyte.max) {
        ubyte z = y;
    }
}



uint x;
void main() {
    immutable uint y = x;
    assert(y <= ubyte.max);
    ubyte z = y;
}


https://issues.dlang.org/show_bug.cgi?id=10594

---------------

More:
https://issues.dlang.org/show_bug.cgi?id=10615
https://issues.dlang.org/show_bug.cgi?id=12753

Bye,
bearophile

On 05/16/2014 01:00 AM, H. S. Teoh via Digitalmars-d wrote:
> On Thu, May 15, 2014 at 03:22:25PM -0700, Walter Bright via Digitalmars-d wrote:
>> On 5/15/2014 2:41 PM, Timon Gehr wrote:
>>> On 05/15/2014 11:33 PM, Walter Bright wrote:
>>>> On 5/15/2014 9:07 AM, Timon Gehr wrote:
>>>>> Why? A memoizable function is still memoizable if it is changed
>>>>> internally to memoize values in global memory, for example.
>>>>
>>>> I doubt a compiler could prove it was pure.
>>>>
>>>
>>> Yes, that was actually my point. Memoizable is actually a non-trivial
>>> property.
>>>
>>> (But note that while a compiler cannot in general discover a proof,
>>> it could just _check_ a supplied proof.)
>>
>> If the compiler cannot mechanically verify purity, the notion of
>> purity is rather useless, since as this thread shows it is incredibly
>> easy for humans to be mistaken about it.
>
> What if the language allowed the user to supply a proof of purity, which
> can be mechanically checked?
>
> Just rephrasing what Timon said, though -- I've no idea how such a thing
> might be implemented. You'd need some kind of metalanguage for writing
> the proof in, perhaps inside a proof block attached to the function
> declaration, that can be mechanically verified to be correct.

Yes, either that or one could even just implement it in the existing language by introducing types for evidence, and basic termination checking.

eg. http://dpaste.dzfl.pl/33018edab028
(This is a really basic example. Templates or more language features could be used to simplify some of the more tedious steps, but I think it illustrates well the basic ideas. Maybe there are some small mistakes because I didn't find the time to actually implement the checker.)


> Alternatively, if only one or two statements are causing trouble, the
> proof can provide mechanically checkable evidence just for those
> specific statements.
>
> The metalanguage must be mechanically checkable, of course. But this may
> be more plausible than it sounds -- for example, solutions to certain
> NP-complete problems are verifiable within a far shorter time than it
> would take to actually solve said problem.

Indeed checking whether there is a proof of some fact up to some specific length N for a powerful enough logic is an NP-complete problem. (If N is encoded in unary.)

> This suggests that perhaps,
> while the purity of an arbitrary piece of code is, in general,
> infeasible for the compiler to mechanically prove, it may be possible in
> some cases that the compiler can mechanically verify a user-supplied
> proof, and thus provide the same guarantees as it would for
> directly-provable code.
>
>
> T
>

In fact, this would cover most cases. Usually there is some checkable reason why a piece of code is correct (because otherwise it would not have been invented in the first place.)

On 05/16/2014 01:56 AM, Walter Bright wrote:
> On 5/15/2014 4:00 PM, H. S. Teoh via Digitalmars-d wrote:
>> What if the language allowed the user to supply a proof of purity, which
>> can be mechanically checked?
>
> I think those sorts of things are PhD research topics.

Well, feasibility has long ago been demonstrated and I hope those ideas will eventually see general adoption.

> It's a bit beyond the scope of what we're trying to do with D.
>

Sure, but it still makes sense to be aware of and think about what would be possible. (Otherwise it is too tempting to get fully sold on inferior technology, based on the mistaken assumption that there is no way to do significantly better.)

On Thu, 15 May 2014 18:30:55 -0400, David Nadlinger <code@klickverbot.at> wrote:

> On Thursday, 15 May 2014 at 15:09:32 UTC, Steven Schveighoffer wrote:
>> But in this case, you have ignored the rules, […]
>
> Which rules exactly? My point is mainly that this area of the language is underspecified.

The rules that we have been discussing, you cannot make significant decisions based on the addresses of 2 unrelated pointers.

>> This means format("%x", ptr) isn't allowed to be pure?
>
> The short answer would be: Yes. The alternatives seem to be:
>   - Disallowing memory allocations in pure code (not workable)
>   - Bidding farewell to the idea that pure + no mutable indirections means FP-sense purity.

There is a 3rd option:

- FP purity, working fine as long as you don't do stupid things based on addresses. And even possibly working fine if you do stupid things based on addresses.

In other words, still assume FP purity, and if you expect randomness based on heap addresses to work, it just won't. Keep in mind, nothing discussed so far can cause invalid results. It just will be less random than expected. I really don't see a problem with this.

You are changing non-deterministic behavior to different, but still non-deterministic behavior. How do you even measure the impact?

>> What about calculating index offsets? Note that pointer math between two pointers on the same block of memory is perfectly legitimate.
>
> Taking offsets within the same block are fine. Even in the light of GC allocations being pure, this doesn't lead to any non-determinism, as there isn't any mechanism for the relative offset between whatever you are considering to change without any outside input.

I think it is impossible to statically prevent address comparison between 2 unrelated pointers, but statically allow address comparison between 2 related ones. The compiler does not have the information to determine whether 2 pointers are related at compile time.

In fact, it may do BOTH!

bool foo(int *x, int *y) pure
{
   return x < y;
}

bool bar() pure
{
   if(foo(new int, new int)) // bad
   {
      int[10] x;

      return foo(x.ptr, x.ptr + 5); // ok
   }
   return false;
}


In the interest of nailing down what the rules SHOULD be (and I agree they need to be in the spec), here is a strawman to discuss:

You cannot do comparisons between two unrelated heap pointers that were allocated from the heap inside the same pure call. This only applies to the pointer values themselves, not the data pointed at (as long as that data is not a similar pointer).

I will define the "same pure call" as the function call into a pure function from a non-pure function.

Note, this is not a rule to implement as a static enforcement, it's one the programmer must not do. Like 'undefined behavior'. I don't think we can enforce it, as I mentioned above.

A lint tool may be able to catch it, and we can also possibly catch it at runtime, as long as the allocator can determine whether you're inside a pure function.

-Steve

On 5/16/14, 4:53 AM, Timon Gehr wrote:
> On 05/16/2014 01:00 AM, H. S. Teoh via Digitalmars-d wrote:
>> On Thu, May 15, 2014 at 03:22:25PM -0700, Walter Bright via
>> Digitalmars-d wrote:
>>> On 5/15/2014 2:41 PM, Timon Gehr wrote:
>>>> On 05/15/2014 11:33 PM, Walter Bright wrote:
>>>>> On 5/15/2014 9:07 AM, Timon Gehr wrote:
>>>>>> Why? A memoizable function is still memoizable if it is changed
>>>>>> internally to memoize values in global memory, for example.
>>>>>
>>>>> I doubt a compiler could prove it was pure.
>>>>>
>>>>
>>>> Yes, that was actually my point. Memoizable is actually a non-trivial
>>>> property.
>>>>
>>>> (But note that while a compiler cannot in general discover a proof,
>>>> it could just _check_ a supplied proof.)
>>>
>>> If the compiler cannot mechanically verify purity, the notion of
>>> purity is rather useless, since as this thread shows it is incredibly
>>> easy for humans to be mistaken about it.
>>
>> What if the language allowed the user to supply a proof of purity, which
>> can be mechanically checked?
>>
>> Just rephrasing what Timon said, though -- I've no idea how such a thing
>> might be implemented. You'd need some kind of metalanguage for writing
>> the proof in, perhaps inside a proof block attached to the function
>> declaration, that can be mechanically verified to be correct.
>
> Yes, either that or one could even just implement it in the existing
> language by introducing types for evidence, and basic termination checking.
>
> eg. http://dpaste.dzfl.pl/33018edab028

Typo: int_leibiz_equality :o). -- Andrei

On Thu, 15 May 2014 08:43:11 -0700
Andrei Alexandrescu via Digitalmars-d <digitalmars-d@puremagic.com>
wrote:

> On 5/15/14, 6:28 AM, Dicebot wrote:
> > This is not true. Because of such code you can't ever automatically memoize strongly pure function results by compiler. A very practical concern.
>
> I think code that doesn't return pointers should be memoizable. Playing tricks with pointer comparisons would be appropriately penalized. -- Andrei

Agreed. The fact that a pure function can return newly allocated memory pretty much kills the idea of being able to memoize pure functions that return pointers or references, because the program's behavior would change if it were to memoize the result and reuse it. However, that should have no effect on pure functions that return value types - even if the function took pointers or references as arguments or allocated memory internally. They should but perfectly memoizable.

- Jonathan M Davis

On Thu, 15 May 2014 11:03:13 -0700
Walter Bright via Digitalmars-d <digitalmars-d@puremagic.com> wrote:

> On 5/15/2014 2:45 AM, Don wrote:
> > An interesting side-effect of the recent addition of @nogc to the language, is that we get this ability back.
>
> I hadn't thought of that. Pretty cool!

Definitely, but we also need to be careful with it. If @nogc just restricts
allocations by the GC and not allocations in general, and if we make it so
that malloc is pure (even if it's only when wrapped by a function which throws
an Error when malloc returns null), then I don't think that we quite get it
back, because while the GC may not have allocated any objects, malloc could
still have be used to allocate them. We'd need to be able to either say that
_nothing_ allocated within the function, which isn't quite what @nogc does as
I understand it (though admittedly, I haven't paid much attention to the
discussions on it, much as I would have liked to). So, maybe we need to
find a way to make it so that a wrapped malloc can be pure but isn't
@nogc? Though if we go that route, that implies that @nogc should have
been @noalloc. Regardless, I think that making malloc pure
definitely affects the issue of whether a @nogc function can be assumed
to not return newly allocated memory.

- Jonathan M Davis

On 05/16/2014 07:41 PM, Andrei Alexandrescu wrote:
> On 5/16/14, 4:53 AM, Timon Gehr wrote:
>> ...
>>
>> Yes, either that or one could even just implement it in the existing
>> language by introducing types for evidence, and basic termination
>> checking.
>>
>> eg. http://dpaste.dzfl.pl/33018edab028

> On 5/16/14, 4:53 AM, Timon Gehr wrote:
> (This is a really basic example. Templates or more language features
> could be used to simplify some of the more tedious steps, but I think
> it illustrates well the basic ideas. Maybe there are some small mistakes
> because I didn't find the time to actually implement the checker.)

>
> Typo: int_leibiz_equality :o). -- Andrei

If that is everything, then I am in good shape! :o)

On 05/17/2014 09:29 PM, Timon Gehr wrote:
>>
>
>>
>> Typo: int_leibiz_equality :o). -- Andrei
>
> If that is everything, then I am in good shape! :o)

It could be argued though, that this axiom was not too aptly named in the first place, because it describes the indiscernibility of identicals instead of the identity of indiscernibles.