Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!swrinde!elroy.jpl.nasa.gov!decwrl!pa.dec.com!shlump.nac.dec.com!engage!marx.enet.dec.com!grier
From: grier@marx.enet.dec.com
Newsgroups: comp.lang.misc
Subject: RE: Dynamic typing (part 3)
Message-ID: <1991Mar14.183323.27020@engage.enet.dec.com>
Date: 14 Mar 91 18:33:23 GMT
References: <626@optima.cs.arizona.edu>
Sender: news@engage.enet.dec.com (USENET News System)
Reply-To: grier@marx.enet.dec.com ()
Organization: Digital Equipment Corporation
Lines: 233

In article <626@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (David
Gudeman) writes:
|> In article  <1991Mar13.163629.12630@engage.enet.dec.com>
|> grier@marx.enet.dec.com writes:
|> ]
|> ]   In mathematics, it makes NO sense to talk about applying a
|> function
|> ]or operation to a symbol unless the symbol is known to be in the
|> ]domain of the operation/function.  I.e. writing something like "for
|> all
|> ]x, exp(x) is greater than zero" is nonsense.
|> 
|> Nonsense.  Anybody with a clue immediately understands that x is
|> restricted to values in the domain of exp.
|> 

   Wrong.   If you consider a proof to have some static notion of
correctness (which is exactly what they are,) this kind of error is
absolutely wong in a formal exhibition of the proof.

   True, when we're talking and scribbling on the board working
through examples, we'd use the "usual" meanings and not necessarily
be exact, but if you're submitting the proof for formal inspection, in
a journal or book or on an exam, IT IS WRONG.

   But then, I believe this is also the root of my belief that static typing
of variables, included with inheritance for reuse and genericity and some
sort of a "type_case" construct to permit more specialized operations in
a controlled fashion, is correct.  (i.e. it's implicit that if I write
"5+6 = 11"
on the board, I'm referring to the addition operator for the integers
or
possibly naturals.  If you think I'm arguing for specially writing code
to deal with all of the possibly addition definitions, you're missing
the
part of my argument about subtyping.)

|> ]...  In David Gudeman's example, I most
|> ]certainly don't want some "read()" operation which can return ANY
|> ]type of value to allow my code to blindly attempt to apply the "+" or
|> ]"Log()" operator to it.
|> 
|> In the first place, the read() only produced ints and floats, and the
|> return value was used in a context where either was a legal value.  In
|> the second place, if the read() function were defined to return other
|> sorts of values and you wrote "x + read()" the problem would be in the
|> program, not in the definition of "read()".

   Where is this knowledge known?  Your arguments so far have been to
not explicitly state the type of value accepted by or returned by an
operator.  And it still doesn't help when "Read()" is extended in the
future to return strings, cats and dogs.

|> 
|> ]My code should have some reason to believe
|> ]that "Log()" makes sense when applied to the value.  Statically checked,
|> ]before allowing me or anyone else to run it.
|> 
|> Then you are going to need types "positive int" and "positive float".
|> Do you also want type security for division?  Then you are going to
|> need "non-0 int", "non-0 float", as well as "positive non-0 int", etc.
|> I count 8 numeric types needed just to get type security for two
|> common operations.  The point is that static type checking involves an
|> essentially arbitrary set of restrictions, and there is no evidence
|> that it adds to program security at all.

   That's silly.  I'm arguing this in the light of subtyping, so you could
have some sort of abstract subtype called "Algebraic" or "Number" where
it has the "usual" operations defined.

   ReadNumber() would return a "Number" to permit at least type-safety.
This is a case where the compiler would not have a choice but defer the
binding of the operation invocation to actual code/methods until run-time,
but it's still working in a statically typed type-safe environment.

|> 
|> I will concede that optional type declarations might help program
|> security in the same way that optional assert clauses do.  (I don't
|> object to having type declarations in a language, I object to
|> _required_ type declarations.)  However, for many variables there is
|> no need to declare the type since it is obvious from the var's use,
|> and programmers should be smart enough to know the difference.
|> Whatever makes a language designer think --at language design time--
|> that he knows more about the requirements of a program than the
|> programmer will know --at program design time?
|> 

   She doesn't.  That's why I argue for subtyping/inheritance/genericity/etc.

   The language is the framework and syntax to work in.  It should be
minimal and formal.

   There's no one language for mathematics, but if you DO pick one, it's
very formal and minimal (usually it just involves notions of n-ary operators,
groupings via parenthesis - not necessary if you use prefix notation - and
quantifiers.  But look what you can do once you've build up your base of
operations and theorems!)

|> ]... I just wouldn't do my banking or trust my life to software which
|> ]relies on extensive testing rather than some level of ensurred correctness.
|> 
|> You must be joking.  Static type checking doesn't give any reasonable
|> level of assurance at all -- it is never the case that simply because
|> program compiles without errors, there is reason to believe that it
|> has some level of reliability.  Testing is the _only_ known way to
|> give any assurance at all.  And a given amount of testing generally
|> provides more assurance for a language with dynamic typing than it
|> would for a language with static typing.  (Because programs in
|> dynamically typed languages are usually much smaller and have fewer
|> paths to test.)

   Actually, formal proof is the only known way to ensure any measure of
static correctness.  Testing is like the old joke about "all odd numbers are
prime"... (let's see... 3, 5, 7, wow, yeah, I guess they are!)  Exhaustive
testing is also possible, but the claim nowadays is that software systems are
the most complex things mankind has ever built.  Now, I know that
simulations of electronic circuits usually run for hours/months trying to
exhaustively test strange conditions.  And they *still* find bugs years later
due to some strange signal path.

   You're going to tell me that some poking around by either the developers
or users is going to exhaustively test a software system?

   Formal proof is rather unwieldy in my opinion in software right now, but
I believe it's because we don't have a good enough set of theorems to work
with.  (The CS proofs I read tend to either be extremely vague, or end up
doing the equivalent of re-proving that 1+1=2 over and over again.  I argue
that code is a proof of an algorithm, and the compiler should do as much as
it can to check it before allowing it to be executed.  Certain semantics are
IMO beyond the realm of computers to verify, but correctness of structure
and syntax are certainly possible.)

   We're well beyond the topic now though... back to dynamic typing.

|> 
|> ]   Heck, there's an even more direct parallel.  Syntax checking! 
|> Next thing,
|> ]why don't we have languages where they "try" to interpret commands
|> and
|> ]do what their best guess to the requested operations are!
|> ]
|> ]   I don't WANT a smart computer, I don't WANT a computer which can
|> ]misinterpret ambiguous commands, I don't WANT a computer which
|> ]can forget...
|> 
|> There is no parallel there at all.  Dynamically typed languages in
|> no
|> sense try to interpret ambiguous commands or "guess" what is wanted.
|> The typing rules are just as unambiguous in a dynamically typed
|> language as in a statically typed language.  But in the dynamically
|> typed language the rules are simpler, more intuitive, and easier to
|> use.  (Depending on the language of course -- I wouldn't argue that
|> Smalltalk's rules are any of the above...)
|> 

   Once you've built up a large type library, the chances that any one
person has a detailed gestalt of the whole thing is very unlikely.  Therefore,
unless you explicitly restrict the type of a value you receive, you can only
assume that it's any type.  Therefore the complex operation application rules
(well, they're probably not complex, but when you have a library of
hundreds or thousands of types you start to hit a level of complexity where
it *looks* almost like guessing,) aren't totally predictable and you can get
an unexpected operation invoked.

   That's clearly a loose argument.

   Again, one more time, with feeling, my concern is with large software
systems.  If you're toying around with some new means to perform
parallel decomposition of a relational join, your domain is probably small
enough that you could maintain the simulation correctly yourself with
a dynamically typed system.  This is great for prototyping and research.
Let the ideas flow!

   Real-life systems get quite large and no one person has the complete and
total understanding of the whole system that you might in a limited domain.
This is my argument.  I'm sorry, David, if I've taken away from the
pure discussion of the topic and it's an interesting one even outside of
the engineering aspects, but I'm responding largely to the claims that
some testing by (a) people who know the system or (b) people who are
likely to only push the buttons that the (a) folks told them to are going to
ensure anything.

   Having something of a mathematical background, I believe that the
True Path to Software Engineering and Correctness is by building up
layers and levels of provably correct software.  (If I'm proving some sort
of extension theorem in topology, I don't have to continually prove
basic identities of fields.)  I'm also a fan of Eiffel, which allows for
building
up of these layers, refining them as you go along.  (It has its
problems,
but more than any other language I know of today, I think it's on the
right track for enabling building of large extensible systems.)

|> ]... and some program writes past the end of an array, blasting
|> ]away the stack, crashing the ATC computer,)
|> 
|> You are confusing weak typing with dynamic typing.  I don't know of
|> any dynamically typed language that lets you write past the end of an
|> array (unless it first expands the array).
|> 

   You're right.  I was in unnaturally early yesterday and not everything
came out as it would have after a good cup of coffee.  :-)

|> ]   This is tiring.  If you don't agree with me, that's OK, but I hope you
|> ]stay in the research world rather than producing software which people
|> ]pay for and expect to work reliably.
|> 
|> I'm sure that the thousands of people currently using and relying on
|> software written in dynamically typed languages are touched by your
|> concern.  We aren't worried about it though, we'll just go on using
|> easily modifiable software that was written in half the time with
|> twice the functionality, with no loss of reliabilty.  (Although we
|> _do_ have to buy faster machines or put up with slower response.)

   Yup, and it's going to cost when we have to maintain those
systems for the next 5-20 years.  Or are we going to just re-develop
them all over again when we need to extend them?  There go all your
claims of productivity and efficiency for the programmer.  Remember that
most of the cost of a software system is in the long term maintenance
and evolution - not in the initial development.

|> --
|> 					David Gudeman
|> gudeman@cs.arizona.edu
|> noao!arizona!gudeman
|> 
------------------------------------------------------------------------
I'm saying this, not Digital.  Don't hold them responsibile for it!

Michael J. Grier                           Digital Equipment Corporation
(508) 496-8417                             grier@leno.dec.com
Littleton, Mass, USA                       Mailstop OGO1-1/R6