On 15.5.2014. 17:24, Andrei Alexandrescu wrote:
> On 5/15/14, 3:31 AM, luka8088 wrote:
>> Yeah, I read all about weak/string purity and I do understand the background. I was talking about strong purity, maybe I should pointed that out.
>>
>> So, to correct myself: As I understood strong purity implies memoization. Am I correct?
> 
> Yes, as long as you don't rely on distinguishing objects by address.
> 
> Purity of allocation is frequently assumed by functional languages because without it it would be difficult to get much work done. Then, most functional languages make it difficult or impossible to distinguish values by their address. In D that's easy. A D programmer needs to be aware of that, and I think that's fine.
> 
> 
> Andrei
> 
> 

Hm, this does not seem right. @safe prevents you from taking the address
of of a value, as stated in
http://dlang.org/function.html#safe-functions , shouldn't pure do the same?

Reading again through the @safe docs it seems to me that purity (both strong and weak) should imply @safe.

I have seen many claims that in D pure means something else from what it means in functional languages and I think that it is too bad if there is not going to be functional language alike purity in D. I have not seen any example of something that can't be forbidden by the compiler if such support would considered.

On 05/15/2014 07:41 PM, Steven Schveighoffer wrote:
>>
>> Not really, allocation is just an implementation detail. The
>> computational language is meaningful independent of how you might
>> achieve evaluation of expressions. I can in principle evaluate an
>> expression of such a language on paper without managing a separate
>> store, even though this usually will help efficiency.
>>
>> Functional programming languages are not about taking away features
>> from a procedural core language. They are based on the idea that the
>> fundamental operation is substitution of terms.
>
> But they do not deal in explicit pointers.

(Well,

http://hackage.haskell.org/package/base-4.7.0.0/docs/Foreign-Marshal-Alloc.html#v:malloc )

> Otherwise, that's a can of
> worms that would weaken the guarantees, similar to how D's guarantees
> are weakened.
> ...

The concept of a 'pointer' to some primitive value does not have a meaning in such languages. Every value is an "rvalue".

> We have no choice in D, we must accept that explicit pointers are used.
> ...

We could e.g. ban comparing immutable references for identity / in-memory order.

>>> To be honest, code that would exploit such an anomaly is only ever used
>>> in "proof" exercises, and never in real code.
>>
>> Hashtables are quite real.
>
> Pretend I'm ignorant, what does this imply?
> ...

E.g. order of iteration may be dependent on in-memory order of keys and the 'same' keys might occur multiple times.

>> This is the issue:
>>
>> On Thu, 15 May 2014 10:48:07 +0000
>> Don via Digitalmars-d <digitalmars-d@puremagic.com> wrote:
>>>
>>>> Yes. 'strong pure' means pure in the way that the functional
>>>> language crowd means 'pure'.
>>>> 'weak pure' just means doesn't use globals.
>>
>> There is no way to make that claim precise in an adequate way such
>> that it is correct.
>
> This doesn't help, I'm lost with this statement.
>
> -Steve

The issue is that there are apparently different expectations about what the keyword is supposed to do.

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.

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

On 05/15/2014 03:06 PM, "Ola Fosheim Grøstad" <ola.fosheim.grostad+dlang@gmail.com>" wrote:
> On Thursday, 15 May 2014 at 12:37:22 UTC, w0rp wrote:
>> To consider the design of pure, you must first consider that you
>> cannot add functional purity to an imperative language.
>
> Of course you can. Functional languages execute in an "imperative
> context".  That's why you need monads.
> ...

Strictly speaking you don't "need" monads, they are sometimes just an adequate way of structuring a program.

> The term "pure function" is only needed in a non-functional language.
> Applicative/functional languages only have mathematical functions, no
> need for the term "pure" there.

In discussions about e.g. Haskell, it is often used to denote an expression of a specific form inside a `stateful' DSL. E.g. if "η" is the unit of some monad, then (η v) is sometimes called a "pure value", while values of other forms are not called pure.

On 05/15/2014 08:03 PM, Andrei Alexandrescu wrote:
>>>
>>> Purity of allocation is frequently assumed by functional languages
>>
>> Examples?
>
> cons 1 2 is equal to cons 1 2
> ...

I don't see anything whose specification would need to mention 'allocation'.

>>> because without it it would be difficult to get much work done.
>>
>> Why?
>
> It's rather obvious. You've got to have the ability to create new values
> in a pure functional programming language.

This kind of operational reasoning is not essential. Of course, in practice you want to evaluate expressions, but the resulting programs are of the same kind as those of a non-pure language, and can do the same kind of operations. There is not really a distinction to be made at that level of abstraction.

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.

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.

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

> 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 would expect that someone could be able to write a type equivalent to a slice, and it should be allowed to be pure.

Yes.

David

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

-- 
When solving a problem, take care that you do not become part of the problem.

H. S. Teoh:

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

Yes, this is common enough. As an example the Whiley (http://whiley.org/ ) is not able to find the proof for various invariants and contracts, but the programmer can write them down and Whiley verifies them to be correct during the compilation. Inventing a proof is harder, but verifying it is often much easier.

The first way D can introduce such things (simple proof) is in the static verify of some contracts.

Verifying @memoizable or @reflexive/@symmetric/@transitive (for functions with two arguments) is perhaps a bit too much ambitious for D compilers. But it surely goes well with the idea of a language that tries to both avoid bugs and generate efficient binaries :-) (And perhaps someday C++ Axioms of Concepts will be handled by a C++ compiler able to verify a function to be symmetric).

Bye,
bearophile