Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Vicente J. Botet Escriba (vicente.botet_at_[hidden])
Date: 2012-10-02 17:29:34

Le 26/09/12 21:00, Lorenzo Caminiti a écrit :
> Hello all,
>
>
>
> However, N3351 says that axioms should not be checked by the compiler...
>
> ``Axioms express the semantics of a concept’s required syntax; they
> are assumed to be true and
> must not be checked by the compiler beyond conformance to the C++
> syntax. Any additional
> checking is beyond the scope of the compiler’s translation
> requirements. The compiler must not
> generate code that evaluates axioms as preconditions, either. This
> could lead to program errors
> if the evaluated assertions have side effects. For example, asserting
> that distance(first, last) > 1
> when the type of those iterators is istream_iterator will consume the
> first element of the range,
> causing the assertion to pass, but the algorithm to have undefined behavior.''
>
> So what am I supposed to do with axioms? Do nothing? Axioms are just
> "comments" that document the semantic?
>
> For example:
>
> ``
> concept EqualityComparable<typename T> =
>      requires (T a, T b, T c) {
>          bool { a == b };
>          bool { a != b };
>          axiom { a == b <=> eq(a, b); } // true equality
>          axiom {
>              a == a; // reflexive
>              a == b => b == a; // symmetric
>              a == b && b == c => a == c; // transitive
>          }
>          axiom { a != b <=> !(a == b); } // complement
>      };
>
> So, EqualityComparable<T> is true if T
> 1. has == and != with result types that can be converted to bool
> 2. == compares for true equality
> 3. == is reflexive, symmetric, and transitive
> 4. != is the complement of ==
> However, the compiler can only check the first of these conditions.
> The rest must be verified
> through other means (i.e. manually).
> ''
>
Hi Lorenzo,

Not only the compiler should not check the axioms, but it will in 
general be unable to do it. So a type modeling the non-axiom part is 
seen as a model of the concept even if doesn't satisfy the axioms.

An alternative for the concept definition could be to force the modeler 
to state explicitly that the class satisfies some kind of semantic trait 
associated to the axiom.

The preceding example can be rewrite as follows

concept EqualityComparable<typename T> =
     TrueEquality<T> && EqualReflexive<T> && EqualSymetric<T> && EqualTransitive<T> &&
     requires (T a, T b, T c) {
         bool { a == b };
         bool { a != b };
     };

where

concept TrueEquality<typename T> = is_true_equal<T>::value &&
     requires (T a, T b) {
         axiom { a == b <=> eq(a, b); } // true equality
     };

concept EqualReflexive<typename T> = is_equal_reflexive<T>::value &&
     requires (T a) {
             a == a; // reflexive
     };

concept EqualSymmetric<typename T> = is_equal_symetric<T>::value &&
     requires (T a, T b) {
             a == b => b == a; // symmetric
     };

concept EqualTransitive<typename T> = is_equal_transitive<T>::value &&
     requires (T a, T b, T c) {
             a == b && b == c => a == c; // transitive
     };

The traits is_true_equal, is_equal_reflexive, is_equal_symmetric and 
is_equal_transitive could be defined for the builtin types as a 
true-type and a false-type otherwise. A user defining a class X that is 
a model of EqualityComparable should need however to specialize these traits

template <> is_true_equal<X>: true_type {};

template <> is_equal_reflexive<X>: true_type {};

template <> is_equal_symmetric<X>: true_type {};

template <> is_equal_transitive<X>: true_type {};

In this way, the compiler could take advantage of the axioms but only 
when the modeler has given permission.

This has of course a lot of disadvantages as ...

Best,
Vicente