Typing system vs. Java

[mcherm at destiny.com]

Alex Martelli writes:
> I don't request
> a language that will in fact absolutely CHECK assertions containing
> universal or existential quantifiers, nor one that will always be
> able to take advantage of them to further optimization or other
> type-inference goals: just one that will let me *express* such
> assertions simply, which, per se, isn't all that hard.

Alex, I strongly agree with your proposal that a language allow
the expression of assertions which are STRONGER than what the
language guarantees to deliver.

The closest thing I've found is programming by contract features
in Eiffel, but that's really not perfect. I've always felt that
this was something that "naturally" ought to be in a good 
language, but hardly ever encountered.

I'll give another example of how I think it could be used. In
Java's collection classes, or C++'s STL, there are several
different kinds of List. Some are array-based, some are linked-list
based others are for other special purposes. In contrast, Python
has just one kind of List (array based).

Now Python is pretty good, in that array-based lists are the
kind you want most often. But suppose you had a language in
which you could just declare Lists, and let the compiler worry
about which implementation to use. But you would have the OPTION
of specifying some things about the lists. For instance, you
might specify:
   list.willWriteTo('End': 1.0)
   list.willDelFrom('End': 1.0)
   list.willReadFrom('End': 0.90, 'Any': 0.10)
which would be a stack where we occasionally interrogate deeper
into the stack, or we could specify:
   list.willWriteTo('End': 0.8, 'Start': 0.2, 'Any': 0.0)
   list.willDelFrom('Start': 1.0, 'Any': 0.0)
   list.willReadFrom('Start': 1.0)
which is a priority queue. Or even something like this:
   list.willWriteTo('Any': 1.0)
   list.willDelFrom('Any': 0.0)
   list.willReadFrom('Sequenced': 1.0)
   list.isSorted()
where we will insert all over (keeping things sorted), but won't
ever do deletes, and only read from start to end.

Now a PROGRAMMER presented with these specifications (and please
forgive the clumsy form of these assertions... it could be
much improved) would use an array-based list for the first
senario, but possibly not for the second and definitely would
use a linked-list for the last. Compilers can't be as smart as
programmers, but this seems to me like a really useful paradigm.

After all, 90% of the time when you are using the list you really
don't care HOW it is implemented, you just want to use the list.
Only when you are considering the list itself do you want to
know (or care) how it is implented.

And if you're starting with something like Python, than you can
ONLY improve things... if the "hints" were implemented and then
ignored (always using array-list), then we'd be exactly where we
are right now, plus hints.


Anyway, I think that "compiler hints" are MORE useful in other
places (like invariants, preconditions, etc) which are more
useful overall and more easily ammenable to compile-time testing
or debug-version testing, but this is an additional application
of the concept that I just wanted to throw out there.

-- Michael Chermside