Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Marcin Zalewski (marcin.zalewski_at_[hidden])
Date: 2012-10-04 16:43:29

On Fri, Sep 28, 2012 at 5:39 AM, Andrew Sutton <asutton.list_at_[hidden]> wrote:
>>> 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):
>
> *cringe* Don't think about eq(). That was a compromise between myself
> and Marcin Zalewski. We couldn't determine if <=> should be
> interpreted as logical equivalence or behavioral equivalence (as in
> the previous axioms work). We ended assigning <=> to logical
> equivalence and using eq() as a kind of oracle that decided equality:
> either according to the rules of == or memberwise equality comparison.

Just to put it into perspective, equality comes from Elements of
Programming. Page 7 shows that there is a "specification" equality and
a "C++" equality. If one reads the first chapter of EoP, the notion of
equality is explained well in context of what the types actually
represent. In a sense, there is an implicit assumption of
"denotational" semantics that assigns to every value an abstract
*mathematical* entity. Then, equality is simply mathematical equality
on these entities.

The == operator *does not* have to always be implemented. The book
discusses this as well. Sometimes it is hard, and sometimes it is
impossible to implement ==. Sometimes it is enough to just compare
some kind of a hash. In some other cases, we may settle for
representational equality, where we just compare bits. This gives us a
partial implementation of a true equality.

There is a paper related to this subject, by John Lakos:

http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2007/n2479.pdf

This paper has a similar notion of equality.

> In retrospect, I think this was the wrong choice. Using <=> to
> describe the behavioral equivalence of two expressions provides a much
> more robust way of stating the relative meaning of operations.

To put this into perspective too, I think that "behavioral"
equivalence here would be an equivalence in terms of "operational"
semantics. I don't think that either approach is wrong in any way.
Each approach fits some applications better then others. If behavioral
equivalence is taken to mean equality defined in terms of operational
semantics, then defining it works out a bit differently. For example,
we must deal with cases such as 1/2 and 2/4 being equal which comes
for free in denotational semantics, but requires some fiddling in
operational semantics. We just need to be careful about how we defined
"behavioral equivalence," but that is not to say that it is
impossible.

So, to summarize, the current approach is a direct descendant of EoP
where we have simply renamed the "specification" = from page 7 to
eq(). Reading EoP carefully can help in understanding how it works.
For operational definitions of equality, one can look back at the
existing work.

BTW, just an additional example to keep in mind, which we have used
frequently. Two vectors with equal elements but different capacities
(allocated memory) are trivially equal in denotational approach (such
as used in EoP) since they end up representing identical mathematical
sequences. With operational semantics one has to sweat a bit more, and
perhaps say something like "the two vectors will behave the same with
respect to some operations." This has to be a recursively applied
definition, since these operations may themselves return something
that differs only, say, in memory allocation. Thus, for operational
definition, we always need some "context" to decide when things are
equal. The denotational definition needs a context too, but it takes
care of it right away and once and for all.

> Andrew
>
> _______________________________________________
> Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost