Typing system vs. Java

[Michael Abbott]

"Alex Martelli" <aleaxit at yahoo.com> wrote in
news:9kbpjj0kb at enews1.newsguy.com: 

> "Michael Abbott" <michael at rcp.co.uk> wrote in message
> news:Xns90F19B5D37704michaelrcpcouk at 194.238.50.13...
>>
>> 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.

Um.  But I don't see the point.  If the compilers going to ignore 
everything you write, then why not just put your assertions into comments?  
It's what we all have to do already!

> 
> 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. 

I always thought that compiler register allocation made the register 
keywork pointless.  Surely using this keyword is just noise now.

> 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?

Seems to me that there'd only be any point in putting such hints into your 
program if there was a chance that they'd have some concrete effect.  
Otherwise you might as well just write good comments, surely?

> 
> 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.  

Interesting idea.  So, our "high level abstract assertions" can be used in 
several ways:
1.  To supplement comments
2.  As a pious hope that the complier will check and validate them (fat 
chance!)
3.  As run time debug consistency checks
4.  To generate automated thorough tests
5.  As a stepping stone to the future

Hmm.  Well, for 1 I think we should write comments, and it seems we're 
agreed that 2 is implasible.  Of course, it sounds like you'd like an 
assertion language that is not fully amenable to 3 (after all, checking 
quantifiers can't necessarily be done in finite time), but I suppose we 
could expect that a compiler could make a stab at generating sensible 
tests.  Automatically generated tests is an interesting idea as well, and 
would be very handy: the abstract assertions could be used to guide the 
generation of tests.


> 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".

But what do you gain by writing all this in a formal language that's going 
to be quietly ignored by all your tools?  Why not just write good comments?


>  (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!-).

Oh, that's unfair!  After all, there is always a trade-off in type checking 
between the expressive power of the language being checked and how much 
checking is actually performed.