Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Evgeny Panasyuk (evgeny.panasyuk_at_[hidden])
Date: 2012-10-08 15:02:41

08.10.2012 14:06, Andrzej Krzemienski wrote:
> Should the programmer instantiate STL algorithms for 'T' == double? My
> answer is: they know the risks (of potentially not meeting the
> assumptions), they should assess if the risk is low or make sure they
> eliminate the usage of NaNs, and they should make the call at their own
> risk. If the program has a bug due to type double not having met the
> assumptions on 'T' it is the fault of the programmer who requested the
> instantiation of the algorithm with type double.
>
> Axioms (according to N2887) do not change this situation. An assumption of
> type 'T' is never 'valid' or 'invalid'. It is just an assumption that one
> may use or not. When you request an instantiation of an algorithm
> constrained with an 'axiom-rich' concept with type X, you take the
> responsibility for X meeting or not the expectations expressed in the
> concept.

So, all responsibility is on user, and in that case, compiler MUST not 
reject code if he founds that type does not fulfil axioms.
Is it right?

> The good strategy for compilers, regarding axioms, would be to make use of
> axioms only if they have some way of verifying if type 'X' meets them,
> (either by limited static code analysis or run-time checks). This might
> require selecting only a subset of all axioms that the compiler is able to
> check and utilize only this subset.

So, if type does not fulfil axioms, then compiler must not complain AND 
it must not make any assumptions and optimizations based on these axioms?
So, within this approach if user pass some ieee754 floating point type 
to algorithm which expects types with associative addition operation, 
compiler MUST not assume associativity, can't do optimizations, is it right?
Even if user want to take all responsibility, and he accepts all 
side-effects?

That does not sounds - if all responsibility to check is on user, 
compiler should be free to exploit axioms knowledge.

Currently, I inclined to following approach:
1. Compiler MUST not do any checks on axioms besides syntactic.
2. User has ALL responsibility on verifying axioms.
3. Compiler has rights to exploit any knowledge which it gets from 
axioms, regardless of fact if type fulfil them or not.
I.e. in following example:
axiom { a.size() == a.length(); }
and:
int T:size() { return 0;}
int T:length() { return 1;}
Compiler has rights to substitute a.size() with a.length(); - user takes 
all responsibility for such cases.

What I would like also to see, or at least to discuss, is requirement to 
explicitly state that type fulfils axioms. Maybe something similar to 
non-intrusive traits approach.
That would be more robust than requirements only at algorithms side 
which are silently accepted. That would also allow us to overload 
functions on axioms too.
For instance some types may have exactly same syntactic requirements, 
but fulfil different axioms. In general compiler can't check axioms, so 
it can't select right overload.
If axioms would be not used for overload, then we have to "duplicate" 
them with traits.

Best Regards,
Evgeny