Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Andrzej Krzemienski (akrzemi1_at_[hidden])
Date: 2012-10-01 16:32:23

> > Yes, and you'll never be able to actually do anything programmatically
> > with is_valid.
>
> Same for eq(), <=>, and =>, I can't do anything programmatically with
> them neither, can I?
>

I suppose you cannot.

> Just to clarify, when I say to use code comments, you could use
> programming-style comments. So the difference is between:
>
>     concept BidirectionalIterator<ForwardIterator I> = // (a)
>         requires decrement (I i, I j) {
>             axiom {
>                 is_valid(––i) <=> is_valid(i––);
>                 is_valid(i––) => (i == j => i–– == j);
>                 is_valid(i––) => (i == j => (i––, i) == ––j);
>             }
>             ...
>
> And:
>
>     concept BidirectionalIterator<ForwardIterator I> = // (b)
>         requires decrement (I i, I j) {
>             // axiom {
>             //     is_valid(––i) <=> is_valid(i––);
>             //     is_valid(i––) => (i == j => i–– == j);
>             //     is_valid(i––) => (i == j => (i––, i) == ––j);
>             // }
>             ...
>
> As Andrzej pointed out, (a) is better than (b) because the compiler
> will error if the axioms get out of sync with the rest of the concept
> (change type/variable name I, i, j, etc). Any other reason to favor
> (a) over (b)? (Leaving a side possible future compiler optimizations
> that might never come and that will not be possible with a lib like
> Boost.Contract in any case.)
>

The other reasons I can think of can just work comments: e.g.,
differentiating two concepts that differ only by semantics but not syntax,
like InputIterator and ForwardIterator or StrictWeakOrder<T> and
Predicate<T, T>.

IMO, with (b) is more clear that axioms don't actually check anything
> while (a) can be misleading causing programmers to think that the
> expressed semantics of the concept will actually be checked and
> enforced by the program. I guess it's only fair to assume that
> programmers read the docs and understand that axioms _document_ but
> don't actually check or enforce the semantics.
>

Not supporting axioms altogether, I guess, is also a reasonable approach.
As you say, many people are confused about axioms' semantics. And having
axioms in concepts as language feature (rather than informal comments) is
controversial in general: mostly because there is almost nothing a compiler
could do about them.

> At the end, I'm thinking that there's value in the syntax checking
> provided by (a) over (b) (even if I wish (a) could check and enforce
> more of the semantics maybe generating preconditions to check at
> run-time for the concept... I'm not sure...).
>

But then again, you are implementing a contract programming library; and
the primary goal of specifying contracts -- I believe -- is not that you
check them in run-time, but that everyone can read what they state: they
are a comment, although enforced by run-time checks, if one can say so.

It looks like it may be more the question of an arbitrary call. My
preference would be to be able to specify axioms with concepts, although I
find it difficult to justify why. Perhaps when they are part of language
(or type-system) I feel more obliged to satisfy them. :)

Regards,
&rzej