Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2012-09-27 15:42:52

On Thu, Sep 27, 2012 at 12:29 PM, Marc Glisse <marc.glisse_at_[hidden]> wrote:
> On Thu, 27 Sep 2012, Lorenzo Caminiti wrote:
>
>> On Thu, Sep 27, 2012 at 12:03 PM, Nathan Ridge <zeratul976_at_[hidden]>
>> wrote:
>>>
>>>
>>>> Again, I'm learning these things as we go... but aren't => and <=> the
>>>> "implies" and "if and only if" logical operators? If so, their operand
>>>> must be boolean predicates so I don't understand what this axioms
>>>> means:
>>>>
>>>> c.resize(0) <=> c.clear()
>>>>
>>>> Oh, I see, <=> is some sort of magic "equivalence" operator as it can
>>>> be defined only meta+programmatically in the programmer's mind. This
>>>> axiom means that "the effect of c.resize(0) must be /equivalent/ to
>>>> c.clear()" in a way that the program will never be able to assert. I
>>>> can't even check that syntactically, can I? What does it mean to check
>>>> the axiom above syntactically given that I'd have to completely strip
>>>> away the <=> operator because it cannot be represented
>>>> programmatically? Then such an axiom is just a code comment and maybe
>>>> it should be programmed as such IMO.
>>>
>>>
>>> Perhaps we can interpret this formally as "all the variables that appear
>>> in both expressions [in this case, c] compare equal after the expressions
>>> are evalauted"?
>>
>>
>> Yeah, I was thinking more about it and maybe we can program it more or
>> less like this:
>>
>> c1.resize(0);
>> c2.clear();
>> assert( eq(c1, c2) ); // the actual check
>>
>> For every (this "for every" part is going to be hard to implement) c1
>> and c2 of type C and where eq returns true iff c1 and c2 are equal (eq
>> could be implemented as operator== at least to start with).
>
>
> One could write axioms for types that don't have an operator==, or where
> comparison doesn't make sense:
> p=malloc(n) <=> p=realloc(0,n)

Wouldn't this mean the following? For any p and q of some type T:

p = malloc(n);
q = realloc(0, n);
assert( eq(p, q) );

Where eq() is the N3351 equality operator that checks if two objects
are equal. eq could be implemented using == but it's more of a logical
equality so even if a type doesn't have == than it is still logically
sensible to check if two objects for that type are the same. In
reality however, eq will have to be implemented and checkable somehow
so if a type doesn't have a way to programatically checked for
equality (using == or some other boolean function eq(), equal(),
is_equal(), etc) then either you don't program the axiom or you add an
assertion requirement to guard against the lack of == (like
Boost.Contract does):

p = malloc(n);
q = realloc(0, n);
assert( p == q ), requires has_equal<T>::value; // with assertion
requirement that T has ==

For a given T, if has_equal<T>::value is true, assert( p == q ) will
be compiled and checked at run-time, otherwise it will not even be
compiled.

> v.random_shuffle().random_shuffle() <=> v.random_shuffle()
> (x+y)+z <=> x+(y+z) for double (somewhat like passing -fassociative-math
>   to gcc)

--Lorenzo