templatizing parameters and induction (was Re: Writing Bug-Free C/D Code)

[Don Clugston]

Andrei Alexandrescu (See Website For Email) wrote:
> Kevin Bealer wrote:
>> Dan wrote:
>> ...
>>> What should then happen is this:  The compiler should recognize that we
>>  > only accept values such that x > y.  Knowing that, it should then 
>> verify
>>> that in all cases where this function can be called, that the input 
>>> to the
>>  > function must have this condition.  In cases where this *can* fail, it
>>> should raise an error - such as variables that are affected by user 
>>> input
>>  > or outside parameters that aren't already bounds checked or 
>> adjusted...
>>>
>>> Theoretically, one could take any given int (between int.min and 
>>> int.max)
>>  > and adjust it such that x > y will be true for all cases.  This can be
>>  > proven and verified by a proof by induction.
>>>
>>> If you don't isolate the in/out tests from the body, a proof by 
>>> induction
>>> couldn't know what needs to be proved to prove the code safe.
>>
>> I think there are very few cases where this kind of induction could 
>> reasonably be done, unless x and y are literals.  I suspect that in 
>> most cases where the compiler had enough info to do this kind of 
>> induction checking, the code for the function could nearly as easily 
>> be "constant folded" and optimized away entirely.  Prove me wrong, but 
>> I suspect that this kind of induction is too hard (and in the cases 
>> where it works, too slow) to be practical.
>>
>> If x and y are literals, though, you can do something like this now:
>>
>> Original source:
>>
>> int foo(int x, int y, int z)
>> {
>>     assert( x > y ); // runtime
>> ...
>> }
>>
>> int z = foo(10, 20, 30);
>>
>> Checking at compile time:
>>
>> int foo(int x, int y)(int z)
>> {
>>     static assert( x > y ); // compile time
>> ...
>> }
>>
>> int z = foo!(10, 20)(30);
>>
>> It's a very simple transformation --- take any compile-time known 
>> values and make them template parameters.  In this case, the calling 
>> syntax even looks nearly the same!
> 
> The need to cater for cases with partial statically-available
> information is seriously taken into consideration. The general scenario
> is called "partial evaluation": you call a function with a few
> statically-known values and a few runtime values. The current
> compile-time evaluation mechanism can't help with that. So a considered
> addition to D is to accommodate static parameters (pushed by yours truly
> and using a syntax suggested by Dave Held):
> 
> int foo(int x, int y, int z);
> int foo(static int x, int y, int z); // x is known during compilation
> int foo(int x, static int y, int z); // y is known during compilation
> int foo(static int x, static int y, int z); // x and y are... you know

I pushed for essentially the same thing, about six months ago:

http://lists.puremagic.com/pipermail/digitalmars-d/2006-October/008987.html

and the syntax I proposed was:

int foo(template int x, template int y, int z)
{
    static if (is(x: const) && is(y: const)) { ... }
    else return simple_foo(x);
}

I think the concept (in whichever form) is a killer feature; the 
potential for optimisation is incredible.