Typing system vs. Java

[Alex Martelli]

"Michael Abbott" <michael at rcp.co.uk> wrote in message
news:Xns90F19B5D37704michaelrcpcouk at 194.238.50.13...
> [posted and mailed]
>
> Alex, I'd like to say more in response to your very interesting message
> below, but it's difficult to know where to begin.  I agree wholeheartedly
> with your sentiments, but I'm wondering if you're aware of just how
> difficult what you're describing is to achieve!?

I suspect we may be talking at cross-purposes -- 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.

Surely it wouldn't be the first time a language let me express
design-intent aspects without committing any implementation of
the language to doing anything in particular about them!  Don't
you recall the 'register' keyword in C, for example?  Nowadays
compilers do their own register allocation -- but I still get to
express my design intent "and, I believe this thing here should
live in a register" to my heart's content.  Not much, as far
as expression design intentions goes, but, a start.  Similarly,
I recall BSD variants where my programs were ALLOWED to give
hints to the operating systems about their intentions wrt some
files or memory areas -- "I think I'll just read this file
right through" or "I'll jump up and down all over this file
in random-access so I don't think I would bother doing any
prefetch if I were you", and so on, and so forth.  Sometimes,
when reading such programs, such expressions of design intent
were illuminating, in ways that comments and other forms of
documentation rarely are.  And, hey, maybe SOME versions of the
system did/will take advantage of my design-hints, so, why not?

We may have gotten too focused on the imperative and declarative
to exploit the value of *design-intent hints*.  The assertions
I'd like to be able to make aren't just hints, but even if they
work like no more than that, I still think they'd be a pre-req
before one can state a language has types in a meaningful sense.

Eventually, 'checking modes' where some of the assertions were
partially checked (maybe just at runtime, maybe just during
some kinds of very thorough tests...), and 'optimizing modes'
where some of the assertions were relied upon for possible
optimizations (maybe just when compiling with "optimize all
you can please" flags), might emerge.  Automatic deductions
and inferences would be a potential further step.  But I think
the key step is the first one -- ALLOWING me to express those
design-intent constraints!  I won't pay a dime extra to be
able to say something pretty useless such as "I intend X to
be a list" (particularly because it's *NOT* what I _really_
should intend -- 'a mutable sequence', MAYBE:-); I might be
much better disposed could I express "I intend X to be a
mutable sequence with an odd number of items such that at
all times items with an even positive index are strictly
greater than either of their neighbors" -- now *THAT* is
what I'd call "typing".  (No, I wouldn't insist on THAT
being checked at compile-time... even checking it at RUN
time might be expensive enough that I'd be quite content
with only checking partially, and/or only when using certain
flags, if at all -- but my point is that, THIS is the kind
of things I find myself wishing I *COULD* usefully express,
*NOT* 'X is a list', 'Y is a complex', 'Z is a tuple of
float'... so, I think that for languages to claim they're
doing 'typing checks' for me, when such trivialities is all
they can or do check, violates truth in advertising!-).


Alex