Why I don't believe in static typing
Erann Gat
We've been having so much fun having theological arguments about the
relative merits of static versus dynamic typing I thought I'd spoil it all
by introducing an actual data point.
Once upon a time I wrote a credit card billing system for a company which
shall remain nameless. The company's product was on-line advertising
delivered by an ad server, which was already up and running. (At the
time, the company only had corporate accounts, which were billed
manually.) The number of ads delivered was written to a database which
the biller that I wrote would periodically scan to generate invoices. The
invoices were then automatically charged to credit cards on file. The
entire process was fully automated.
During the initial development of the system I had a run-in with a
high-level manager at the company who opined that my dislike of Java and
C++ in favor of Lisp was irrational, that the static type systems provided
by these languages provided a powerful and reliable mechanism for
introducing incremental changes to a system, to wit: you'd make a change
to part of the system, compile it, and the compiler errors would point you
reliably to all the other parts of the system that required attention in
order to support that change. The introduction of credit card billing
required some changes to the ad server which were done more or less
following that methodology by a very bright and highly competent engineer
(not me).
The system was launched and had been happily humming along for a week or
two when all of a sudden it began to issue outrageously large charges -
millions of dollars in some cases - to people's credit cards.
Fortunately, sanity checks at the credit card processor prevented most of
these charges from going through, but a few did, and sorting out the
resulting mess took a very long time.
The proximate cause of the problem was quickly determined to be in the ad
server, which was suddenly claiming to have served vastly more ads than
was physically possible. But the ad server was old software. It had been
running for months with no problems. So there we were, facing this
critical problem in what had been a stable piece of software with no idea
how to even reproduce it, let alone track it down.
To make a long story short, what happened was this: when an ad-server shut
down, part of the shut-down code did a final update of the database to
record all the ads that had been served since the last update before the
shut-down. But the ad-server was multi-threaded, and it turned out that
there was a race condition. The thread that did the final database update
used data structures whose destructors were being run in a different
thread. Kablooey.
I can no longer recall whether the changes made to support credit card
billing actually introduced the race condition or just changed the timing
so that a problem that had actually been there all along began to manifest
itself, but it doesn't matter. The point is this: the more kinds of
errors are flagged for you at compile time, the more you can get lulled
into a sense of complacency and start to believe that if a program
compiles without errors then it is actually free of bugs. This is
especially true if you are using a language that doesn't allow you to run
your program at all until you have eliminated all the errors that the
compiler could find. After all, it is not unreasonable to expect that all
the work required just to get the program to compile so you could run it
for the first time should pay a dividend of some sort, and what else could
that dividend possibly be other than having to do less testing?
So it is not at all clear to me that eliminating even a certain class of
run-time errors actually has net positive utility. The real payback from
compile-time detection of type errors is not a reduced necessity for
testing; it is instead merely a time savings, finding those errors sooner
rather than later. And if one does allow onesself to be deluded into
thinking that static typing does pay a dividend in reduced testing then
static typing could actually have a negative net benefit when the laws of
physics and mathematics come around to remind you that you were wrong.
E.
Barry Margolin
Erann Gat <g...@jpl.nasa.gov> wrote:
>I can no longer recall whether the changes made to support credit card
>billing actually introduced the race condition or just changed the timing
>so that a problem that had actually been there all along began to manifest
>itself, but it doesn't matter. The point is this: the more kinds of
>errors are flagged for you at compile time, the more you can get lulled
>into a sense of complacency and start to believe that if a program
>compiles without errors then it is actually free of bugs.
Well, if you have incompetent programmers, no language can really solve
that problem. I've used static-typed languages and dynamic-typed
languages, and they each have their pros and cons. I've never known a
decent programmer who assumed that the only kinds of errors are the ones
that the compiler can detect.
Compilers can generally only detect some really simple, stupid errors like
misspelling variable names or changing a type in one place without changing
it in others. Semantic errors like the one that caused your problem are
clearly beyond the abilities of any compiler to detect, and you have to do
exhaustive testing to verify things at this level.
Blaming this failure on the language is really barking up the wrong tree.
--
Barry Margolin, barry.m...@level3.com
Level(3), Woburn, MA
*** DON'T SEND TECHNICAL QUESTIONS DIRECTLY TO ME, post them to newsgroups.
Please DON'T copy followups to me -- I'll assume it wasn't posted to the group.
Thant Tessman
[...]
> During the initial development of the system I had a run-in with a
> high-level manager at the company who opined that my dislike of Java and
> C++ in favor of Lisp was irrational, that the static type systems provided
> by these languages provided a powerful and reliable mechanism for
> introducing incremental changes to a system, [...]
There ought to be some sort of comp.lang FAQ entry explaining that no
advocate of static type systems will ever take any defense of latent
typing seriously if it mentions C++ or Java.
-thant
Arthur Lemmens
> The real payback from compile-time detection of type errors is not
> a reduced necessity for testing; it is instead merely a time savings,
> finding those errors sooner rather than later.
Actually, finding errors sooner rather than later is not always an
advantage.
There's one big advantage to finding errors at run-time rather than
compile-time: you can get a lot more information about the situation
that caused the error. Any decent debugger will let you inspect the
entire sequence of events, i.e. function calls and arguments, that
led to the error. You get an actual, real-life, fully worked out
*example* of your thinking mistake, not just a type-mismatch error
(which can sometimes be very cryptic, in my experience). It's hard
to overestimate the value of a good example.
(Obviously, finding errors at run-time rather than compile-time has
its disadvantages too.)
Arthur Lemmens
Erann Gat
<barry.m...@level3.com> wrote:
> In article <gat-171103...@k-137-79-50-101.jpl.nasa.gov>,
> Erann Gat <g...@jpl.nasa.gov> wrote:
> >I can no longer recall whether the changes made to support credit card
> >billing actually introduced the race condition or just changed the timing
> >so that a problem that had actually been there all along began to manifest
> >itself, but it doesn't matter. The point is this: the more kinds of
> >errors are flagged for you at compile time, the more you can get lulled
> >into a sense of complacency and start to believe that if a program
> >compiles without errors then it is actually free of bugs.
>
> Well, if you have incompetent programmers, no language can really solve
> that problem.
But that's just the thing: this wasn't a case of programmer incompetence.
The person who made the changes to the ad server that resulted in the
problem was very smart, very competent. (You may say that the fact that
this problem arose is de facto evidence that he was not competent, but
after the problem occurred it took a whole team of engineers a week to
figure out what was going on. That whole team would have had to have been
incompetent, and I assure you they were not. These were the cream of the
crop.)
> Blaming this failure on the language is really barking up the wrong tree.
You have badly misunderstood my point. I do not blame this failure on the
language. I blame this failure on the mindset that because the compiler
catches certain kinds of errors that you can get away with less testing
than if it didn't. In other words, I am not saying static typing is bad,
just that one of the benefits that many people cite for it is not really a
net benefit.
E.
Thant Tessman
> [...] I do not blame this failure on the
> language. I blame this failure on the mindset that because the compiler
> catches certain kinds of errors that you can get away with less testing
> than if it didn't. In other words, I am not saying static typing is bad,
> just that one of the benefits that many people cite for it is not really a
> net benefit.
I've heard exactly this argument used to defend manual memory management
over GC.
-thant
Barry Margolin
And I'm saying that that mindset is an indication of poor programming
skill. If your cream of the crop thinks like that, you need to find a
better crop. Extensive testing is always necessary, especially in
multi-threaded applications -- timing holes are notoriously transient and
difficult to detect.
Adrian Hey
> After all, it is not unreasonable to expect that all
> the work required just to get the program to compile so you could run it
> for the first time should pay a dividend of some sort,
I'm still baffled by what this extra work that you (and a few others like
Raffael and Pascal) keep refering to actually is. So maybe you could
illustrate what extra work your talking about if we chose a specific
example we are both familiar with, the phonecodes problem. I posted
a Haskell solution which you can dig out of the google if you like.
How do you think the presence of a static type system impeded development
of this program?
The only extra work I can think of is that a static type system does
force you to give some thought to correctness as you write your
code. But anybody who doesn't do that as a matter of routine is
storing up a heap of trouble for themselves further down the line.
> and what else could that dividend possibly be other than having to do less
> testing?
For non-trivial programs testing will never prove correctness. The best
you can hope for is that more testing will raise the probability that
a program which passes all its tests is indeed correct. So static typing
does not reduce the amount of testing you *need* to do (which is infinite
if you like). But for a given finite test time/effort static typing will
improve test coverage (testing for certain properties which are a
necessary but not sufficient condition for correctness is 100% and
comes for free). So it will raise the probability of correctness IMO.
Also, detection of a fault and diagnosis are not the same thing at all.
In my testing I often detect bugs hours before I diagnose the cause and
fix it. In contrast, those bugs detected by the static type system are
pinpointed imediately (well almost, once I've grocked the error message
thrown out by the compiler).
Regards
--
Adrian Hey
Dirk Thierbach
> But the ad-server was multi-threaded, and it turned out that
> there was a race condition.
Nobody expects static typing to guard against race conditions.
> The point is this: the more kinds of errors are flagged for you at
> compile time, the more you can get lulled into a sense of
> complacency and start to believe that if a program compiles without
> errors then it is actually free of bugs.
The same goes for unit tests: Even if you have quite a lot of them,
you probably would have been lucky if they caught the race condition.
You guard against race conditions by careful programming, and by
planning in advance. Modelling the interaction of the threads is also
helpful, but requires some effort.
No matter what tools you use, you should know what you can expect
from them. So the "data point" you gave is irrelevant for static vs.
dynamic typing.
- Dirk
Matthias Blume
> Erann Gat <g...@jpl.nasa.gov> wrote:
>
> > But the ad-server was multi-threaded, and it turned out that
> > there was a race condition.
>
> Nobody expects static typing to guard against race conditions.
Why not?
http://citeseer.nj.nec.com/boyapati01parameterized.html
> > The point is this: the more kinds of errors are flagged for you at
> > compile time, the more you can get lulled into a sense of
> > complacency and start to believe that if a program compiles without
> > errors then it is actually free of bugs.
>
> The same goes for unit tests: Even if you have quite a lot of them,
> you probably would have been lucky if they caught the race condition.
In fact, static analysis (although perhaps not in form of type
systems) is your best (some may say: only) bet against the possibility
of race conditions and their ilk.
Jesse Tov
> Nobody expects static typing to guard against race conditions.
I would be very surprised if no one were working on precisely this.
Jesse
Ray Blaak
> > Blaming this failure on the language is really barking up the wrong tree.
>
> You have badly misunderstood my point. I do not blame this failure on the
> language. I blame this failure on the mindset that because the compiler
> catches certain kinds of errors that you can get away with less testing
> than if it didn't. In other words, I am not saying static typing is bad,
> just that one of the benefits that many people cite for it is not really a
> net benefit.
Race conditions and deadlocks can occur readily in either static or dynamic
languages.
If the programmer's mindset leads them to believe that concurrency issues
cannot occur just because things compile, then they are indeed incompetent, at
least with regards to concurrency.
They can be outrageously smart in other areas, but forgetting about
concurrency issues is a mistake, plain and simple.
I would imagine that after the mistake you describe, your smart programmer was
quite a bit smarter.
I would also imagine that your programmer's opinion of static typing is in no
way affected by the incident either.
--
Cheers, The Rhythm is around me,
The Rhythm has control.
Ray Blaak The Rhythm is inside me,
rAYb...@STRIPCAPStelus.net The Rhythm has my soul.
Erann Gat
<ah...@NoSpicedHam.iee.org> wrote:
> Erann Gat wrote:
>
> > After all, it is not unreasonable to expect that all
> > the work required just to get the program to compile so you could run it
> > for the first time should pay a dividend of some sort,
>
> I'm still baffled by what this extra work that you (and a few others like
> Raffael and Pascal) keep refering to actually is. So maybe you could
> illustrate what extra work your talking about if we chose a specific
> example we are both familiar with, the phonecodes problem. I posted
> a Haskell solution which you can dig out of the google if you like.
> How do you think the presence of a static type system impeded development
> of this program?
I can't really speak to this because I don't know Haskell. But the
episode in question involved C++. And in the case of ML the extra work
involves things like changing all you arithmetic operations if you decide
to change an int to a float.
> The only extra work I can think of is that a static type system does
> force you to give some thought to correctness as you write your
> code.
No, it only forces you to give some thought to a particular kind of
correctness, which may or may not be a kind that actually matters to you.
That's the whole point.
E.
William D Clinger
Ringo Starr
Raffael Cavallaro
> The only extra work I can think of is that a static type system does
> force you to give some thought to correctness as you write your
> code.
By "thought to correctness" you really mean, thinking in a type system,
an additional burden I don't want to take on, especially for such little
benefit - virtually all of these type errors will be caught by other
necessary testing.
> But anybody who doesn't do that as a matter of routine is
> storing up a heap of trouble for themselves further down the line.
No, they are storing up failed tests and runtime exceptions, which lead
to corrections.
I wan't to run my program at any stage, knowing that it isn't fully
correct yet, and ignore those errors I choose to, and attend to those I
want to, when I want to. I don't wan't the compiler dictating the order
in which I must move my program toward correctness (i.e., fix the type
errors *first* or I won't let your program run). Type errors aren't all
that important to me, since I know they'll either be caught in other
necessary testing, or disappear as my code is refined and refactored.
> So maybe you could
> illustrate what extra work your talking about if we chose a specific
> example we are both familiar with, the phonecodes problem. I posted
> a Haskell solution which you can dig out of the google if you like.
> How do you think the presence of a static type system impeded development
> of this program?
This is tantamount to asking us to retroactively get inside your head
and know everything that you were doing and thinking from the time you
first read the spec, to the time your program compiled and tested
correctly. The extra work is having to conform your thought about the
problem to Haskell's type system, and being forced to correct any type
errors before your program is allowed to run. This extra work isn't
going to be visible in the finished code any more than the initial list
based, throw away drafts of a lisp solution would be visible in a final
program that uses CLOS or hash tables.
Erann Gat
<dthie...@gmx.de> wrote:
> Erann Gat <g...@jpl.nasa.gov> wrote:
>
> > But the ad-server was multi-threaded, and it turned out that
> > there was a race condition.
>
> Nobody expects static typing to guard against race conditions.
Not consciously, no. But tacitly, yes, I think people do expect this,
even if they don't realize it.
> You guard against race conditions by careful programming, and by
> planning in advance.
Or by putting in run-time sanity checks. If I had had the foresight and
the strength of my own convictions I would have put code into the biller
that stopped the billing process immediately as soon as a request was made
to bill a ridiculously high amount, for some value of "ridiculously
high". That would have solved the problem too.
Neither static nor dynamic typing would have helped in this situation.
But I do believe that a dynamic typing *mindset* would have been more
likely to produce a correct solution because it encourages you to think
more about possible run-time errors.
E.
Erann Gat
<fi...@my.address.elsewhere> wrote:
> In fact, static analysis (although perhaps not in form of type
> systems) is your best (some may say: only) bet against the possibility
> of race conditions and their ilk.
Ironically, I actually agree with this.
E.
Erann Gat
<rAYb...@STRIPCAPStelus.net> wrote:
> g...@jpl.nasa.gov (Erann Gat) writes:
> > > Blaming this failure on the language is really barking up the wrong tree.
> >
> > You have badly misunderstood my point. I do not blame this failure on the
> > language. I blame this failure on the mindset that because the compiler
> > catches certain kinds of errors that you can get away with less testing
> > than if it didn't. In other words, I am not saying static typing is bad,
> > just that one of the benefits that many people cite for it is not really a
> > net benefit.
>
> Race conditions and deadlocks can occur readily in either static or dynamic
> languages.
>
> If the programmer's mindset leads them to believe that concurrency issues
> cannot occur just because things compile, then they are indeed incompetent, at
> least with regards to concurrency.
The situation was that the programmer was making what appeared outwardly
to be a minor change to a piece of code that had run for months in a
production environment with no problems. No one imagined that this
problem would happen. Even after it happened, as I said, it took the
entire team the better part of a week to figure out what had gone wrong.
> I would imagine that after the mistake you describe, your smart programmer was
> quite a bit smarter.
Well, they're still using C++ so I don't know ;-)
> I would also imagine that your programmer's opinion of static typing is in no
> way affected by the incident either.
That is probably true. Certainly the manager who insisted I write the
biller in Java was unmoved.
E.
Artie Gold
> I'm certain that it happens all the time.
>
> Ringo Starr
Ringo sang it. But it was a Lennon/McCartney composition.
[If I read one of your papers out loud, can I take the credit?
Please? ;-) ;-)]
--ag
--
Artie Gold -- Austin, Texas
Oh, for the good old days of regular old SPAM.
Matthias Blume
Rayiner Hashem
those who use the type system as a mental crutch to avoid reasoning
about the code. The comment about changing a type and then having the
compiler tell you where you need to make modifications made me cringe.
That's an abuse of the type system, not a good way to take advantage
of it! Of course, dynamic typing would not have helped in your case.
Only proper testing and code review would have.
Static typing will tell you exactly one thing --- that your code is
free of type errors. It has its utility --- it means that, if your
code typechecks correctly, you don't have to pay attention to looking
for type errors, rather, you can spend your efforts (testing, code
review time) looking for other sorts of errors. People who sell static
typing as a panacea (like anybody who sells anything as a panacea) are
selling you snake oil.
Alain Picard
> Neither static nor dynamic typing would have helped in this situation.
> But I do believe that a dynamic typing *mindset* would have been more
> likely to produce a correct solution because it encourages you to think
> more about possible run-time errors.
Well, I quite liked your story, and in my experience the
sort of error you relate is absolutely typical.
What I also find interesting about this episode is, at
the meta level, that you got the responses I expected
right away:
* the programmers were incompetent (shoot the messenger)
* That's not a typing issue, it's a concurrency issue (head in the sand).
* refusal to learn from the experience (from your managers/team).
I would almost go so far as to say that KNOWING you're going
to get errors at runtime is BETTER, because it leads to safer/more
robust designs. Your programmer _knows_ he might have missed a
call path, and will think about where/how to handle those missed
errors, even if it's just to log the bug and continue in some sane
state.
An interesting war story. Thanks.
Joe Marshall
> Dirk Thierbach <dthie...@gmx.de> writes:
>>
>> Nobody expects static typing to guard against race conditions.
>
Matthias Blume <fi...@my.address.elsewhere> writes:
> Why not?
>
> http://citeseer.nj.nec.com/boyapati01parameterized.html
>
> In fact, static analysis (although perhaps not in form of type
> systems) is your best (some may say: only) bet against the possibility
> of race conditions and their ilk.
Great. I agree with you.
--
~jrm
Joe Marshall
> Static typing will tell you exactly one thing --- that your code is
> free of type errors. It has its utility --- it means that, if your
^
static
> code typechecks correctly, you don't have to pay attention to looking
> for type errors, rather, you can spend your efforts (testing, code
^
static
> review time) looking for other sorts of errors.
Like the dynamic type errors.
--
~jrm
Matthias
> Dirk Thierbach <dthie...@gmx.de> writes:
>
> > Erann Gat <g...@jpl.nasa.gov> wrote:
> >
> > > But the ad-server was multi-threaded, and it turned out that
> > > there was a race condition.
> >
> > Nobody expects static typing to guard against race conditions.
>
> Why not?
>
> http://citeseer.nj.nec.com/boyapati01parameterized.html
There is also a technique in C++ which uses the type system and the
volatile keyword to guard against race conditions. I haven't used the
technique myself, so I don't know about benefits and problems. But it
sounds reasonable and might be of practical value. The technique
really relies on the language being statically typed.
One article describing it is here (sorry for the long URL):
> > The same goes for unit tests: Even if you have quite a lot of them,
> > you probably would have been lucky if they caught the race condition.
>
> In fact, static analysis (although perhaps not in form of type
> systems) is your best (some may say: only) bet against the possibility
> of race conditions and their ilk.
The reason for this is that in a multithreaded environment you would
have to check an /exponential/ number of "different" programs (because
the scheduling might switch threads after each operation, in effect
creating a different control flow each time). IMHO, there is no
chance to fix a race condition in a moderately complex multithreaded
program by unit testing. (Note: I am /not/ saying a multithreaded
program shouldn't be unit-tested!)
Dirk Thierbach
> Dirk Thierbach <dthie...@gmx.de> writes:
>> Nobody expects static typing to guard against race conditions.
> Why not?
[...]
> In fact, static analysis (although perhaps not in form of type
> systems)
Because it's static analysis, and not a static type system.
> is your best (some may say: only) bet against the possibility
> of race conditions and their ilk.
Yes. I know.
- Dirk
Dirk Thierbach
> In article <h6sn81-...@ID-7776.user.dfncis.de>, Dirk Thierbach
> <dthie...@gmx.de> wrote:
>> Nobody expects static typing to guard against race conditions.
> Not consciously, no. But tacitly, yes, I think people do expect this,
> even if they don't realize it.
So you say you don't believe in static typing because you have met
people who are stupid? Come on, you cannot be serious. That would
be like saying that I don't believe that dynamic typing can work
because I have seen people who treat it as a religion.
> Neither static nor dynamic typing would have helped in this situation.
> But I do believe that a dynamic typing *mindset* would have been more
> likely to produce a correct solution because it encourages you to think
> more about possible run-time errors.
You seem to have some strange ideas about a "static typing mindset".
I believe you that you have met incompetent people who were using
static typing, but they are also incompetent people who are using
dynamic typing. That really proves nothing.
And in this case, a static analysis (not a static type system) will
probably buy you much more, so some "static" thinking doesn't hurt.
- Dirk
Dirk Thierbach
> The comment about changing a type and then having the
> compiler tell you where you need to make modifications made me cringe.
> That's an abuse of the type system, not a good way to take advantage
> of it!
Why? Types encode invariants. They form a contract about the behaviour
of some part of my code. If I break this contract in such a way that
it changes the type, the type checker *will* point out all places
I have to think about. (Of course, if I change it in a way that keeps
the type, I have to do testing and code review).
> Only proper testing and code review would have.
But static typing *does* testing by abstract interpretation. And it
does this more thoroughly than any test suite or code review ever
can, because it is automated.
> People who sell static typing as a panacea (like anybody who sells
> anything as a panacea) are selling you snake oil.
Yes. Nobody tries to sell static typing as a panacea. (Though I
sometimes got the impression that people were trying to sell dynamic
typing as one). Static typing is a great tool, nothing more. It has
its limits, but within those limits, it is really helpful.
- Dirk
Dirk Thierbach
> What I also find interesting about this episode is, at
> the meta level, that you got the responses I expected
> right away:
> * the programmers were incompetent (shoot the messenger)
> * That's not a typing issue, it's a concurrency issue (head in the sand).
> * refusal to learn from the experience (from your managers/team).
Excuse me, so you're saying that if A claims he had an accident
on his way to work because you saw a black cat passing from left
to right, and if B points out that the black cat has nothing to
do with it, then B is automatically wrong? Come on.
> I would almost go so far as to say that KNOWING you're going
> to get errors at runtime is BETTER, because it leads to safer/more
> robust designs.
Yes, it is. With a static type system, you not even know that you're
going to get errors at runtime, you have a good idea about *what*a
kinds of errors you're going to get, and what kinds of errors
never won't happen.
- Dirk
Andreas Rossberg
>
> There's one big advantage to finding errors at run-time rather than
> compile-time: you can get a lot more information about the situation
> that caused the error.
No, you get different information. Static analysis can infer global
information that won't be available during runtime, where you just look at
one execution path at a time.
That's why should have both.
- Andreas
--
Andreas Rossberg, ross...@ps.uni-sb.de
"Computer games don't affect kids; I mean if Pac Man affected us
as kids, we would all be running around in darkened rooms, munching
magic pills, and listening to repetitive electronic music."
- Kristian Wilson, Nintendo Inc.
Andreas Rossberg
>
> I can't really speak to this because I don't know Haskell. But the
> episode in question involved C++. And in the case of ML the extra work
> involves things like changing all you arithmetic operations if you decide
> to change an int to a float.
Not in Standard ML.
Tayss
> After all, it is not unreasonable to expect that all
> the work required just to get the program to compile so you could run it
> that dividend possibly be other than having to do less testing?
"Compile time" -- what does this mean, the time when macros are
expanded?
Seriously, I can not imagine in this new millenium, that static
checking proponents are still talking about compile time. You must
have a bad assumption in your posting; perhaps you are explaining the
very real problem of how local fixes to satisfy a static system end up
damaging code globally.
So I'd ask: Could a lisp system be configured so that it runs a
static analysis upon runtime errors, or at arbitrary points on
arbitrary subsets of code? In fact, if the user is allowed to
incrementally supply type information, it can ask for specific info to
make certain guarantees. It may even be combined with runtime
analysis to recommend exactly which types and where they are most
sorely needed.
Joachim Durchholz
>
> You have badly misunderstood my point. I do not blame this failure on the
> language. I blame this failure on the mindset that because the compiler
> catches certain kinds of errors that you can get away with less testing
> than if it didn't. In other words, I am not saying static typing is bad,
> just that one of the benefits that many people cite for it is not really a
> net benefit.
Non sequitur.
Static typing didn't catch the error - no surprise here, nobody in his
right mind would claim that. (That manager who said that static typing
would tell you all the places where to change the code obviously
over-generalized - only if a change affects the signature of a function
does static typing help spotting the other affected places; the race
condition obviously wasn't of that error class.)
Being lulled into a false sense of security can happen with /any/
testing method, be it unit tests, static typing, black-box testing, or
whatever. One should apply all available test methods and not rely on
just one.
Given the reasoning of the previous paragraph, I draw the exactly
reverse conclusion: Removing a test method increases the likelihood that
a given bug will slip through.
So here's my litmus test for language testability:
Does it enable as many test paradigms as possible?
Lisp doesn't qualify, it makes static testing (type checking, automatic
proving) difficult, as it gives very little easily verifiable guarantees
what a given piece of code does.
C++ doesn't qualify: no introspection and a syntax that requires several
months from a highly qualified expert to write a useful parser, so tools
that inspect the code have a hard time. On top of that, a highly
complicated semantics that makes analyzing the code even more difficult.
Java sort-of qualifies: its introspection facilities give tools a
foothold that they can work with. However, its type system is too weak:
as soon as containers come into play, it fails to give the guarantees
that the programmer knows could be given (every single type cast is such
a failed guarantee).
Note that even when Java acquires parametric classes (scheduled for this
year IIRC), its type system will remain too weak: parallel type
hierarchies (e.g. Driver and Vehicle, the problem is with the drive()
routine in the, say, Ship/Captain subclasses) will continue to require
type casts. This is a typical problem of most if not all statically
typed OO languages.
Typical functional languages with static typing sort-of qualify from the
other side: they usually have an extremely regular syntax and semantics,
so writing tools (including testing tools) should be comparatively easy,
so they /should/ qualify; however, these tools often aren't present (or
they don't get the high visibility that they deserve, I don't know), so
for me, they fall a bit short of their potential.
Regards,
Jo
Joachim Durchholz
>
> I can't really speak to this because I don't know Haskell. But the
> episode in question involved C++. And in the case of ML the extra
> work involves things like changing all you arithmetic operations if
> you decide to change an int to a float.
That's of of the least common types of change that I have met in my life
(with the exception of school examples where this can indeed happen).
The type of changes that I usually see are a change in the fields of a
data structure, or replacing a data structure with a slightly different
one. Static typing will not require me to rewrite all the code where the
semantics has remained unchanged. (Static typing without inference will
require me to needlessly rewrite the routine signatures such as
"f (foo: BAR)" if the type of foo changes to BAZ, and f just passes the
value through to other functions without actually inspecting it. Which
is what I see in type inference - I've been spending too many hours
twiddling function signatures.)
Regards,
Jo
Arthur Lemmens
> No, you get different information. Static analysis can infer global
> information that won't be available during runtime, where you just
> look at one execution path at a time.
>
> That's why should have both.
Definitely. Getting static type *information* is great. But getting an
impenetrable static type *barrier*, that won't let you run a program
just because it might cause a type error at run-time, is not so great.
It makes it more difficult to explore many paths in the search space from
ideas to useful programs.
Arthur Lemmens
Adam Warner
> I can't really speak to this because I don't know Haskell. But the
> episode in question involved C++. And in the case of ML the extra work
> involves things like changing all you arithmetic operations if you
> decide to change an int to a float.
This lack of explicitness is a weakness in Common Lisp and a potential
source of inaccuracy. It arises whenever integer to float conversion must
be more precise than single floating point arithmetic and it can be really
hard to spot the inaccuracy within a series of computations.
Specifically the problem is with automatic single- to higher-float
contagion which the rules make difficult to spot.
(values #1=(loop for i in '(2 3 5 7 11) sum (* pi (sqrt i))) (type-of #1#))
=> 35.640452700666685
double-float
Here I've been lulled into the false belief that calculations have been
performed to double-floating point accuracy. But SQRT returned single
floats. It is PI that lead to the double float contagion.
Here's the correct level of accuracy provided by a double-float:
(values #1=(loop for i in '(2d0 3d0 5d0 7d0 11d0) sum (* pi (sqrt i))) (type-of #1#))
=> 35.64045272006214
double-float
Here's the more realistic level of accuracy that was computed in the
original example:
(values #1=(loop for i in '(2 3 5 7 11) sum (* (coerce pi 'single-float)
(sqrt i))) (type-of #1#))
=> 35.640453f0
single-float
Hidden contagion would not be a problem if floats of different formats
lead to contagion to the float of a lower level of accuracy. If a
single-float appeared in a series of double-float calculations the outcome
would be a single-float and the fix would be to locate the source of the
contagion. As it stands a programmer may be none the wiser when half the
precision is thrown away at some point--or potentially worse if the
implementation supports even higher levels of floating point precision:
(loop for i in '(2 3 5 7 11) sum (* pi (sqrt i)))
=> 35.64045270066668789L0 in CLISP in ANSI Common Lisp mode. CLISP warns:
WARNING:
Floating point operation combines numbers of different precision. See ANSI
CL 12.1.4.4 and the CLISP impnotes for details. The result's actual
precision is controlled by *floating-point-contagion-ansi*.
To shut off this warning, set *warn-on-floating-point-contagion* to nil.
Regards,
Adam
Joachim Durchholz
> Adrian Hey <ah...@NoSpicedHam.iee.org> wrote:
>
>> The only extra work I can think of is that a static type system
>> does force you to give some thought to correctness as you write
>> your code.
>
> By "thought to correctness" you really mean, thinking in a type
> system, an additional burden I don't want to take on, especially for
> such little benefit - virtually all of these type errors will be
> caught by other necessary testing.
If you say "type", you think Integer, Real, or some record type.
Functional data types are (mostly) variant records (similar to Pascal,
but type-safe: the type used is encoded, and the language will not allow
you to reinterpret memory bits by assuming the wrong type).
The "thought to correctness" is thinking which data should go in what
records, what functions should operate on them, what these functions can
assume and what they cannot. Designing your data structures has a
profound effect on program correctness (a phenomenon that functional
programming shares with OO).
> I wan't to run my program at any stage, knowing that it isn't fully
> correct yet, and ignore those errors I choose to, and attend to those
> I want to, when I want to.
You're not making a case for dynamic typing here. You're making a case
for classifying type errors as warnings. (Which isn't unreasonable in my
eyes, even though I don't adhere to this style of coding - but hey,
people are different and ought to be.)
> The extra work is having to conform your thought about the problem to
> Haskell's type system, and being forced to correct any type errors
> before your program is allowed to run. This extra work isn't going to
> be visible in the finished code any more than the initial list based,
> throw away drafts of a lisp solution would be visible in a final
> program that uses CLOS or hash tables.
Static checking forces one's attention to some class of errors (namely
whatever errors the type system happens to be able to exclude). I agree
that this can be annoying, and sometimes it can force attention away
from the real issues (particularly when you're refactoring large
libraries, as I did).
I'd rate the importance as somewhere in the middle between "important"
and "irrelevant".
It would be easy to handle: turn type errors into warnings, and have the
compiler insert exception-throwing code in places where the type error
would cause problems. (And, probably, add compiler flags that make type
errors and - possibly - other diagnostics into errors if that's the
policy for the shop in question.) That way, you'd get the best of both
worlds: precise information on those errors that the machine can
diagnose, and an example at run-time where you can actually inspect the
values if the general diagnosis was uninterpretable. (I don't think that
having examples at run-time is too helpful for the seasoned programmer,
but it could be a tremendous help when learning to work with static type
inference. Every fall, comp.lang.functional resounds with lots of pleas
for help interpreting a type error message, so there's certainly a case
here.)
Regards,
Jo
Pascal Costanza
> So here's my litmus test for language testability:
> Does it enable as many test paradigms as possible?
>
> Lisp doesn't qualify, it makes static testing (type checking, automatic
> proving) difficult, as it gives very little easily verifiable guarantees
> what a given piece of code does.
[...]
> Java sort-of qualifies: its introspection facilities give tools a
> foothold that they can work with.
[...]
A question for understanding: What makes you think that Java's
introspective features are better suited than Lisp's?
(Note: When you refer to "Lisp", in c.l.l this typically means Common
Lisp and Scheme. Noone is using LISP anymore as it was defined until,
roughly, the end of the 70's.)
Pascal
--
Pascal Costanza University of Bonn
mailto:cost...@web.de Institute of Computer Science III
http://www.pascalcostanza.de Römerstr. 164, D-53117 Bonn (Germany)
Joachim Durchholz
>
> Or by putting in run-time sanity checks. If I had had the foresight and
> the strength of my own convictions I would have put code into the biller
> that stopped the billing process immediately as soon as a request was made
> to bill a ridiculously high amount, for some value of "ridiculously
> high". That would have solved the problem too.
At the point where you'd like to put in the sanity checks, you usually
don't have the information that allows you to decide what's
"ridiculously high" and what isn't. For some site, an amount in excess
of 10.000$ would have been ridiculous, others might really have to pay
millions.
Actually, some of the bogus payments were actually caught, so this was
already being done. Maybe these checks could have been improved - but I
think they would also have obscured the original problem: instead of a
race condition, you'd have seen bills sometimes being sent and sometimes
not. The problem would have had roughly the same amount, it would just
have been extended over a longer time (if the billing system had worked
correctly, managers wouldn't have sent an entire team of expensive
people working on the problem, so it would have persisted far, far
longer, with the effect that the trust in the billing system would have
slowly eroded over months until somebody had finally decided to send a
fire squad in - the financial loss for the company would have reached
the same order of magnitude, in the form of disgruntled customers going
elsewhere, and more difficult to assess).
Regards,
Jo
Joachim Durchholz
There is no such thing as a dynamic type error. Not in a
statically-typed language.
Unless you count type casts in. Type-inferring languages like ML or
Haskell don't even have them though - they are unnecessary. (Well, you
can always do a type cast by going through C, which would be excessively
awkward. The important point being: there was never pressure from the
language users to add a more convenient way to do type casts.)
Regards,
Jo
Tayss
the code tool #'analyze. No need for Franz or other compiler vendor
to implement this, perfectly voluntary.
Rich & Shrobe's "Initial Report on a LISP Programmer's Apprentice"
(1978) talks a bit about an ambitious superset of this. (In fact,
they mention Floyd's work on this, whom I remember acknowledged you in
a book, Erann, about the color of lunch trays or something. ;)
g...@jpl.nasa.gov (Erann Gat) wrote in message news:<gat-171103...@k-137-79-50-101.jpl.nasa.gov>...
> So it is not at all clear to me that eliminating even a certain class of
> run-time errors actually has net positive utility.
Andreas Rossberg
>
> Getting static type *information* is great. But getting an
> impenetrable static type *barrier*, that won't let you run a program
> just because it might cause a type error at run-time, is not so great.
> It makes it more difficult to explore many paths in the search space from
> ideas to useful programs.
OTOH, erecting barriers of one kind or the other is the only way to
*localise* (confine) errors.
Vincenzo aka Nick Name
> The real payback from
> compile-time detection of type errors is not a reduced necessity for
> testing; it is instead merely a time savings, finding those errors
> sooner rather than later.
Well, there's also the fact that when you give a type to a term you have
a proof, and when you give a series of tests about the type of a term
you have a good probability, but not the rigorous proof, that those
errors won't come up. So besides the time savings there's something
more. Maybe I am ingenuous, because it's impossible that this argument
hasn't yet been told :)
V.
Joachim Durchholz
> Joachim Durchholz wrote:
>
>> So here's my litmus test for language testability: Does it enable
>> as many test paradigms as possible?
>>
>> Lisp doesn't qualify, it makes static testing (type checking,
>> automatic proving) difficult, as it gives very little easily
>> verifiable guarantees what a given piece of code does.
>
> [...]
>
>> Java sort-of qualifies: its introspection facilities give tools a
>> foothold that they can work with.
>
> [...]
>
> A question for understanding: What makes you think that Java's
> introspective features are better suited than Lisp's?
Lisp makes it far easier to access the definitions of data types and
functions, but interpreting the definitions is far more difficult
because it imposes far less restrictions on what the individual
definitions actually do. (It's the downside of unrestricted power.)
I fear I didn't make clear enough that I was talking about testing &
verification in a fully automated manner, particularly the automation of
test case selection.
> (Note: When you refer to "Lisp", in c.l.l this typically means Common
> Lisp and Scheme. Noone is using LISP anymore as it was defined
> until, roughly, the end of the 70's.)
That's understood.
Actually I'm not even talking about the standard Lisps of the '80ies
(which were Interlisp and its likes; Scheme and CL had just started to
interest Lisp programmers in general, at least here in Europe).
Regards,
Jo
Joachim Durchholz
>
> Seriously, I can not imagine in this new millenium, that static
> checking proponents are still talking about compile time.
Come on. 99% of all programmers still work with compilers. (This doesn't
make working with compilers superior, it just defines the standard case
from which people tend to argue. Abstract that away when weighing
arguments.)
> So I'd ask: Could a lisp system be configured so that it runs a
> static analysis upon runtime errors, or at arbitrary points on
> arbitrary subsets of code?
I'd prefer the latter: static checking when I want it.
Checking upon runtime errors is better than nothing, but checking before
the software hits the end user's desk is still better. Automated
checking as first pass of testing procedures would also make sense (it
remains to be seen whether it's better if the developers do the static
tests, or if the testers do it - assuming that these are different
people in the first place.)
> In fact, if the user is allowed to
> incrementally supply type information, it can ask for specific info to
> make certain guarantees.
That's what I'd like to see.
It's not limited to types BTW, there are other properties of a program
that one may want to guarantee.
Actually, a type error message is essentially such a question for
specific info - some kinds of type error anyway. (Type error messages
are a problem only if they prevent running the program.)
> It may even be combined with runtime
> analysis to recommend exactly which types and where they are most
> sorely needed.
I'm highly sceptical that runtime analysis can gather information that
is actually helpful for evaluating the relevance of missing information.
(I'd be interested to see such a system in practice, it's impossible to
tell for sure in advance.)
Regards,
Jo
Joachim Durchholz
This was popularized years ago by Edsger W. Dijkstra, who said that
testing can show no more than the presence of errors, while static
analysis can show the absence of errors.
BTW the dynamic type proponents will say that knowing the type of a term
isn't very interesting after all. (This is because dynamic types tend to
encode little information about the data.)
Regards,
Jo
Pascal Costanza
> Pascal Costanza wrote:
>
>> Joachim Durchholz wrote:
>>
>>> So here's my litmus test for language testability: Does it enable as
>>> many test paradigms as possible?
>>>
>>> Lisp doesn't qualify, it makes static testing (type checking,
>>> automatic proving) difficult, as it gives very little easily
>>> verifiable guarantees what a given piece of code does.
>>
>>
>> [...]
>>
>>> Java sort-of qualifies: its introspection facilities give tools a
>>> foothold that they can work with.
>>
>>
>> [...]
>>
>> A question for understanding: What makes you think that Java's
>> introspective features are better suited than Lisp's?
>
> Lisp makes it far easier to access the definitions of data types and
> functions, but interpreting the definitions is far more difficult
> because it imposes far less restrictions on what the individual
> definitions actually do. (It's the downside of unrestricted power.)
It's possible to impose the restrictions you want in Common Lisp, and a
portable way to analyze these restrictions during macro expansion is in
the works. Some CL implementations already have a limited form of such
analysis facilities, as per CLtL2. I don't know enough about Scheme
implementations, but they probably provide similar facilities.
Of course, as soon as you start to want to have most, or even all of
your code checked, it might have been better to have started with a
language that provides static checks by default. Especially if you don't
want to wait for Lisp implementations to provide the same degree of
static checkability.
But again: a) It would be better if you could provide a static type
system as an additional tool in some futuristic "unified" language
framework. b) There is a class of programs and/or a programming style
that rather needs dynamic checking by default. The essence here is that
you can take advantage of "type" errors at runtime. There are
programs/programming styles in which you _want_ "type" errors at
runtime, however bizarre this might sound to the ears of a static typer.
> I fear I didn't make clear enough that I was talking about testing &
> verification in a fully automated manner, particularly the automation of
> test case selection.
So how do you statically analyze the following piece of code in Java?
Class.forName(someStringExpression)
.getMethod(someOtherStringExpression,
someParameterTypeArrayExpression)
.invoke(someObject,someConcreteParameterArray);
>> (Note: When you refer to "Lisp", in c.l.l this typically means Common
>> Lisp and Scheme. Noone is using LISP anymore as it was defined until,
>> roughly, the end of the 70's.)
>
> That's understood.
> Actually I'm not even talking about the standard Lisps of the '80ies
> (which were Interlisp and its likes; Scheme and CL had just started to
> interest Lisp programmers in general, at least here in Europe).
OK, just wanted to be sure about this.
Pascal Costanza
> Tayss wrote:
>>
>> Seriously, I can not imagine in this new millenium, that static
>> checking proponents are still talking about compile time.
>
> Come on. 99% of all programmers still work with compilers. (This doesn't
> make working with compilers superior, it just defines the standard case
> from which people tend to argue. Abstract that away when weighing
> arguments.)
Nowadays, many programmers use languages like Perl, Python, Ruby, PHP,
and so on. So I wouldn't be so sure about your estimate.
>> So I'd ask: Could a lisp system be configured so that it runs a
>> static analysis upon runtime errors, or at arbitrary points on
>> arbitrary subsets of code?
>
> I'd prefer the latter: static checking when I want it.
> Checking upon runtime errors is better than nothing, but checking before
> the software hits the end user's desk is still better.
There is an important "class" of end-users who might not want to have
their programs checked before they run it. See
http://www.joint.org/use/2003/Papers/18500041.pdf
David Golden
> I'd prefer the latter: static checking when I want it.
> Checking upon runtime errors is better than nothing, but checking before
> the software hits the end user's desk is still better.
Just to be clear, since it's not clear based on your comments that you're
coming from a "modern" lisp background - Common Lisp compilers DO typically
do a degree of static analysis at "compile-time", and some type-inference
e.g. CMUCL.
Also, and this is just a general comment, one must be clear on this:
| Strong | Weak |
--------+---------+----------
Dynamic | Lisp | Perl |
Static | ML | C |
"Strong" and "weak" here referring to how easy it is to violate the type
system. Common Lisp won't happily let you violate its type system, so it's
pretty strongly typed, though it is dynamically typed.
(In fact, the Lisp Machines of yore had hardware type-tagging, so violating
a type would have been a crime akin to a "segmentation violation" on a
conventional untagged CPU, nor did enforcing type safety dynamically have
much speed penalty on such hardware (note that such speed penalties are
themselves pretty irrelevant for most applications in these days of
multi-ghz CPUs)).
Some people assume strong and static go hand-in-hand, even define their
terminology in such a manner, but it's not particularly true.
William D Clinger
>
> Ringo sang it. But it was a Lennon/McCartney composition.
>
> [If I read one of your papers out loud, can I take the credit?
> Please? ;-) ;-)]
Go ahead. Make my day.
Joseph Stinson
;)
Feuer
Erann Gat wrote:
> > If the programmer's mindset leads them to believe that concurrency issues
> > cannot occur just because things compile, then they are indeed incompetent, at
> > least with regards to concurrency.
>
> The situation was that the programmer was making what appeared outwardly
> to be a minor change to a piece of code that had run for months in a
> production environment with no problems. No one imagined that this
> problem would happen. Even after it happened, as I said, it took the
> entire team the better part of a week to figure out what had gone wrong.
The problem was not necessarily (or even likely) caused by the
programmer who made the apparently minor change. It could well have
been caused by the programmers who built the original system.
David
Matthias
> b) There is a class of programs and/or a programming style
> that rather needs dynamic checking by default. The essence here is
> that you can take advantage of "type" errors at runtime. There are
> programs/programming styles in which you _want_ "type" errors at
> runtime, however bizarre this might sound to the ears of a static
> typer.
I think that's true. There is also a class of programs where static
type checking can help find _nontrivial_ errors. Multithreaded
programs might belong to this class:
http://www.cuj.com/documents/s=7998/cujcexp1902alexandr/
So, there's reason enough for both worlds to coexist. :-)
Joachim Durchholz
>
> Of course, as soon as you start to want to have most, or even all of
> your code checked, it might have been better to have started with a
> language that provides static checks by default. Especially if you don't
> want to wait for Lisp implementations to provide the same degree of
> static checkability.
*grin* that's exactly what I wanted to write first.
> But again: a) It would be better if you could provide a static type
> system as an additional tool in some futuristic "unified" language
> framework.
Agreed.
> b) There is a class of programs and/or a programming style
> that rather needs dynamic checking by default. The essence here is that
> you can take advantage of "type" errors at runtime. There are
> programs/programming styles in which you _want_ "type" errors at
> runtime, however bizarre this might sound to the ears of a static typer.
It indeed sounds bizarre.
However, it might be due to a difference in the definition of the term
"type". For me, a type is essentially a tag that I associate with some
piece of data; it may be as precise or imprecise as I wish.
The imprecise-precise spectrum is indeed large; as has been demonstrated
in other threads, it's possible to go from fully dynamic type checking
to ropes-and-shackles discipline-and-bondage style.
(Maybe one should say "fine grain vs. coarse grain" instead of "precise
and imprecise".)
From this perspective, saying "you need to exploit type errors" doesn't
make much sense; if this indeed happens to static typer, the knee-jerk
reaction would be to modify the type system until it properly includes
those types that were previously outside the type checking system.
(Note that with "proper" static typing, the majority of entities uses
types that were defined by the programmer. The type system is part of
the programmer's expressivity just as the program text proper. That's
one of the reasons why the idea of "a type system just restricts me"
sounds absurd.)
>> I fear I didn't make clear enough that I was talking about testing &
>> verification in a fully automated manner, particularly the automation of
>> test case selection.
>
> So how do you statically analyze the following piece of code in Java?
>
> Class.forName(someStringExpression)
> .getMethod(someOtherStringExpression,
> someParameterTypeArrayExpression)
> .invoke(someObject,someConcreteParameterArray);
Initially, I wouldn't, but it might be an interesting exercize to get
some degree of static checking into this type of code. For example, the
someOtherStringExpression could exclude some errors by restricting it to
a javaIdentifierExpression (of JavaIdentifierExpression type), of which
we might know that they could only be constructed given a Class object.
This would, for example, prevent class names from leaking into the
function name space (it would also trivially prevent invalid identifiers
from being accepted as function names, but that's indeed just a trivial
example).
In practice, the kind of guarantee that can be gained this way isn't too
interesting. Any application that I can imagine for this kind of work is
just a thin wrapper around the introspection APIs, and wrappers don't
usually need much checking to give us enough confidence in their
workings. Things get really interesting only if you do something "thick"
above them. For example, for a refactoring browser that uses Java's
introspection API, it might indeed be a good idea to separate the name
spaces for classes, types, and parameter names by putting each into a
separate type even though all are just strings at their heart. Of
course, this doesn't just keep the name spaces apart, we could (if
that's desired) also add guarantees that the names originated from a
Class object, simply by not providing constructors other than those that
used the Class objects. Such guarantees can be helpful when constructing
guarantees that the refactored code will indeed call the same routines
as before, for example.
Regards,
Jo
Joachim Durchholz
> So, there's reason enough for both worlds to coexist. :-)
I'd prefer it if the two worlds were integrated, so that we wouldn't be
forced to choose which of them to throw away for any given project...
Regards,
Jo
Barry Margolin
Erann Gat <g...@jpl.nasa.gov> wrote:
>In article <uisliv...@STRIPCAPStelus.net>, Ray Blaak
><rAYb...@STRIPCAPStelus.net> wrote:
>
>> g...@jpl.nasa.gov (Erann Gat) writes:
>> > > Blaming this failure on the language is really barking up the wrong tree.
>> >
>> > You have badly misunderstood my point. I do not blame this failure on the
>> > language. I blame this failure on the mindset that because the compiler
>> > catches certain kinds of errors that you can get away with less testing
>> > than if it didn't. In other words, I am not saying static typing is bad,
>> > just that one of the benefits that many people cite for it is not really a
>> > net benefit.
>>
>> languages.
>>
>> If the programmer's mindset leads them to believe that concurrency issues
>> cannot occur just because things compile, then they are indeed incompetent, at
>> least with regards to concurrency.
>
>The situation was that the programmer was making what appeared outwardly
>to be a minor change to a piece of code that had run for months in a
>production environment with no problems. No one imagined that this
>problem would happen. Even after it happened, as I said, it took the
>entire team the better part of a week to figure out what had gone wrong.
Isn't that the case with many bugs?
I think you're focusing on the wrong programmer, and maybe that's where the
"cream of the crop" confusion is coming from. Since the bug was always
there, the incompetent programmer was the one who wrote the original code
and left a race condition in it.
--
Barry Margolin, barry.m...@level3.com
Level(3), Woburn, MA
*** DON'T SEND TECHNICAL QUESTIONS DIRECTLY TO ME, post them to newsgroups.
Please DON'T copy followups to me -- I'll assume it wasn't posted to the group.
Barry Margolin
Joachim Durchholz <joachim....@web.de> wrote:
>Joe Marshall wrote:
>
>> hel...@mindspring.com (Rayiner Hashem) writes:
>>
>>>Static typing will tell you exactly one thing --- that your code is
>>>free of type errors. It has its utility --- it means that, if your
>> ^
>> static
>>
>>>code typechecks correctly, you don't have to pay attention to looking
>>>for type errors, rather, you can spend your efforts (testing, code
>> ^
>> static
>>
>>>review time) looking for other sorts of errors.
>>
>> Like the dynamic type errors.
>
>There is no such thing as a dynamic type error. Not in a
>statically-typed language.
You can still have dynamic type errors when the language supports
subtypes. A function that accepts a particular type also accepts any of
its subtypes, but it's possible that it doesn't work properly for some of
them.
There's a simple proof of this: A dynamically-typed language is equivalent
to a statically-typed language where all functions are declared to accept
and return the type at the root of the type hierarchy. Since dynamic type
errors are possible in this language, it shows that there's at least one
statically-typed language that permits dynamic type errors.
Adrian Hey
> In article <bpbirl$rmb$1$8300...@news.demon.co.uk>,
> Adrian Hey <ah...@NoSpicedHam.iee.org> wrote:
>
>> The only extra work I can think of is that a static type system does
>> force you to give some thought to correctness as you write your
>> code.
>
> By "thought to correctness" you really mean, thinking in a type system,
No that isn't what I meant. Though I using that caricature makes you happy
please continue.
> an additional burden I don't want to take on,
It is not a burden, though learning a new language might be.
> especially for such little benefit
The benefits are not "little".
> virtually all of these type errors will be caught by other necessary
> testing.
Virtually all, or all? and they won't be so easy to diagnose in any
event.
Thinking about types must be an important part of correctness, even in an
untyped or "dynamically typed" language. Surely when you define a
function you must have some idea what are and are not safe arguments?
and what "type" (in a very loose informal sense) of result the function
will return. You'll also need some way to communicate this information
to other users of the function, or even just to remind yourself later on.
Since nobody appears to want to demonstrate this alleged extra work
with the phonecodes example, perhaps if we chose a different simpler
example somebody will. Excuse me if I use Haskell, but I think this is
will be clear enough even to non-Haskellers.
I chose the foldr function..
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr f default [] = default -- How to deal with emtpty list
foldr f default (a:as) = f a (foldr f default as)
The first line is an (optional!) type signature. The lower case
letters are universally quantified type variables, which means
the actual types can be anything at all, so long as they match
properly in any actual use of foldr (the same lower case letter
always stands for the same actual type in any expression involving
foldr).
Typical use might be:
sum :: Num n => [n] -> n -- Sums any list of Num(bers)
sum ns = foldr (+) 0 ns -- (+) is overloaded for all Num(bers)
concat :: [[a]] -> [a]
concat as = foldr (++) [] as -- ++ joins 2 lists.
In general the first argument can be any function of type..
A -> B -> B , where A and B are actual types
but it is an error to use a function of type..
B -> A -> B , for example
(a common enough mistake that I make from time to time).
This is real logical error (not the type system being awkward
or getting in the way) that isn't going to go away and will have
to be fixed sooner or later. If the Haskell compiler permitted
such expressions I'd still have 1 more bug to find by some other
means.
So I ask, if I was using Lisp (for arguments sake)..
How do I communicate to other users what are and are not legal
arguments?
Why is it easier to detect *and* diagnose such errors using
unit tests, especially considering that typically the error won't
be detected until the first argument (f) is actually applied (and
often not even then I suspect), making diagnosis of the real problem
much harder.
Where is the extra work in the Haskell solution that isn't
required one way or another in any (correct) implementation of
foldr in any language?
>> So maybe you could
>> illustrate what extra work your talking about if we chose a specific
>> example we are both familiar with, the phonecodes problem. I posted
>> a Haskell solution which you can dig out of the google if you like.
>> How do you think the presence of a static type system impeded development
>> of this program?
>
> This is tantamount to asking us to retroactively get inside your head
> and know everything that you were doing and thinking from the time you
> first read the spec, to the time your program compiled and tested
> correctly. The extra work is having to conform your thought about the
> problem to Haskell's type system, and being forced to correct any type
> errors before your program is allowed to run. This extra work isn't
> going to be visible in the finished code any more than the initial list
> based, throw away drafts of a lisp solution would be visible in a final
> program that uses CLOS or hash tables.
This "extra work" wasn't extra work at all, all type errors were real
logical flaws and would need correction anyway before the program stood
any chance of working, even if Haskell did provide some way of turning
type checking off.
I see fact that they were detected and diagnosed automagically, without
me having to write or run a single line of test code as a *big* win,
not a "little benefit". (In fact in this case once the program typechecked
it did indeed work first time).
Regards
--
Adrian Hey
Adrian Hey
Andreas Rossberg wrote:
> Erann Gat wrote:
>>
>> I can't really speak to this because I don't know Haskell. But the
>> episode in question involved C++. And in the case of ML the extra work
>> involves things like changing all you arithmetic operations if you decide
>> to change an int to a float.
>
> Not in Standard ML.
Not in Haskell either
(not that I think that's necessarily a good thing :-).
Regards
--
Adrian Hey
Adrian Hey
> perhaps you are explaining the
> very real problem of how local fixes to satisfy a static system end up
> damaging code globally.
Huh? I don't understand this very real problem at all.
Can you provide a concrete example?
Regards
--
Adrian Hey
Isaac Gouy
> In article <h6sn81-...@ID-7776.user.dfncis.de>, Dirk Thierbach
> <dthie...@gmx.de> wrote:
> > You guard against race conditions by careful programming, and by
> > planning in advance.
>
> Or by putting in run-time sanity checks. If I had had the foresight and
> the strength of my own convictions I would have put code into the biller
> that stopped the billing process immediately as soon as a request was made
> to bill a ridiculously high amount, for some value of "ridiculously
> high". That would have solved the problem too.
>
> Neither static nor dynamic typing would have helped in this situation.
> But I do believe that a dynamic typing *mindset* would have been more
> likely to produce a correct solution because it encourages you to think
> more about possible run-time errors.
Neither a static nor dynamic typing *mindset* would have helped,
that's clear as soon as you say "more likely to produce a correct
solution".
Maybe the interesting question is "How can we program systems which
behave in a reasonable manner in the presence of software errors?"
The Erlang community seems to have some coherent ideas about that
question.
(Thanks for starting a new discussion, the old thread had become
difficult to follow.)
best wishes, Isaac
Mario S. Mommer
Joachim Durchholz <joachim....@web.de> writes:
> There is no such thing as a dynamic type error. Not in a
> statically-typed language.
> Unless you count type casts in. Type-inferring languages like ML or
> Haskell don't even have them though - they are unnecessary. (Well, you
> can always do a type cast by going through C, which would be
> excessively awkward. The important point being: there was never
> pressure from the language users to add a more convenient way to do
> type casts.)
That's interesting. How do you handle a case like this in such a language?:
double b;
b = sqrt(4*x^4+8*x^3-3*x^2+3*x-8*x+2);
with x a floating point number? Do you have no other choice but to
define b as a complex number, or do these languages fire up maple and
figure it out?
Andreas Rossberg
>>
>>There is no such thing as a dynamic type error. Not in a
>>statically-typed language.
>
> You can still have dynamic type errors when the language supports
> subtypes.
Only if the type system has holes or its subtyping rules are unsound (one
instance of the former is the presence of downcasts, instances of the
latter are the infamous covariant function types, or subtyping on mutable
collections).
> A function that accepts a particular type also accepts any of
> its subtypes, but it's possible that it doesn't work properly for some of
> them.
Then it would not be a subtype.
> There's a simple proof of this: A dynamically-typed language is equivalent
> to a statically-typed language where all functions are declared to accept
> and return the type at the root of the type hierarchy.
No, this is wrong. All subtypes of the type TOP->TOP you sketch have the
form TOP->t (for arbitrary t). That is, no function of this type can do
anything interesting with its argument, as long as it does not do an
(inherently type-unsafe) downcast.
This confusion about the direction (variance) of subtyping for function
types unfortunately still is common.
Frank A. Adrian
> Types encode invariants. They form a contract about the behaviour
> of some part of my code. If I break this contract in such a way that
> it changes the type, the type checker will point out all places
> I have to think about.
Why do you believe that all variables and parameters need this very strict
invariant during all phases of program development, even disallowing the
testing of a portion that does type-check safely simply because some other
portion of the program does not?
faa
Joe Marshall
> The reason for this is that in a multithreaded environment you would
> have to check an /exponential/ number of "different" programs (because
> the scheduling might switch threads after each operation, in effect
> creating a different control flow each time). IMHO, there is no
> chance to fix a race condition in a moderately complex multithreaded
> program by unit testing.
I disagree, but the technique isn't easy. The idea is to attempt to
*induce* the situations that lead to race conditions: heavy loads,
huge numbers of threads, rapid thread switching, etc. It can make
sense to put switches in the code that deliberately detune the system
to enhance the liklihood of races.
Joachim Durchholz
> Maybe the interesting question is "How can we program systems which
> behave in a reasonable manner in the presence of software errors?"
>
> The Erlang community seems to have some coherent ideas about that
> question.
For those who don't want to dig it up, here's the Erlang "philosophy" in
a nutshell, filtered through my understanding:
1) Decouple the task at hand into many (>> 100, often >> 10.000)
processes. (You need your own scheduler to do that, OS schedulers
usually aren't up to that task. Processes also need to be extremely
lightweight, both in terms of size overhead and in terms of process
switching time.)
2) Use copying semantics to communicate between processes. No "shared
memory", at least not conceptually. That way, if one process crashes
(something that we expect since software is buggy), it will not be able
to affect the data that other processes are working with. (This is what
Erlangers mean if they say "message passing semantics" - the messages
are copied, not transmitted by reference.)
3) If a process runs into a problem, let it crash as quickly as
possible. "Problem" in this context means /uncorrectable/ problem, that
is, if the programmer has no idea what the process should do in some
specific circumstance. (Actually the advice goes even further: if the
specification is incomplete and a situation occurs that's not described,
the programmer shouldn't try to fill in the gaps, he should simply throw
an exception that will crash the process.)
4) Processes have supervisor processes. If a process crashes, the
supervisor is reliably informed that the process has crashed. Usually,
the supervisor should also get a stack dump and other information that
might help diagnose the crash, but that's more for giving the
programmers a clue than for the operation of the system itself. (It's
still important, of course.)
5) If a supervisor finds that a child has crashed, it should restart it
(possibly after restarting other processes that must be restarted
together with it). This is to work around transient problems, such as
read errors, nonfatal race conditions (they tend to be nonfatal because
processes crash at the earliest opportunity, i.e. usually before any
corrupted data makes it into a permanent data pool).
6) If restarting results in an immediate crash (for some
application-dependent definition of "immediate"), assume the failure is
permanent. Either let the supervisor itself crash (causing a
higher-level supervisor to inspect the problem). Alternatively, start a
simpler (set of) process(es) that will render a restricted set of
services. (In other words, if a telephone finds that its dialling
process crashes permanently, shut it down. Let the process for receiving
phone calls continue, or - if dialling and receiving processes are
interrelated - shut down the receiving process and restart a simpler
receiver process that doesn't interact with dialling.)
I haven't programmed with that paradigm, but from my experience with
other paradigms, I'd say that this has potential.
It isn't entirely necessay to map this all to processes. Processes with
a copying communication semantics are just the easiest and historically
most reliable strategy for achieving fail-safe independence between
program parts. A language that uses immutable data almost exlusively,
offers strong barriers between those domains that do use mutable data,
and has an Eiffel-style exception mechanism (designed for shutting down
faulty software, not for shortcut control transfers) should be able to
apply this mindset just as well.
Generally, it's a "let it crash, have other software layers correct the
problem if possible, have these other layers diagnose it anyway" philosophy.
As a side benefit, it allows "aggressive programming". You don't litter
your code with error handling, you simply trigger an exception if things
go wrong unexpectedly.
Just my understanding, as far as I gleaned it from Joe Armstrong's
doctoral thesis. (Thanks to Joe for explaining the issues so clearly, it
made a lot of things explicit that would have remained implicit for me
if not written down in his thesis.)
Regards,
Jo
Joe Marshall
> Joe Marshall wrote:
>
>> hel...@mindspring.com (Rayiner Hashem) writes:
>>
>>>Static typing will tell you exactly one thing --- that your code is
>>>free of type errors. It has its utility --- it means that, if your
>> ^
>> static
>>
>>>code typechecks correctly, you don't have to pay attention to looking
>>>for type errors, rather, you can spend your efforts (testing, code
>> ^
>> static
>>
>>> review time) looking for other sorts of errors.
>> Like the dynamic type errors.
>
> There is no such thing as a dynamic type error. Not in a
> statically-typed language.
> Unless you count type casts in.
Type casts *and* cases where a type union needs to be discriminated
and at least one clause raises an error. I would consider both of
those to be dynamic type errors.
If you do not consider the union discrimination case to be a type
error, then Lisp trivially does not raise dynamic type errors, either.
Erann Gat
<fi...@my.address.elsewhere> wrote:
> g...@jpl.nasa.gov (Erann Gat) writes:
>
> > In article <m1llqe8...@tti5.uchicago.edu>, Matthias Blume
> > <fi...@my.address.elsewhere> wrote:
> >
> > > In fact, static analysis (although perhaps not in form of type
> > > systems) is your best (some may say: only) bet against the possibility
> > > of race conditions and their ilk.
> >
> > Ironically, I actually agree with this.
>
> With Gerard at JPL now, you better agree! :-)
I've been singing the praises of Spin ever since it was used to catch race
condition bugs in code that I had written. That really knocked my socks
off.
E.
Erann Gat
<dthie...@gmx.de> wrote:
> Erann Gat <g...@jpl.nasa.gov> wrote:
> > In article <h6sn81-...@ID-7776.user.dfncis.de>, Dirk Thierbach
> > <dthie...@gmx.de> wrote:
>
> >> Nobody expects static typing to guard against race conditions.
>
> > Not consciously, no. But tacitly, yes, I think people do expect this,
> > even if they don't realize it.
>
> So you say you don't believe in static typing because you have met
> people who are stupid?
No, I am saying that I don't believe in static typing because I have met
very smart people who ended up doing very stupid things as a result (I
believe) of using static typing systems.
> Come on, you cannot be serious.
I am quite serious.
> You seem to have some strange ideas about a "static typing mindset".
> I believe you that you have met incompetent people who were using
> static typing, but they are also incompetent people who are using
> dynamic typing. That really proves nothing.
This all comes down to the question of whether the engineer in question
was smart or not. Of course, I can't prove he was; you have to take my
word for it. The only objective evidence I can offer is how long it took
to find the bug after it manifested itself. You'd have to believe that
the entire team was stupid. That may well be, but the company in question
is doing quite well and their product is very highly regarded so someone
there is doing something right.
You can also calibrate my assessment by asking anyone who knows me if I am
the least bit shy about levying a charge of stupidity if I think it is
warranted.
E.
Erann Gat
> Arthur Lemmens wrote:
> >
> > There's one big advantage to finding errors at run-time rather than
> > compile-time: you can get a lot more information about the situation
> > that caused the error.
>
> No, you get different information. Static analysis can infer global
> information that won't be available during runtime, where you just look at
> one execution path at a time.
>
> That's why should have both.
Yes. The story was not meant to be a warning against *using* static
typing, merely against *relying* on it. I believe that languages that
enforce static typing (as opposed to offering it as an optional tool) tend
to drive people towards relying on it.
E.
Joe Marshall
> Erann Gat wrote:
>
>> The real payback from
>> compile-time detection of type errors is not a reduced necessity for
>> testing; it is instead merely a time savings, finding those errors
>> sooner rather than later.
>
> Well, there's also the fact that when you give a type to a term you have
> a proof, and when you give a series of tests about the type of a term
> you have a good probability, but not the rigorous proof, that those
> errors won't come up.
Depends on what you mean by `proof' and `good probability'.
If the type checker complains, you have found a `proof' that the type
checker cannot determine that your code is correct. But this is not
the same as proof that your code is wrong.
If a test case finds an error, this is proof that your code is wrong.
If all test cases pass, this is *not* proof that your code is right.
Marco Antoniotti
Rayiner Hashem wrote:
> Hmm, that's not so much a weakness in static typing, but rather of
> those who use the type system as a mental crutch to avoid reasoning
> about the code. The comment about changing a type and then having the
> compiler tell you where you need to make modifications made me cringe.
> That's an abuse of the type system, not a good way to take advantage
> of it! Of course, dynamic typing would not have helped in your case.
> Only proper testing and code review would have.
>
> Static typing will tell you exactly one thing --- that your code is
> free of type errors. It has its utility --- it means that, if your
> code typechecks correctly, you don't have to pay attention to looking
> for type errors, rather, you can spend your efforts (testing, code
> review time) looking for other sorts of errors. People who sell static
> typing as a panacea (like anybody who sells anything as a panacea) are
> selling you snake oil.
Exactly. I agree with this. This is why CMUCL/SBCL are the closest
thing to THE RIGHT THING that exists on the planet. OTOH, spending ages
to satisfy the Type Checker before you can run your program (in a
*ML-like language without S-exprs and macros - sorry the Ocaml
preprocessor and Haskell macros do not even come close) is not my idea
of fun or productivity :)
Cheers
--
Marco
Dirk Thierbach
> Of course, as soon as you start to want to have most, or even all of
> your code checked, it might have been better to have started with a
> language that provides static checks by default.
Yes. That's exactly the point.
> Especially if you don't want to wait for Lisp implementations to
> provide the same degree of static checkability.
For reasons already discussed, I don't think this is going to happen.
(It is not *necessary* that Lisp does everything you can do in other
languages. It's fine as it is.)
> But again: a) It would be better if you could provide a static type
> system as an additional tool in some futuristic "unified" language
> framework.
Yes, it would. I think that if there is really need for it, one
could probably modify Haskell or OCaml to "go dynamic" if type
inference fails. Introduce a "top" type, do something clever about
compositionality so you still retain a reasonable amount of type
inference, tag everything that comes "into" a top type at runtime
with the appropriate type, and insert dynamic type checks everywhere
where they are needed. And print big fat warnings :-)
But that would be a huge effort, with (from the "static typers" point
of view) little benefit.
> b) There is a class of programs and/or a programming style
> that rather needs dynamic checking by default. The essence here is that
> you can take advantage of "type" errors at runtime. There are
> programs/programming styles in which you _want_ "type" errors at
> runtime, however bizarre this might sound to the ears of a static typer.
Yes. In those cases, use a dynamically typed language. All languages
have advantages and disadvantages. No language does everything equally
well.
- DIrk
Ray Blaak
> The situation was that the programmer was making what appeared outwardly
> to be a minor change to a piece of code that had run for months in a
> production environment with no problems. No one imagined that this
> problem would happen. Even after it happened, as I said, it took the
> entire team the better part of a week to figure out what had gone wrong.
And this is quite normal, even for smart programmers. Concurrency is
*hard*. It really really is.
You almost have to do (pseudo-) formal correctness proofs constantly to be
sure things are ok. Using a language with decent concurrency support helps
too, of course.
What this example is definitely not, however, is an example of a disadvantage
of statically typed languages.
--
Cheers, The Rhythm is around me,
The Rhythm has control.
Ray Blaak The Rhythm is inside me,
rAYb...@STRIPCAPStelus.net The Rhythm has my soul.
Andreas Rossberg
>>
>> No, you get different information. Static analysis can infer global
>> information that won't be available during runtime, where you just look
>> at one execution path at a time.
>>
>> That's why should have both.
>
> Yes. The story was not meant to be a warning against *using* static
> typing, merely against *relying* on it. I believe that languages that
> enforce static typing (as opposed to offering it as an optional tool) tend
> to drive people towards relying on it.
The subject line you chose suggested otherwise. And I found your reasoning
mildly absurd, especially since the problem in question would be completely
unaffected by any preference wrt typing. You could equally well deduce that
higher-level languages give a false sense of security, because they used
C++ or Java rather than assembly language.
And having been bitten by concurrency issues myself more than once, I would
suspect that the actual bug wasn't in the changes, but already lied buried
in the original code, as somebody else pointed out before.
Ray Blaak
> What I also find interesting about this episode is, at
> the meta level, that you got the responses I expected
> right away:
> * the programmers were incompetent (shoot the messenger)
> * That's not a typing issue, it's a concurrency issue (head in the sand).
Umm. It *is* a concurrency issue. "Head in the sand" would be to pretend it's
something else.
> I would almost go so far as to say that KNOWING you're going
> to get errors at runtime is BETTER, because it leads to safer/more
> robust designs.
You are right.
But you have to deal with runtime errors in every "real" program, static vs
dynamic typing notwithstanding.
The incompetency, if there was any, is the assumption that one doesn't have
runtime errors just because a statically typed language is used.
(And I am not convinced this incompetency was present in this example either.
I think instead that they ran into a difficult concurrency bug. Perhaps a
better design could have avoided it, perhaps a language with better
concurrency support would have helped, I don't know.)
One maybe has little or no *typing* errors, but that is not the same thing.
The mantra of static typing freaks is that one still gets bugs, but just the
interesting ones, not the stupid tedious ones that result from things not
"fitting" together.
> Your programmer _knows_ he might have missed a call path, and will think
> about where/how to handle those missed errors, even if it's just to log the
> bug and continue in some sane state.
Wise advice for any programmer in any language.
Ivan Boldyrev
> William D Clinger wrote:
>> I'm certain that it happens all the time.
>> Ringo Starr
>
> Ringo sang it. But it was a Lennon/McCartney composition.
>
> [If I read one of your papers out loud, can I take the credit? Please?
> ;-) ;-)]
If you would sing one of his papers, surely you can :)
--
Ivan Boldyrev
Onions have layers. Unix has layers too.
Marco Antoniotti
Joachim Durchholz wrote:
> Raffael Cavallaro wrote:
>
>> Adrian Hey <ah...@NoSpicedHam.iee.org> wrote:
>>
>>> The only extra work I can think of is that a static type system
>>> does force you to give some thought to correctness as you write
>>> your code.
>>
>>
>> By "thought to correctness" you really mean, thinking in a type
>> system, an additional burden I don't want to take on, especially for
>> such little benefit - virtually all of these type errors will be
>> caught by other necessary testing.
>
>
> If you say "type", you think Integer, Real, or some record type.
>
> Functional data types are (mostly) variant records (similar to Pascal,
> but type-safe: the type used is encoded, and the language will not allow
> you to reinterpret memory bits by assuming the wrong type).
I think it is very difficult to have #C(3.14 4) be interpreted as a
symbol or a string or a FOO (where FOO was defined as a class) in Common
Lisp.
Cheers
--
Marco
Dirk Thierbach
> Dirk Thierbach wrote:
>
>> Types encode invariants. They form a contract about the behaviour
>> of some part of my code. If I break this contract in such a way that
>> it changes the type, the type checker will point out all places
>> I have to think about.
> Why do you believe that all variables and parameters need this very strict
> invariant during all phases of program development,
Because unless I explicitely say so, this invariant will be the minimal
invariant needed to make the program work at all. Let's again have a
look at the type of map
map :: (a -> b) -> [a] -> [b]
This just says that one argument should be a function, and the other
argument should be a list. Duh. Moreover, the function should be able
to deal with the elements that are in the list. In return, I am
promised a list of whatever things the function produces.
If any of these invariants is invalidated, map cannot possibly work.
So either I have made a typo somewhere, or I have made a design error.
> even disallowing the testing of a portion that does type-check
> safely simply because some other portion of the program does not?
We already discussed this. If I typed too fast and I really want
to experiment with parts of the code, I just comment the other part
out. Usually, I don't want to do any experiments at all, because
the type checks *are* the experiments I am interested in in the
first place. And in situations where I haven't dealt with all
the possible tags in a datatype (as in Joes example), I don't have
to do anything at all, it *will* typecheck and I can do the experiments,
though I will get warnings.
- Dirk
[Followup ignored]
Dirk Thierbach
> No, I am saying that I don't believe in static typing because I have met
> very smart people who ended up doing very stupid things as a result (I
> believe) of using static typing systems.
This does not match my experience at all. And, as you say,
the important point is:
> The story was not meant to be a warning against using static typing,
> merely against relying on it.
If there are indeed any people who are so stupid to think that because
they have static typing, their programs will be automatically
completely bug free, then it should be easy to explain to them
that no possible static type system in the world can achieve this.
> I believe that languages that enforce static typing (as opposed to
> offering it as an optional tool) tend to drive people towards
> relying on it.
I still cannot believe this.
> The only objective evidence I can offer is how long it took
> to find the bug after it manifested itself.
That's somewhat typical for race conditions. If you don't invest
effort up front to combat them, they are really hard to catch.
> You'd have to believe that the entire team was stupid.
I'd probably believe that somebody in the team was sloppy. Race condition
bugs do happen, even to smart people.
> You can also calibrate my assessment by asking anyone who knows me if I am
> the least bit shy about levying a charge of stupidity if I think it is
> warranted.
I certainly think that any claim that your usual Java, C++, Haskell or
OCaml type system guards against race conditions is so completely stupid
that I cannot even imagine someone could make it.
And concluding that "one does not believe in static typing" based on
that evidence isn't really smart IMHO, either. (Sorry, but I am also
not shy in this respect).
- Dirk
Dirk Thierbach
> Exactly. I agree with this. This is why CMUCL/SBCL are the closest
> thing to THE RIGHT THING that exists on the planet.
There we go again with claims that there is ONLY ONE RIGHT THING.
From the "static camp" point of view, it is the WRONG THING, because
it's much too weak. It combines some of the disadvantages of both
worlds: You are forced to use type annotations, *and* you don't
get complete code coverage.
> OTOH, spending ages to satisfy the Type Checker before you can run
> your program [...] is not my idea of fun or productivity :)
And if you don't want to do that, then don't do it. But from the
"static camp" point of view, you don't have to "satisfy" the
type checker or invest "extra work". It's part of the normal
development process, in the same way you write your tests, let
your code fail, and then change your code until it works. The only
difference is that the tests are not hand written.
Is it so hard to accept that there might be actually different ways
of doing things, and your way, however you personally like it, is
not the only one, or the "best" one?
- Dirk
Garry Hodgson
> No, I am saying that I don't believe in static typing because I have met
> very smart people who ended up doing very stupid things as a result (I
> believe) of using static typing systems.
so i take it you are opposed to four-wheel-drive and anti-lock
brakes in cars? i have seen many people do incredibly stupid
things around here when the weather is bad, because they
fail to realize that their spiffy new vehicles, alas, must still
obey the laws of physics.
if they knew they had no traction, and couldn't stop quickly
without spinning out, they might drive more carefully.
or maybe they'd just have more accidents.
----
Garry Hodgson, Technology Consultant, AT&T Labs
Be happy for this moment.
This moment is your life.
Kaz Kylheku
> In article <bpd0og$6e9$1...@news.oberberg.net>,
> Joachim Durchholz <joachim....@web.de> wrote:
> >There is no such thing as a dynamic type error. Not in a
> >statically-typed language.
>
> its subtypes, but it's possible that it doesn't work properly for some of
> them.
You can have dynamic type errors in a static language if it has an
escape hatch that allows for discriminated unions. In other words, it
allows the program to conditionally treat a piece of memory as having
more than one possible type.
If you don't have this escape hatch, then dynamic typing can be
bootstrapped only in some very circuitous, expensive way. For example,
you pick the most flexible data structure in the language---such as
the character string---and force it to represent everything. The
integer 42 is represented, perhaps, as the string "42", and addition
is done on strings, and so forth. Or instead of a discriminated union,
you make a large aggregate instead. Since you can't overlap the memory
between an integer, floating point number or string (for instance),
you make a container that has all three and an indicator of which
value is intended.
We can look at Lisp as a dynamic language that is bootstrapped in a
simple, low-level static language with discriminated unions. That
static language ensures that a memory cell is always treated properly.
A rigid representation scheme allows some bits of memory to be trusted
to indicate what can be done with the remaining bits. Unless an escape
hatch has been invoked to defeat the safety, Lisp will not, for
instance, add two cons cell references as though they were integers.
Or, for instance, passing an integer to a function that needs a cons
cell will not blow the parameter passing mechanism: the representation
was chosen so that the call is compatible.
Your Lisp compiler and/or interpreter eliminated these errors at the
time they were built.
When your Lisp system throws some type mismatch condition at you,
that's not realy a type error; it's a soft condition detected by a
statically typed program (or safe machine code generated by a program
that was statically typed).
Static typing forms that rigid substrate that lets us bootstrap more
flexible things. At some point, it helps to have the assurance that a
variable points to valid memory with a known, rigid representation.
Some programmers want to carry this ``stone knife'' with them to
higher levels of programming.
> There's a simple proof of this: A dynamically-typed language is equivalent
> to a statically-typed language where all functions are declared to accept
> and return the type at the root of the type hierarchy.
Right, but that static language needs some type introspection. It's
not an entirely static language. To be useful, this type hierarchy
needs a way to ask an object what its type is, so for instance the
most specific method can be applied to it. That constitutes a form of
dynamic typing. Otherwise, if a reference to an object can be
converted to a supertype reference, but the reverse conversion is not
possible, that is next to useless!
Barry Margolin
Erann Gat <g...@jpl.nasa.gov> wrote:
>No, I am saying that I don't believe in static typing because I have met
>very smart people who ended up doing very stupid things as a result (I
>believe) of using static typing systems.
What you're basically indicting is not static typing, but most forms of
automation. Any time we hand off some responsibility to the computer, we
end up relying on it, and sometimes we may expect the computers to do more
than they really can. Someone else pointed out that your complaint about
static typing is very similar to the complaints people have made about
automatic memory management. In fact, it goes much lower than that; it
took a long time before most of the CS community accepted that high level
languages were appropriate for OS programming (for many years Multics and
Unix were the only examples outside research groups).
I just can't fathom an experienced programmer thinking that if a program
compiles cleanly then it must be OK. In particular, if he's used to
programming in statically-typed languages, he doesn't generally encounter
type errors, but he must have experienced many bugs in his career. Since
they weren't type errors (because the language prevents those), he should
be used to dealing with non-type errors, and be on the lookout for them.
So what possible experience could have led him to do this stupid thing?
Perhaps "incompetent" wasn't the right word. In my career I've met some
excellent programmers who are sloppy. They know the system well, and they
produce lots of product, but bugs are frequently found during code reviews
and testing. We bitch about them and maybe make jokes behind their backs,
but we keep them on board because even with the bugs the net result is
better than if we didn't have them in the first place.
--
Barry Margolin, barry.m...@level3.com
Level(3), Woburn, MA
*** DON'T SEND TECHNICAL QUESTIONS DIRECTLY TO ME, post them to newsgroups.
Please DON'T copy followups to me -- I'll assume it wasn't posted to the group.
Steven E. Harris
> Ironically, I actually agree with this.
Can you elaborate? How do types interact with timing conditions?
--
Steven E. Harris :: seha...@raytheon.com
Raytheon :: http://www.raytheon.com
Barry Margolin
Andreas Rossberg <ross...@ps.uni-sb.de> wrote:
>Barry Margolin wrote:
>>>
>>>There is no such thing as a dynamic type error. Not in a
>>>statically-typed language.
>>
>> You can still have dynamic type errors when the language supports
>> subtypes.
>
>Only if the type system has holes or its subtyping rules are unsound (one
>instance of the former is the presence of downcasts, instances of the
>latter are the infamous covariant function types, or subtyping on mutable
>collections).
>
>> A function that accepts a particular type also accepts any of
>> its subtypes, but it's possible that it doesn't work properly for some of
>> them.
>
>Then it would not be a subtype.
I disagree. Sometimes you need to special-case certain subtypes. For
instance, flightless-bird is a subtype of bird, but a function that takes
objects of type bird and performs operations on the assumption that they
can fly would have a type error.
Perhaps the bird type should be split into two subtypes, flying-bird and
flightless-bird, and that function should only accept flying-bird. What
this shows is that you have to design your type hierarchy carefully to
prevent type errors like this.
Steven E. Harris
> How do types interact with timing conditions?
I misread "static /analysis/" and thought you were referring only to
static type checking.
Tayss
reading a flamewar and maybe a couple of rhetorical flourishes stuck
in my head. Especially strange since I mainly agree.
Joachim Durchholz <joachim....@web.de> wrote in message news:<bpd5s3$dpt$1...@news.oberberg.net>...
> Tayss wrote:
> > Seriously, I can not imagine in this new millenium, that static
> > checking proponents are still talking about compile time.
>
> Come on. 99% of all programmers still work with compilers.
I think that using this terminology, born from what many now regard as
an optimization, is mentally limiting. Even with Java, I can use an
incremental compiler as a step to making myself forget it's compiled
(from a developer's standpoint).
Further, if I conflate "compiletime and runtime" by making unit tests
a part of my compile process, then how relevant do those words become
to this discussion?
> Checking upon runtime errors is better than nothing, but checking before
> the software hits the end user's desk is still better. Automated
> checking as first pass of testing procedures would also make sense (it
> remains to be seen whether it's better if the developers do the static
> tests, or if the testers do it - assuming that these are different
> people in the first place.)
- Erann argues that local fixes to shut a static typechecker up causes
bad software overall. Many of us have seen this fix-and-run style.
- Static checking can point to more insidious errors, but this good
information is lost if we arbitrarily partition compiletime and
runtime errorhunting.
- This compiletime/runtime split can interfere with future engineering
methodologies. For example, an engineer may desire to test an Agile
Methodology hypothesis that errorfixing should occur at once, starting
from a compiled image. While it may fail, her experiments could
provide valuable insights for engineering improvements.
- Pull all the analysis from James W. Goodwin's 1981 paper "Why
Programming Environments Need Dynamic Data types": "Dynamic data
types... require that the distinction between compile and runtime
environments be removed, and that the explicit use of type information
at runtime be recognized as a valid and desirable abstraction
technique, not merely a symptom of some deficiency in the type
checking."
(Man, that _Interactive Programming Environment_ book recommended by
lispers comes in real handy.) For deeper analysis, you can consult
that paper and ask yourself is it's been obsoleted.
- Perhaps the ideas in Rich & Shrobe's "Initial Report on a LISP
Programmer's Apprentice" paper have led to some success (maybe amid
failures) that could be cannibalized to creating a working
static+dynamic system.
> I'm highly sceptical that runtime analysis can gather information that
> is actually helpful for evaluating the relevance of missing information.
> (I'd be interested to see such a system in practice, it's impossible to
> tell for sure in advance.)
This could strengthen code coverage tools, though I haven't used them.
Thant Tessman
> In article <bpdggn$t3b$1...@grizzly.ps.uni-sb.de>,
> Andreas Rossberg <ross...@ps.uni-sb.de> wrote:
>
>>Barry Margolin wrote:
[...]
>>>A function that accepts a particular type also accepts any of
>>>its subtypes, but it's possible that it doesn't work properly for some of
>>>them.
>>
>>Then it would not be a subtype.
>
>
> I disagree. Sometimes you need to special-case certain subtypes. For
> instance, flightless-bird is a subtype of bird, but a function that takes
> objects of type bird and performs operations on the assumption that they
> can fly would have a type error.
What you're describing is inheritance. Inheritance is one way to provide
for subtyping, but it places constraints on designs that encourage the
introduction of holes in the type system to allow for the
"special-cases" to which you refer. Some people even erroneously
conclude we're better off with no static typing systems at all. :-)
[...]
-thant
Erann Gat
<joachim....@web.de> wrote:
> Being lulled into a false sense of security can happen with /any/
> testing method, be it unit tests, static typing, black-box testing, or
> whatever.
Static typing is not a testing method. That's the whole point. It is a
technique that purports to eliminate a certain class of run-time errors
and therefore (presumably) the need to test for them.
E.
Erann Gat
<use...@consulting.net.nz> wrote:
> Hi Erann Gat,
>
> > I can't really speak to this because I don't know Haskell. But the
> > episode in question involved C++. And in the case of ML the extra work
> > involves things like changing all you arithmetic operations if you
> > decide to change an int to a float.
>
> This lack of explicitness is a weakness in Common Lisp and a potential
> source of inaccuracy. It arises whenever integer to float conversion must
> be more precise than single floating point arithmetic and it can be really
> hard to spot the inaccuracy within a series of computations.
>
> Specifically the problem is with automatic single- to higher-float
> contagion which the rules make difficult to spot.
The solution to this is to add a (optional) warning to signal when this
happens, not to require the user to write single-float-add and
double-float-add and integer-add and rational-add and
single-float-multiply and double-float-multiply and integer-multiply and
rational-multiply and single-float-complex-add and
double-float-complex-add etc. etc. etc. etc. instead of + and *.
E.
Erann Gat
<joachim....@web.de> wrote:
> Erann Gat wrote:
> >
> > Or by putting in run-time sanity checks. If I had had the foresight and
> > the strength of my own convictions I would have put code into the biller
> > that stopped the billing process immediately as soon as a request was made
> > to bill a ridiculously high amount, for some value of "ridiculously
> > high". That would have solved the problem too.
>
> At the point where you'd like to put in the sanity checks, you usually
> don't have the information that allows you to decide what's
> "ridiculously high" and what isn't. For some site, an amount in excess
> of 10.000$ would have been ridiculous, others might really have to pay
> millions.
> Actually, some of the bogus payments were actually caught
Right, and as soon as the first one was caught the system should have
stopped and waited for human intervention instead of proceeding.
This would not have eliminated the problem, of course, but it would have
mitigated the damage and made recovery easier. IMO that is in general the
best you can hope for.
E.
Erann Gat
<vincenzo_...@yahoo.it> wrote:
> Erann Gat wrote:
>
> > The real payback from
> > compile-time detection of type errors is not a reduced necessity for
> > testing; it is instead merely a time savings, finding those errors
> > sooner rather than later.
>
> Well, there's also the fact that when you give a type to a term you have
> a proof,
Maybe, but that doesn't matter. What I am disputing is the tacit
implication that this proof has net positive value.
E.
Erann Gat
> Erann Gat wrote:
> >>
> >> No, you get different information. Static analysis can infer global
> >> information that won't be available during runtime, where you just look
> >> at one execution path at a time.
> >>
> >> That's why should have both.
> >
> > Yes. The story was not meant to be a warning against *using* static
> > typing, merely against *relying* on it. I believe that languages that
> > enforce static typing (as opposed to offering it as an optional tool) tend
> > to drive people towards relying on it.
>
> The subject line you chose suggested otherwise.
Well, I chose a title that was deliberately provocative to stir up
debate. This is usenet after all :-)
> And I found your reasoning
> mildly absurd, especially since the problem in question would be completely
> unaffected by any preference wrt typing.
Not directly, no. But I do believe that there was indirect causation. An
overemphasis on static typing led to other issues not receiving the
attention they deserved.
The important point here is not what the programmer did, it's what the
manager did. His reasoning was: we can't use language X because it
doesn't have static typing, and any language that doesn't have static
typing could produce run-time type errors and that would be bad. So we'll
use C++, which has static typing, instead. The use of C++ was, IMO,
directly causal in this case because it was not only a race condition, but
it was a race condition that involved an implicit call to a destructor,
which can only happen in a language without automatic memory management.
So this manager traded one potential problem (run-time type errors) for a
different potential problem with (nearly) disastrous results. But I don't
believe he made this decision consciously. I believe - based on the
conversation I had with him about development methodlogy - that he simply
believed that static type checking trumps everything else, or at the very
least that it has inherent value independent of all other considerations.
And I'm saying that it doesn't.
E.
Ray Blaak
> The important point here is not what the programmer did, it's what the
> manager did. His reasoning was: we can't use language X because it
> doesn't have static typing, and any language that doesn't have static
> typing could produce run-time type errors and that would be bad. So we'll
> use C++, which has static typing, instead.
Any manager that believes that C++ does not have runtime errors is grossly
incompetent.
Barry Margolin
Erann Gat <g...@jpl.nasa.gov> wrote:
>The important point here is not what the programmer did, it's what the
>manager did. His reasoning was: we can't use language X because it
>doesn't have static typing, and any language that doesn't have static
>typing could produce run-time type errors and that would be bad. So we'll
>use C++, which has static typing, instead. The use of C++ was, IMO,
>directly causal in this case because it was not only a race condition, but
>it was a race condition that involved an implicit call to a destructor,
>which can only happen in a language without automatic memory management.
>So this manager traded one potential problem (run-time type errors) for a
>different potential problem with (nearly) disastrous results. But I don't
>believe he made this decision consciously. I believe - based on the
>conversation I had with him about development methodlogy - that he simply
>believed that static type checking trumps everything else, or at the very
>least that it has inherent value independent of all other considerations.
>And I'm saying that it doesn't.
On the other hand, Lisp doesn't have destructors at all because of its
automatic memory management. If you need to take care of cleaning up
state, you have to do some extra programming to handle it, whereas C's
implicit destructor calls are often just the right thing. This isn't going
to be familiar territory to Lisp programmers, so the chance of them getting
it right goes down.
Choosing a language almost always involves some trade-offs -- there's no
ultimate language that solves every problem. You pick your poison.
His logic isn't all that flawed. Program validation involves lots of
testing, and anything that reduces the dynamic conditions that you need to
test for seems like a good thing. All other things being equal (yes, I
know they aren't), static typing means that you don't have to do as much
testing for potential type errors, and can concentrate more on other things
during testing. Unfortunately, it seems like the programmers dropped the
ball on that -- they somehow seemed to be of the mind-set that using this
language allowed them to do even less testing than was necessary, so they
never discovered the timing problem.
Erann Gat
<dthie...@gmx.de> wrote:
> Frank A. Adrian <fad...@ancar.org> wrote:
> > Dirk Thierbach wrote:
> >
> >> Types encode invariants. They form a contract about the behaviour
> >> of some part of my code. If I break this contract in such a way that
> >> it changes the type, the type checker will point out all places
> >> I have to think about.
>
> > Why do you believe that all variables and parameters need this very strict
> > invariant during all phases of program development,
>
> Because unless I explicitely say so, this invariant will be the minimal
> invariant needed to make the program work at all. Let's again have a
> look at the type of map
>
> map :: (a -> b) -> [a] -> [b]
>
> This just says that one argument should be a function, and the other
> argument should be a list. Duh. Moreover, the function should be able
> to deal with the elements that are in the list. In return, I am
> promised a list of whatever things the function produces.
>
> If any of these invariants is invalidated, map cannot possibly work.
> So either I have made a typo somewhere, or I have made a design error.
What is the type of this function:
(defun mapn (fn &rest lists)
(if (every #'null lists)
nil
(cons (apply fn (remove nil (mapcar #'car lists)))
(apply #'mapn fn (mapcar #'cdr lists)))))
in light of this example:
? (mapcar 'type-of (mapn (compose 'sqrt '+) '(1 2 3) '(nil 5 -41/4 1)
'(-101.7 5 5 -3/4 nil)))
((COMPLEX FLOAT) DOUBLE-FLOAT (COMPLEX RATIONAL) RATIO FIXNUM)
E.
Erann Gat
<ga...@sage.att.com> wrote:
> g...@jpl.nasa.gov (Erann Gat) wrote:
>
> > No, I am saying that I don't believe in static typing because I have met
> > very smart people who ended up doing very stupid things as a result (I
> > believe) of using static typing systems.
>
> so i take it you are opposed to four-wheel-drive and anti-lock
> brakes in cars?
There's actually empirical evidence that anti-lock brakes don't reduce the
number of accidents because people just drive more carelessly as a result
of having them. (Interesting you should bring up this example. Just the
other day I ended up sailing through an intersection because my ABS kicked
in when I wasn't expecting it to. I was going about 20 MPH downhill on a
rainy day.)
E.
Erann Gat
<barry.m...@level3.com> wrote:
> In article <gat-181103...@192.168.1.51>,
> Erann Gat <g...@jpl.nasa.gov> wrote:
> >No, I am saying that I don't believe in static typing because I have met
> >very smart people who ended up doing very stupid things as a result (I
> >believe) of using static typing systems.
>
> What you're basically indicting is not static typing, but most forms of
> automation.
No, what I am indicting is what I perceive to be the undue emphasis placed
on static typing in some quarters, not static typing itself.
E.
Erann Gat
<seha...@raytheon.com> wrote:
> g...@jpl.nasa.gov (Erann Gat) writes:
>
> > Ironically, I actually agree with this.
>
> Can you elaborate? How do types interact with timing conditions?
Static analysis can be used to detect race conditions and other
multi-threading bugs like potential deadlocks. It's not exactly static
typing, but the techniques are similar. And unlike static typing, the
typical mode in which these techniques are deployed is as an adjunct to a
programming language, not as built-in parts of programming languages which
refuse to run your code until you pass all their tests.
This isn't ideal either IMO, because you have to jump through all sorts of
hoops to get your code in a form where the tool can deal with it. The
ideal solution IMO would be to have tools like this -- static analysis for
multithreading bugs, type bugs, etc. -- built-in but optional.
E.
Erann Gat
tayss...@yahoo.com (Tayss) wrote:
> BTW Erann, I didn't mean to sound hostile or critical; I had been
> reading a flamewar and maybe a couple of rhetorical flourishes stuck
> in my head. Especially strange since I mainly agree.
No worries, mate.
E.