On Wednesday, 22 October 2014 at 21:34:51 UTC, Peter Alexander
wrote:
Term rewriting is very interesting, and I believe some work has
been done for this in Haskell. I don't believe anything has
been done with this propositions and inference approach you
describe.
I would always assume it has been done plenty of work related to
proving properties about a program since this is the holy grail
of CS!
I think it is related to so-called dependent types?
http://en.wikipedia.org/wiki/Dependent_type
I'd like to take a look at Xanadu some time…
http://www.cs.bu.edu/~hwxi/Xanadu/Xanadu.html
And Agda which also guarantee termination!
http://en.wikipedia.org/wiki/Agda_(programming_language)
I see a number of problems:
First, annotating this, in the presence of templates, is very
hard. Consider:
auto f(alias g, T)(T x) { return g(x); }
We cannot possibly annotate this function with any of
propositions you described because we know nothing about g or T.
Why not? You know the moment you instantiate.
If you had pattern matching you could break the signature into
multiple distinguishing ones, but the equivalent is to put
conditionals into the postcondition.
Like purity and nothrow, we'd have to deduce these properties,
but most escape deduction in all but the most trivial cases.
I think you can solve this with logic/constraints programming and
simple dataflow analysis.
// a is @notnull and @aliasfree
b = sort(a)
// b is @notnull, @aliasfree, @sorted_ascending(somekey)
// assume f is @sortpreserving, @pure
c = f(b)
// b is @notnull, @aliasfree, @sorted_ascending(somekey)
// assume reverse is @sortpreserving, @pure
d = reverse(b)
// d is @notnull, @aliasfree, @sorted_descending(somekey)
e = unknownfunction(b)
// e is @typeinfobased
Suppose we could deduce a large subset of useful propositions,
how does the programmer know what has been deduced?
He doesn't have to. The point is to express common patterns in
the most terse and readable way. Developers analyze this and come
up with the appropriate heuristics. Juste like with peephole
optimization?
How can I tell what has been deduced and applied without having
to disassemble the code to see what's actually going on?
If you are that performance oriented then you will not use
templates at all! Generic programming is not suitable for
performance… Because performance comes with changing the data to
fit the hardware, e.g. SIMD instruction set, caches etc
And even if everything is deduced correctly, and I know what's
deduced, what if it does a transformation that's undesirable?
For example, you changed linear_search to binary_search. What
if I knew the element was likely to be at the front and would
prefer linear_search to binary_search?
That's a good point, but then you should be able to guide the
search by adding an optimization hint that states that the sought
element probably is at the front, or that you constrain the
search to a linear_search.
But that does not have to be part of the semantics of the
program. So you can keep correctness and optimization separate.
IMO it is always an advantage to keep the code that has to do
with correctness short, simple and readable.
