Algorithms, term rewriting and compile time reflection

[via Digitalmars-d]

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.