Positive

[Andrei Alexandrescu]

Bruce Adams wrote:
> On Sun, 05 Oct 2008 15:12:13 +0100, Andrei Alexandrescu 
> <SeeWebsiteForEmail at erdani.org> wrote:
>>> Internal temporaries would be checked at compile time (when 
>>> initialised to a compile time constant value)
>>> so there would be no added cost to implementing sqrt only using it 
>>> with values that might
>>> be negative.
>>
>> That can't be done in the current language, sigh.
>>
> It can't? That surprises me. Doesn't CTFE apply to:
> 
> Positive!(int) x = 1;

Not currently.

>>> If my understanding is correct you are proposing this mainly because 
>>> unlike contracts,
>>> templates are checked by the compiler at compile time.
>>> I suspect that is the real problem. I and others have previously 
>>> tried to argue for compile
>>> time checkable contracts.
>>> Another advantage of compile time contracts is that you can design 
>>> and test arbitrary new
>>> categories of type without having to add new type specifiers to the 
>>> language. I'm thinking about
>>> const and pure here. Though pure would require functions to have 
>>> visible compile time attributes
>>> (as opposed to the purely invisible ones which must exist internally) 
>>> which is another kettle of fish.
>>
>> I'd love compile-time-checked contracts, but they're simply not doable 
>> with current compiler technology.
>>
>> Andrei
> 
> I disagree. I'm not saying its easy but it could be done. We would have 
> to start
> with something relatively simple and work our way up but it could be done.

I, too, think it can be done in the same way supersonic mass
transportation can be done, but having done research in the area I can
tell you you are grossly underestimating the difficulties. It is a
project of gargantuan size. Today the most advanced systems only managed
to automatically prove facts that look rather trivial to the casual
reader. There is absolutely no hope for D to embark on this.

> Compiler's already do all kinds of clever analyses behind the scenes but 
> each one
> is often hard coded. I suspect the main difficulty is giving users too 
> much rope
> by which to hang themselves, or rather hang the compiler trying to prove 
> something
> it doesn't realise it can't. Marrying declarative / constraint based 
> programming
> at compile time is creeping in via templates. I wish it was less well 
> hidden.

I discussed the problem this morning with Walter and he also started
rather cocky: if you assert something early on, you can from then on
assume the assertion is true (assuming no assignment took place, which
is not hard if you have CFA in place). He got an arrow in a molar with
the following example:

double[] vec;
foreach (e; vec) assert(e >= 0);
// now we know vec is all nonnegatives
normalize(vec);

The definition of normalize is:

void normalize(double[] vec)
{
     foreach (e; vec) assert(e >= 0);
     auto sum = reduce@"a + b"(vec, 0);
     assert(sum > 0);
     foreach (ref e; vec) e /= sum;
}

If normalize takes udouble[] and you have one of those, there's no need 
to recheck. Automated elimination of the checking loop above is really hard.


Andrei