Comparisons of incompatible types

[Mark Wooding]

John Nagle <nagle at animats.com> writes:

[Stepanov]
> makes the point that, for generic programs to work right, the basic
> operations must have certain well-defined semantics.  Then the same
> algorithms will work right across a wide variety of objects.
>
> This is consistent with Python's "duck typing", but inconsistent with
> the current semantics of some operators.

This isn't a disaster.  You should check that the arguments define the
necessary operations and obey the necessary axioms.  Python is already
dynamically typed: this kind of proof-obligation is already endemic in
Python programming, so you've not lost anything significant.

> For example, "+" as concatenation makes "+" non-commutative.  In other
> words,
>
> 	a + b
>
> is not always equal to
>
> 	b + a
>
> which is not good.

I think I probably agree with this.  Concatenation yields a nonabelian
monoid (usually with identity); `+' is pretty much universally an
abelian group operator (exception: natural numbers, where it's used in
an abelian monoid which extends to a group in a relatively obvious way).
But then we'd need another operator symbol for concatenation.
Nonnegative integers act on strings properly, but the action doesn't
distribute over concatenation, which is also a shame.  i.e.,

        n*(a + b) != n*a + n*b

But it's a familiar notation, by no means peculiar to Python, and
changing it would be difficult.

> Exactly one of
>
> 	a > b
> 	a = b
> 	a < b
>
> is true, or an type exception must be raised.

This will get the numerical people screaming.  Non-signalling NaNs are
useful, and they don't obey these axioms.

I think, more generally, that requiring a full total order (rather than
either a preorder or a partial order) is unnecessarily proscriptive.
Sorting only requires a preorder, for example, i.e., { (a, b) | a <= b
<= a } is an equivalence relation, and the preorder naturally induces a
total order on the equivalence classes.  Topological sorting requires
only a partial order, and makes good use of the notation.  As an
example, sets use `<=' to denote subsetness, which is well known to be a
partial order.

(I presume you weren't going to deny

        a <= b iff a < b or a == b

or

        a < b iff b > a

because that really would be bad.)

> The basic Boolean identities
>
> 	(a or b) == (b or a)
> 	not (a or b) == (not a) and (not b)
> 	not (not a) == a
>
> should all hold, or an type exception should be raised.

The first of these contradicts the axiom

        x => x or _|_ == x

which is probably more useful.  The last can't usefully be true since
`not' is lossy.  But I think that, for all values a, b,

        not (a or b) == not (b or a) == (not a) and (not b)
        not (not (not a)) == not a

which is probably good enough.  (The application of `not' applies a
boolean coercion, which canonifies adequately.)

-- [mdw]