Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Andrzej Krzemienski (akrzemi1_at_[hidden])
Date: 2012-09-29 08:34:16

>
> >> For instance, axiom EqualityComparable::Reflexivity states that some
> >> (rather than every) objects must compare equal to themselves. If you
> >> consider type float, objects with value NaN (not-a-number) compare
> unequal.
> >
> > No; all well-formed values of a type can be compared for equality (if
> > the type is EqualityComparable). NaN is not a well-formed value. It is
> > literally *not a number*.
> >
>
> Unless you mean to say that any program that uses
> a NaN in any way has undefined behavior, this notion
> of a "well-formed value" seems arbitrary and capricious.
>

This entry at Bjarne Stroustrup's FAQ:
http://www.stroustrup.com/C++11FAQ.html#axioms
presents a reasonable "semantics" of axioms. If an axiom states an
equivalence between two expressions, compilers and other tools are allowed
to make an assumption that one expression can be substituted for another
and perform optimizations or other code transformation or analysis based on
this assumption regardless if the assumption holds or not. When you
instantiate template FUN with type X, you are responsible for guaranteeeing
that this assumption will hold. Under this interpretation we do not care
(while doing transformations) that we get NaN or not. In fact, the
following axiom:

  x / y * y <=> x;

could be used to avoid the generation of NaN value for some values of x and
y. Of course, such "allowance of substitution" would only make sense inside
concept-constrained function templates (or member functions of class
templates) because in "free code" (i.e, with no templates, you may want to
rely on the semantics of NaN's.Also, with the previous concept design that
used concept maps, a type could model some concept in more than one way.
For instance type int models concept Monoid in two ways: using addition and
identity element 0 as well as using multiplication and element 1. I am not
sure how the making use of axiom would work in such situations unless we
are in a constrained template.

Regards,
&rzej