Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Andrzej Krzemienski (akrzemi1_at_[hidden])
Date: 2012-10-09 04:04:40

2012/10/8 Evgeny Panasyuk <evgeny.panasyuk_at_[hidden]>

> 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?

IMO - yes. However, note that it is only my interpretation of N2887, which
says that axioms only state what compilers (and generic algorithm authors)
can assume - nothing more. Another interpretation of axioms (which I am not
in favor of) would be to say that axioms impose some constraints on type
'T' which must be met even if compiler cannot check them. I also believe
that the usage of term 'user' may be ambiguous. To be more precise I would
say: by instantiating a generic algorithm constrained by concept C with
concrete type X, you agree to all code transformations that may occur as a
result of making use of C's axioms; regardless if X is prepared for these
transformations or not.

> 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:

Again, under the interpretation in N2887, I would say that you are right
about points (1) and (3), but not necessarily by (2). That is, you are
right that no-one else besides the guy that instantiates the constrained
template has any responsibility, but such a user does not have to make sure
that the axioms hold either: in fact he may deliberately request the
instantiation because he knows the axioms do not hold and he wants to make
use of this!

One example provided by Matt is copy elision. Just suppose for a second
that CopyElision is an axiom. Even if you know that type X has a destructor
or copy constructor with side effects you still want to make use of the
axiom. Because you allow the pair-wise cancellation of side effects of both
operations. (Note that if compiler was checking if type X satisfies axiom
CopyElision, it would refuse to compile or prevent a useful optimization).

Another example of axioms for code transformations would be the following:

  axiom AvoidCancellation( T x, T y ) {
    y * x / x <=> y;
  }

You know that it does not hold for any reasonable arithmetic type: and
that's why you define it. With this axiom the compiler knows what
transformations to perform to avoid producing NaNs.

> 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.

The previous concept proposals offered concept maps for this purpose. For
instance n2906 suggested the following solution: by default concepts are
implicit (auto-concepts), but concept refinements that differ from their
bases only by axioms are defined as explicit, and you need to use a concept
map to state that your type models the refined concept.
N3351<http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2012/n3351.pdf>suggests
the use of tags for this purpose: in short, you turn an axiom set
into a bit artificial small syntactic requirement. One could think of a
separate language feature for this purpose, but if such axiom-only concept
refinements are rare it may not be worth the effort.

Regards,
&rzej