Typing system vs. Java

[Alex Martelli]

"Christian Tanzer" <tanzer at swing.co.at> wrote in message
news:mailman.996682083.19421.python-list at python.org...
    ...
"""
> Back to Python -- programming in Python has always felt to
> me a *LOT* like generic programming

Yup. Only, in Python it's very implicit.
"""
...just about as in C++, except more so:-).


"""
The nice thing about Ada and Eiffel generics is that the requirements
on the generic parameters are spellt out explicitly. For most
"""
The problem with Ada and Eiffel generics is that the requirements
on the generic parameters are to be spelled out explicitly.  Type
inference (as in Haskell) or signature-based polymorphism (as in
C++ templates and in Python) is smooth indeed (although the ability
to state out loud what you think the compiler will infer, if it
could be done without really adding any significant complexity,
would be a nice extra).

The issue from my POV is: what defines "a type", except the
signatures of that subset of its interfaces that a given generic
component is actually using?  Presumably the programming-as-
contracting preconditions/postconditions/invariants on those
interfaces -- but those are *runtime*-checked, and even that
hardly catches a significant portion of the "type semantics".

Consider the issue of: what predicate-parameter P can I pass to
a generic such as C++'s std::sort.  Of course, I have some
signature constraints -- P(x,y) must be callable for certain
x and y and return something usable as a boolean value; C++
catches errors about this at compile-time, while Python, if
I try calling mylist.sort(unsuitableP) where unsuitableP is
not callable with two parameters that are items of mylist,
will only catch it at run-time.  Having the check happen at
compile-time gives me the error diagnostics slightly earlier
(5 to 10 minutes, if I use a sensible testing policy) AND
makes it easy for C++ to generate stupendous code (if P is
inline or can be inlined).

But that barely scratches the surface!  The REAL conditions
that define the type of P are:
    not P(x,x) for any x
    P(x, y) implies not P(y, x) for any x, y
    P(x, y) and P(y, z) implies P(x, z) for any x, y, z
Note the universal-quantifier 'any' liberally used here:
it's not something quaint and peculiar, it's TYPICAL of
real type-constraints, making them uncheckable in the
general case, even at runtime (much less compiletime).

THIS is the kind of thing I'd really like to express in a
compiler-usable way!  THIS is the kind of thing that would
make my programs MUCH clearer to human readers, and really
get mileage out of type-checking.  What, if anything, the
compiler is able to do with such a hypothetically formalized
expression of my real design intentions is a minor issue.

If *sometimes* a runtime check (or, joy!, even a compile
time one, saving me several precious extra minutes) can be
inferred from such type-constraints (maybe only in some
kind of debug-mode, if, as likely, checks would burden
the program), then great.  If *sometimes* the compiler is
able to optimize away some computation by *relying* on my
assertions, then super (maybe only in some kind of optimize
mode, if, as likely, it would slow down compilation a lot).

But existing languages appear to me to have things
backwards.  They *start* from what they'll be able to
check, and/or able to exploit for optimization, and
use THAT criterion to decide what subset of my design
intentions I'm allowed (or, more often, required) to
formally express in the language.

That's like the drunkard looking for his keys under
the streetlamp, even though he knows he's dropped them
at the other end of the road, because it's too dark
over there...:-).  A language should let me say what
I mean, and do of that what it can.  Compilers and
supporting tools do evolve, old applications tend to
live forever; basing what a language lets me express
(or forces me to express) on today's compiler and
tool technology is back-asswards.

Given the incomplete and unsatisfactory state of the
way various languages let me (or rather force me to)
express my design intentions, I'd rather do away with
all the complexity, and just use Python (or C++
templates).  Give me an URL to a usable language that
lets me express the most basic typing constraints,
such as symmetry or antisymmetry, reflexivity or
antireflexivity, and transitivity, as above, and I'll
be more than happy to give it a try.  But Ada, Eiffel,
C++ (what it DOES do for typechecking), Java, and,
sigh, even Haskell, don't really cut the mustard today.
Therefore, Python's *simplicity* wins the day, as
you say...:

"""
application areas, Python still wins hands down, though.
"""
I agree, but I hope you can now better see WHY I do
so fully agree.  Complication must bring a payoff that
offsets its undeniable costs.  Today's type-checking,
as applied in the above-listed languages, doesn't, in
terms of useful earlier-detection of errors -- it's
little use to find out about an error 10 minutes
earlier, if it takes me 15 more minutes to write the
code snippet because of extra language complication.
Most interesting checks happen at runtime if at all,
and in fact most important properties can't even be
stated formally in the languages, because of a lack
of existential and universal quantifiers.

Today's typechecks DO help hugely in terms of
optimization, even though Self, the Scheme compiler
stalin, and good Common Lisp compilers all prove
that static typing is nowhere near a NEED to get
such optimizations, that type inference even in
a hugely dynamic language can get there too.  But
C++'s generics are an excellent example of the way
lack of type-constraint declaration in no way
inhibits type-based optimization -- given signature
based polymorphism, type-inference in any actual
instantiation of a generic IS pretty trivial:-).


Alex