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
