On to Hydro

[Tyler Close]

Ben Laurie wrote:
> Tyler Close wrote:
> > >  But having partially ordered elements respond to "<=",
> > > but not respond
> > > to "<", freaks me out.
> >
> > It actually seems very natural to me. In order to search a linear
> > container, you need to have either the "<", or the ">",
> operator. A
> > partial ordering does not let you search a linear
> container, and so
> > does not provide either the "<", or the ">" operator.
> Pretty slick,
> > no?
>
> No - this is, in effect, (a -> b) -> (a' -> b'), which is,
> of course,
> false.

Does formal proof logic apply to software interface design?

I do know that a fact of software interface design is that the
interface defines the space of possible operations. My opinion is that
if the operation is not in the space, then the interface should not
include it.

> Besides, "a < b" can be defined as "a <= b && a != b" if you "only"
> provide "<=".

"a <= b && a != b" does not result in a total ordering. The contract
for "a < b" would be that it provides a total ordering. If you tried
to search a linear container using your partial order "<", then your
search would be broken in the way defined by the "<=" contract.

Note that your partial order "<" would allow you to search a
multi-dimensional container like the Xanadu containers. A Xanadu
container could be implemented in E using only the "<=" operator, as
Dean has pointed out. So your syntactically plausible implementation
is valid, so long as you only apply it within the space that it is
defined to be valid for. By not providing your implementation by
default, the language makes it clear that the implementation is only
valid within the space defined by the "<=" operator.

Tyler


__________________________________________________
Do You Yahoo!?
Talk to your friends online with Yahoo! Messenger.
http://im.yahoo.com